vault backup: 2023-11-10 17:46:05

4a1s/MFES/PL - Aula 7.md

@@ -69,3 +69,66 @@ pred insert[n : Node] {
 
 
 ```
+
+//Solved
+```c
+// Recall the hash table Alloy model,
+// now with mutable lists inside the buckets.
+
+sig Bucket {
+	var head : lone Node
+}
+sig Node {
+	key : one Key,
+	var prox : lone Node
+}
+sig Key {
+	hash : one Hash
+}
+sig Hash {}
+
+// Specify the operation of inserting a node
+// in the hash table. The node should be 
+// inserted at the head of a bucket.
+// If the operation only works well when the
+// hash of the new node does not exist in the
+// table you get Two points. If it always 
+// works well you get Five points. Use the
+// respective commands to check how many
+// points you have.
+
+pred nodeToHead[n : Node]{
+  	//node not in hash
+  	n.key.hash not in Bucket.head.key.hash
+    
+	some b : Bucket | {
+		b.head= none and b.head' = n  //put node in the head
+        all x : Bucket - b | x.head' = x.head  //everything remains the same
+    	all y : Node | y.prox' = y.prox //all nodes remain the same
+	}
+  
+}
+
+
+pred nodeToTail[n: Node]{
+  //node not in linked lists of buckets
+  n not in Bucket.head.*prox
+  
+  //node in hash
+  n.key.hash in Bucket.head.key.hash
+  
+  some b : Bucket | {
+      b.head.key.hash = n.key.hash and {  //same hash
+        (b.head' = n and n.prox' = b.head)  //new head
+        all x : Bucket - b | x.head' = x.head //all other buckets remain the same
+        all y : Node - n | y.prox' = y.prox //all other nodes remain the same
+       }
+  }
+}
+
+pred insert[n : Node] {
+	nodeToHead[n] or nodeToTail [n] 
+}
+```
+
+http://alloy4fun.inesctec.pt/mnvLbxeXWRuhsnQSd