Only check for local registrations

grahamrhay · Jan 22, 2024 · c21e84b · c21e84b
1 parent 3648c3c
commit c21e84b
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/syn.tla b/syn.tla
@@ -34,6 +34,9 @@ AllRegisteredNames(nodes, locals, registrations) ==
 RegisteredElsewhere(node) ==
     AllRegisteredNames(AllOtherNodes(node), locally_registered, {})
 
+RegisteredOnThisNode(node) ==
+    AllRegisteredNames({node}, locally_registered, {})
+
 Init ==
     /\ inbox = [n \in Nodes |-> <<>>]
     /\ registered = [n \in Names |-> 0]
@@ -122,7 +125,7 @@ UnregisterOnNode(n) ==
     /\ Head(inbox[n]).action = "unregister_on_node"
     /\ LET message == Head(inbox[n])
         l == [r \in (DOMAIN locally_registered[n][n] \ {message.name}) |-> locally_registered[n][n][r]]
-        already_removed == message.name \notin AllRegisteredForNode(locally_registered[n])
+        already_removed == message.name \notin RegisteredOnThisNode(n)
         IN
         (IF already_removed THEN
             \* {error, undefined}