Track registered values for each node individually

syn.cfg

@@ -3,7 +3,7 @@ NEXT Next
 
 CONSTANTS
 Nodes = {n1, n2}
-MaxValues = 10
+MaxValues = 5
 
 INVARIANTS
 AllRegistered

syn.tla

@@ -3,53 +3,51 @@ EXTENDS FiniteSets, Integers, Sequences
 
 CONSTANTS Nodes, MaxValues
 
-VARIABLES inbox, registered, next_val, added, removed
+VARIABLES inbox, registered, locally_registered, next_val
 
-vars == <<inbox, registered, next_val, added, removed>>
+vars == <<inbox, registered, locally_registered, next_val>>
 
 Init ==
     /\ inbox = [n \in Nodes |-> <<>>]
-    /\ registered = [n \in Nodes |-> {}]
+    /\ registered = {}
+    /\ locally_registered = [n \in Nodes |-> {}]
     /\ next_val = 0
-    /\ added = 0
-    /\ removed = 0
 
 Register(n) ==
     /\ next_val < MaxValues
-    /\ registered' = [registered EXCEPT![n] = registered[n] \union {next_val}]
+    /\ registered' = registered \union {next_val}
+    /\ locally_registered' = [locally_registered EXCEPT![n] = locally_registered[n] \union {next_val}]
     /\ next_val' = next_val + 1
-    /\ added' = added + 1
     /\ inbox' = [o \in Nodes |-> IF o = n THEN inbox[o] ELSE Append(inbox[o], [action |-> "sync_register", name |-> next_val])]
-    /\ UNCHANGED <<removed>>
 
 SyncRegister(n) ==
     /\ Len(inbox[n]) > 0
     /\ Head(inbox[n]).action = "sync_register"
-    /\ registered' = [registered EXCEPT![n] = registered[n] \union {Head(inbox[n]).name}]
+    /\ locally_registered' = [locally_registered EXCEPT![n] = locally_registered[n] \union {Head(inbox[n]).name}]
     /\ inbox' = [inbox EXCEPT![n] = Tail(inbox[n])]
-    /\ UNCHANGED <<removed, added, next_val>>
+    /\ UNCHANGED <<registered, next_val>>
 
 ItemToRemove(n) ==
-    CHOOSE r \in registered[n]: TRUE
+    CHOOSE r \in locally_registered[n]: TRUE
 
 Unregister(n) ==
-    /\ Cardinality(registered[n]) > 0
+    /\ Cardinality(locally_registered[n]) > 0
     /\ LET item_to_remove == ItemToRemove(n)
-        IN registered' = [registered EXCEPT![n] = registered[n] \ {item_to_remove}]
+        IN registered' = registered \ {item_to_remove}
+        /\ locally_registered' = [locally_registered EXCEPT![n] = locally_registered[n] \ {item_to_remove}]
         /\ inbox' = [o \in Nodes |-> IF o = n THEN inbox[o] ELSE Append(inbox[o], [action |-> "sync_unregister", name |-> item_to_remove])]
-    /\ removed' = removed + 1
-    /\ UNCHANGED <<added, next_val>>
+    /\ UNCHANGED <<next_val>>
 
 SyncUnregister(n) ==
     /\ Len(inbox[n]) > 0
     /\ Head(inbox[n]).action = "sync_unregister"
-    /\ registered' = [registered EXCEPT![n] = registered[n] \ {Head(inbox[n]).name}]
+    /\ locally_registered' = [locally_registered EXCEPT![n] = locally_registered[n] \ {Head(inbox[n]).name}]
     /\ inbox' = [inbox EXCEPT![n] = Tail(inbox[n])]
-    /\ UNCHANGED <<removed, added, next_val>>
+    /\ UNCHANGED <<registered, next_val>>
 
 Complete ==
     /\ next_val = MaxValues
-    /\ UNCHANGED <<inbox, added, next_val, registered, removed>>
+    /\ UNCHANGED <<inbox, registered, next_val, locally_registered>>
 
 Next ==
     /\ \E n \in Nodes:
@@ -63,7 +61,7 @@ Spec == Init /\ [][Next]_vars
 
 AllRegistered ==
     \A n \in Nodes:
-        Len(inbox[n]) = 0 => Cardinality(registered[n]) = (added - removed)
+        Len(inbox[n]) = 0 => locally_registered[n] = registered
 
 AllMessagesProcessed ==
     \A n \in Nodes: