.

Route.tla

@@ -56,41 +56,46 @@ EdgeQQ(e) == LET x == CHOOSE x \in e : TRUE
 
 (********
 --algorithm Route {
-  variables depth       \* node -> depth
+  variables ZZdepth       \* node -> depth
                 = [[n \in Nodes |-> Inf]  EXCEPT ![root] = 0],
-            parent      \* node -> parent node
+            ZZparent      \* node -> parent node
                 = [[n \in Nodes |-> NoRoute]  EXCEPT ![root] = root],
                 
             \* msgs[<<n,m>>] is message queue for n->m
-            msgs = [UNION {EdgeQQ(e) : e \in Edges}  |->  << >>];
+            msgs = [q \in (UNION {EdgeQQ(e) : e \in Edges})  |->  << >>];
 
-  fair process (RT \in Nodes) {
+  fair process (RT \in Nodes)
     variables depth  = IF self = root THEN 0 ELSE Inf,
               parent = IF self = root THEN root ELSE NoRoute;
+  {
     loop: while (TRUE) {
             skip;
           }
   } 
 };
 ********)
-\* BEGIN TRANSLATION (chksum(pcal) = "b5e3ebb1" /\ chksum(tla) = "59198579")
-VARIABLES depth, parent, msg
+\* BEGIN TRANSLATION (chksum(pcal) = "65933661" /\ chksum(tla) = "ff5ab133")
+VARIABLES ZZdepth, ZZparent, msgs, depth, parent
 
-vars == << depth, parent, msg >>
+vars == << ZZdepth, ZZparent, msgs, depth, parent >>
 
 ProcSet == (Nodes)
 
 Init == (* Global variables *)
-        /\ depth = [[n \in Nodes |-> Inf]  EXCEPT ![root] = 0]
-        /\ parent = [[n \in Nodes |-> NoRoute]  EXCEPT ![root] = root]
-        /\ msg = [n,m \in Nodes |-> <<>>]
+        /\ ZZdepth = [[n \in Nodes |-> Inf]  EXCEPT ![root] = 0]
+        /\ ZZparent = [[n \in Nodes |-> NoRoute]  EXCEPT ![root] = root]
+        /\ msgs = [q \in (UNION {EdgeQQ(e) : e \in Edges})  |->  << >>]
+        (* Process RT *)
+        /\ depth = [self \in Nodes |-> IF self = root THEN 0 ELSE Inf]
+        /\ parent = [self \in Nodes |-> IF self = root THEN root ELSE NoRoute]
 
 RT(self) == /\ TRUE
-            /\ UNCHANGED << depth, parent, msg >>
+            /\ UNCHANGED << ZZdepth, ZZparent, msgs, depth, parent >>
 
 Next == (\E self \in Nodes: RT(self))
 
-Spec == Init /\ [][Next]_vars
+Spec == /\ Init /\ [][Next]_vars
+        /\ \A self \in Nodes : WF_vars(RT(self))
 
 \* END TRANSLATION