A system with *one* node won't see the token moving.

tlaplus · Apr 10, 2023 · 75673c4 · 75673c4
1 parent ff7a49a
commit 75673c4
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/specifications/ewd998/EWD998ChanTrace.tla b/specifications/ewd998/EWD998ChanTrace.tla
@@ -76,8 +76,8 @@ IsInitiateToken(l) ==
         /\ \E idx \in DOMAIN inbox[snd]:
                 inbox[snd][idx].type = "tok"
         \* The senders's inbox contains no longer the token in the next state.
-        /\ \A idx \in DOMAIN inbox'[snd]:
-                inbox'[snd][idx].type # "tok"
+        /\ snd # rcv => \A idx \in DOMAIN inbox'[snd]:
+                            inbox'[snd][idx].type # "tok"
         \* Sender has *not* to be inactive to initiate the token!
         /\ UNCHANGED <<active, counter>>