Align with commit cf26a3a changing record domain in EWD998ChanID.

Signed-off-by: Markus Alexander Kuppe <[email protected]>

Author: lemmy

specifications/ewd998/EWD998ChanID_export.tla

@@ -13,16 +13,16 @@ EXTENDS EWD998ChanID, TLCExt, TLC, IOUtils, Json
 MCInit ==
   (* Rule 0 *)
   /\ counter = [n \in Node |-> 0] \* c properly initialized
-  /\ inbox = [n \in Node |-> IF n = Initiator 
-                              THEN << [type |-> "tok", q |-> 0, color |-> "black" ] >> 
-                              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 |-> 0] ]
+  /\ inbox = [n \in Node |-> IF n = Initiator 
+                              THEN << [type |-> "tok", q |-> 0, color |-> "black", vc |-> clock[n] ] >> 
+                              ELSE <<>>] \* with empty channels.
 
 ----------------------------------------------------------------------------