Include vector clock in token messages.

tlaplus · Jul 28, 2023 · cf26a3a · cf26a3a
1 parent 6a3a9ab
commit cf26a3a
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 16 deletions.
diff --git a/specifications/ewd998/EWD998ChanID.tla b/specifications/ewd998/EWD998ChanID.tla
@@ -50,24 +50,27 @@ vars == <<active, color, counter, inbox, clock>>
 ------------------------------------------------------------------------------
 
 Init ==
+  (* Each node maintains a (local) vector clock *)
+  (* https://en.wikipedia.org/wiki/Vector_clock *)
+  /\ clock = [ n \in Node |-> IF n = Initiator 
+                THEN [ m \in Node |-> IF m = Initiator THEN 1 ELSE 0 ]
+                ELSE [ m \in Node |-> 0 ] ]
   (* Rule 0 *)
   /\ counter = [n \in Node |-> 0] \* c properly initialized
   /\ inbox = [n \in Node |-> IF n = Initiator 
-                              THEN << [type |-> "tok", q |-> 0, color |-> "black" ] >> 
+                              THEN << [type |-> "tok", q |-> 0, color |-> "black", vc |-> clock[n] ] >> 
                               ELSE <<>>] \* with empty channels.
   (* EWD840 *) 
   /\ active \in [Node -> BOOLEAN]
   /\ color \in [Node -> Color]
-  (* Each node maintains a (local) vector clock *)
-  (* https://en.wikipedia.org/wiki/Vector_clock *)
-  /\ clock = [n \in Node |-> [m \in Node |-> IF m = Initiator THEN 1 ELSE 0] ]
 
 InitiateProbe(n) ==
   /\ n = Initiator
   (* Rule 1 *)
   /\ \E j \in 1..Len(inbox[Initiator]):
       \* Token is at node the Initiator.
       /\ inbox[Initiator][j].type = "tok"
+      /\ clock' = [clock EXCEPT ![n] = Merge(n, inbox[n][j].vc, @)]
       /\ \* Previous round inconsistent, if:
          \/ inbox[Initiator][j].color = "black"
          \/ color[Initiator] = "black"
@@ -78,13 +81,10 @@ InitiateProbe(n) ==
       /\ inbox' = [inbox EXCEPT ![RingOfNodes[Initiator]] = Append(@, 
            [type |-> "tok", q |-> 0,
              (* Rule 6 *)
-             color |-> "white"]), 
+             color |-> "white", vc |-> clock[n]']), 
              ![Initiator] = RemoveAt(@, j) ] \* consume token message from inbox[0]. 
   (* Rule 6 *)
   /\ color' = [ color EXCEPT ![Initiator] = "white" ]
-  \* TODO: Do we attach i's vector clock along with the token?  For now, token-
-   \* TODO: related actions are treated as internal events.
-  /\ clock' = [ clock EXCEPT ![Initiator][Initiator] = @ + 1 ]
   \* The state of the nodes remains unchanged by token-related actions.
   /\ UNCHANGED <<active, counter>>                            
 
@@ -94,18 +94,18 @@ PassToken(n) ==
   /\ ~ active[n] \* If machine i is active, keep the token.
   /\ \E j \in 1..Len(inbox[n]) : 
           /\ inbox[n][j].type = "tok"
+          /\ clock' = [clock EXCEPT ![n] = Merge(n, inbox[n][j].vc, @)]
           \* the machine nr.i+1 transmits the token to machine nr.i under q := q + c[i+1]
           /\ LET tkn == inbox[n][j]
              IN  inbox' = [inbox EXCEPT ![RingOfNodes[n]] = 
                                        Append(@, [tkn EXCEPT !.q = tkn.q + counter[n],
                                                              !.color = IF color[n] = "black"
                                                                        THEN "black"
-                                                                       ELSE tkn.color]),
+                                                                       ELSE tkn.color,
+                                                             !.vc = clock[n]' ]),
                                     ![n] = RemoveAt(@, j) ] \* pass on the token.
   (* Rule 7 *)
   /\ color' = [ color EXCEPT ![n] = "white" ]
-  \* Just increment the node's local clock on token messages.
-  /\ clock' = [ clock EXCEPT ![n][n] = @ + 1 ]
   \* The state of the nodes remains unchanged by token-related actions.
   /\ UNCHANGED <<active, counter>>                            
 
@@ -187,7 +187,9 @@ EWD998ChanInbox ==
             LAMBDA m: 
             IF m.type = "pl" 
             THEN [type |-> "pl"] 
-            ELSE m) 
+            ELSE IF m.type = "tok"
+                 THEN [type |-> "tok", q |-> m.q, color |-> m.color]
+                 ELSE m) 
     ]
 
 (***************************************************************************)

diff --git a/specifications/ewd998/EWD998ChanID_shiviz.tla b/specifications/ewd998/EWD998ChanID_shiviz.tla
@@ -27,18 +27,20 @@ EXTENDS EWD998ChanID, TLC, TLCExt, Json
 \* Init  except that  active  and  color  are restricted to TRUE and "white" to
  \* not waste time generating initial states nobody needs.
 MCInit ==
+  (* Each node maintains a (local) vector clock *)
+  (* https://en.wikipedia.org/wiki/Vector_clock *)
+  /\ clock = [ n \in Node |-> IF n = Initiator 
+                THEN [ m \in Node |-> IF m = Initiator THEN 1 ELSE 0 ]
+                ELSE [ m \in Node |-> 0 ] ]
   (* Rule 0 *)
   /\ counter = [n \in Node |-> 0] \* c properly initialized
   /\ inbox = [n \in Node |-> IF n = Initiator 
-                              THEN << [type |-> "tok", q |-> 0, color |-> "black" ] >> 
+                              THEN << [type |-> "tok", q |-> 0, color |-> "black", vc |-> clock[n] ] >> 
                               ELSE <<>>] \* with empty channels.
   (* EWD840 *)
   \* Reduce the number of initial states. 
   /\ active \in [Node -> {TRUE}]
   /\ color \in [Node -> {"white"}]
-  (* Each node maintains a (local) vector clock *)
-  (* https://en.wikipedia.org/wiki/Vector_clock *)
-  /\ clock = [n \in Node |-> [m \in Node |-> IF m = Initiator THEN 1 ELSE 0] ]
 
 Inv ==
     \* TODO Choose some upper length or a invariant that produces a more