vault backup: 2023-10-23 21:28:40

4a1s/MFES/PL - Aula 5.md

@@ -49,7 +49,7 @@ pred Invs {
   	//all x, y: Node | x.key.hash != y.key.hash implies (x.prox != y and y.prox != x)
 
     //keys are unique to a single node
-  	all k: Key | one x: Node | x.key = k
+  	all x: Key | one y: Node | y.key = x
 
     //heads are unique to a single bucket (UNNECESSARY)
   	all x: Bucket | lone x.head
@@ -69,3 +69,48 @@ pred Invs {
 }
 
 ```
+
+
+// SOLVED
+```c
+sig Bucket {
+	head : lone Node
+}
+
+sig Node {
+	key : one Key,
+	prox : lone Node
+}
+
+sig Key {
+	hash : one Hash
+}
+
+sig Hash {}
+
+pred Invs {
+
+    // no node links to itself and its children don't link to it (no loops)
+  	all x: Node | x not in x.^prox
+  
+  	//for all nodes sequentially linked, they must have the same hash
+  	all x, y: Node | (x.prox = y) implies x.key.hash = y.key.hash
+  
+    //keys are unique to a single node
+  	all x: Key | one y: Node | y.key = x
+  
+  	//nodes must be prox to another node or be the head of a bucket
+   	all x: Node | (x in Bucket.head) or (x in Node.prox)
+  
+  	//different buckets must have different heads
+	all x, y: Bucket, z : Node | x != y and x.head = z implies y.head!=z
+  
+  	//keys must have a hash
+  	all x: Key | some y: Hash | x.hash = y
+  
+  	//nodes(heads) associated to different buckets, must differ in hash
+  	all x, y: Bucket | (x != y and x.head != none and y.head != none ) implies x.head.key.hash != y.head.key.hash
+}
+```
+
+http://alloy4fun.inesctec.pt/5yb5zPPJWP29SDSbD