Ensure duplicate names cannot be seen by any individual node

grahamrhay · Jan 17, 2024 · 033bb28 · 033bb28
1 parent 9323bb4
commit 033bb28
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 0 deletions.
diff --git a/syn.cfg b/syn.cfg
@@ -10,6 +10,7 @@ Symmetry
 
 INVARIANTS
 AllRegistered
+ThereCanBeOnlyOne
 
 PROPERTIES
 AllMessagesProcessed
diff --git a/syn.tla b/syn.tla
@@ -191,6 +191,20 @@ AllRegistered ==
     \A n \in Nodes:
         (\A o \in Nodes: Len(inbox[o]) = 0) /\ visible_nodes[n] = AllOtherNodes(n) => AllRegisteredForNode(locally_registered[n]) = registered
 
+RECURSIVE Duplicates(_, _, _)
+
+Duplicates(keys, struct, acc) ==
+    IF Cardinality(keys) < 2 THEN acc
+    ELSE
+        LET k1 == CHOOSE k \in keys: TRUE
+        k2 == CHOOSE k \in (keys \ {k1}): TRUE
+        duplicates == DOMAIN struct[k1] \intersect DOMAIN struct[k2]
+        IN Duplicates(keys \ {k1}, struct, duplicates \union acc)
+
+ThereCanBeOnlyOne ==
+    \A n \in Nodes:
+        Duplicates(DOMAIN locally_registered[n], locally_registered[n], {}) = {}
+
 AllMessagesProcessed ==
     \A n \in Nodes:
         <>(Len(inbox[n]) = 0)