The trace validation still faces challenges, including the fact that …

…nodes deactivating are not logged in the implementation. This leads to a rejected trace when a seemingly active node passes the token. TLC's limitation in supporting the composition of actions (compare section 7.3 (page 76ff) of Lamport's Specifying Systems) prevents the TraceSpec from defining its next-state relation by conjoining Deactivate \cdot PassToken. However, this limitation can be overcome by defining a suitable action that deactivates the node when it passes the token.
tlaplus · Apr 10, 2023 · ad8988f · ad8988f
1 parent 98c4d40
commit ad8988f
Showing 1 changed file with 10 additions and 3 deletions.
diff --git a/specifications/ewd998/EWD998ChanTrace.tla b/specifications/ewd998/EWD998ChanTrace.tla
@@ -34,14 +34,21 @@ TraceLog ==
 
 -----------------------------------------------------------------------------
 
+DeactivateAndPassToken ==
+    \E i \in Node:
+        /\ PassToken(i)!2
+        /\ PassToken(i)!3
+        /\ active' = [active EXCEPT ![i] = FALSE]
+        /\ UNCHANGED counter
+
 TraceSpec ==
     \* Because of  [A]_v <=> A \/ v=v'  , the following formula is logically
      \* equivalent to the (canonical) Spec formual  Init /\ [][Next]_vars  .  
      \* However, TLC's breadth-first algorithm does not explore successor
      \* states of a *seen* state.  Since one or more states may appear one or 
      \* more times in the the trace, the  UNCHANGED vars  combined with the
      \*  TraceView  that includes  TLCGet("level")  is our workaround. 
-    Init /\ [][Next \/ UNCHANGED vars]_vars
+    Init /\ [][Next \/ UNCHANGED vars \/ DeactivateAndPassToken]_vars
 
 -----------------------------------------------------------------------------
 
@@ -100,8 +107,7 @@ IsPassToken(l) ==
         /\ \A idx \in DOMAIN inbox'[snd]:
                 inbox'[snd][idx].type # "tok"
         \* Sender has to be inactive to pass the token, i.e
-        /\ ~active[snd]
-        /\ UNCHANGED <<active, counter>>                            
+        /\ UNCHANGED <<counter>>                            
 
 IsRecvToken(l) ==
     \* Log statement was printed by the receiver.
@@ -221,6 +227,7 @@ TraceAlias ==
         enabled |-> 
             [
                 InitToken  |-> ENABLED InitiateProbe,
+                DeAndPass  |-> ENABLED DeactivateAndPassToken,
                 PassToken  |-> ENABLED \E i \in Node \ {0} : PassToken(i),
                 SendMsg    |-> ENABLED \E i \in Node : SendMsg(i),
                 RecvMsg    |-> ENABLED \E i \in Node : RecvMsg(i),