.

Route.tla

@@ -44,32 +44,49 @@ m \prec n  ==  IF m = Inf THEN FALSE
 
 CONSTANT NoRoute \* = NoRoute
 
+
+\* Neigh(n) is set of n's neighbours.
+Neigh(n) == {x \in Nodes : {x,n} \in Edges}
+
+\* EdgeQQ({n,m}) is {<n,m>, <m,n>}
+EdgeQQ(e) == LET x == CHOOSE x \in e : TRUE
+             IN  LET y == CHOOSE y \in (e\{x}) : TRUE
+                 IN
+                    {<<x,y>>, <<y,x>>}
+
 (********
 --algorithm Route {
   variables depth       \* node -> depth
                 = [[n \in Nodes |-> Inf]  EXCEPT ![root] = 0],
             parent      \* node -> parent node
-                = [n \in Node |->  IF n = root THEN root ELSE NoRoute];
-  process (RT \in Nodes) {
+                = [[n \in Nodes |-> NoRoute]  EXCEPT ![root] = root],
+                
+            \* msgs[<<n,m>>] is message queue for n->m
+            msgs = [UNION {EdgeQQ(e) : e \in Edges} |-> <<>>];
+
+  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) = "9a717d8a" /\ chksum(tla) = "9b3808dd")
-VARIABLES depth, parent
+\* BEGIN TRANSLATION (chksum(pcal) = "b5e3ebb1" /\ chksum(tla) = "59198579")
+VARIABLES depth, parent, msg
 
-vars == << depth, parent >>
+vars == << depth, parent, msg >>
 
 ProcSet == (Nodes)
 
 Init == (* Global variables *)
         /\ depth = [[n \in Nodes |-> Inf]  EXCEPT ![root] = 0]
-        /\ parent = [n \in Node |->  IF n = root THEN root ELSE NoRoute]
+        /\ parent = [[n \in Nodes |-> NoRoute]  EXCEPT ![root] = root]
+        /\ msg = [n,m \in Nodes |-> <<>>]
 
 RT(self) == /\ TRUE
-            /\ UNCHANGED << depth, parent >>
+            /\ UNCHANGED << depth, parent, msg >>
 
 Next == (\E self \in Nodes: RT(self))