.

Route.tla

@@ -54,15 +54,18 @@ EdgeQQ(e) == LET x == CHOOSE x \in e : TRUE
                  IN
                     {<<x,y>>, <<y,x>>}
 
+\* All n->m and m<-n queues
+Queues == {e \in Nodes \X Nodes : {e[1],e[2]} \in Edges}
+
+
 (********
 --algorithm Route {
-  variables ZZdepth       \* node -> depth
-                = [[n \in Nodes |-> Inf]  EXCEPT ![root] = 0],
-            ZZparent      \* node -> parent node
-                = [[n \in Nodes |-> NoRoute]  EXCEPT ![root] = root],
-                
+  variables  
     \* msgs[<<n,m>>] is message queue for n->m
-            msgs = [q \in (UNION {EdgeQQ(e) : e \in Edges})  |->  << >>];
+\*  msgs = [q \in (UNION {EdgeQQ(e) : e \in Edges})  |->
+    msgs = [q \in Queues  |->
+                   IF q[1] = root THEN <<0>>  \* start with root sending initial messages
+                                  ELSE << >>];
 
   fair process (RT \in Nodes)
     variables depth  =  IF self = root THEN 0 ELSE Inf,
@@ -74,23 +77,23 @@ EdgeQQ(e) == LET x == CHOOSE x \in e : TRUE
   } 
 };
 ********)
-\* BEGIN TRANSLATION (chksum(pcal) = "65933661" /\ chksum(tla) = "ff5ab133")
-VARIABLES ZZdepth, ZZparent, msgs, depth, parent
+\* BEGIN TRANSLATION (chksum(pcal) = "c4d34ca9" /\ chksum(tla) = "7195f9d9")
+VARIABLES msgs, depth, parent
 
-vars == << ZZdepth, ZZparent, msgs, depth, parent >>
+vars == << msgs, depth, parent >>
 
 ProcSet == (Nodes)
 
 Init == (* Global variables *)
-        /\ 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})  |->  << >>]
+        /\ msgs = [q \in Queues  |->
+                          IF q[1] = root THEN <<0>>
+                                         ELSE << >>]
         (* 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 << ZZdepth, ZZparent, msgs, depth, parent >>
+            /\ UNCHANGED << msgs, depth, parent >>
 
 Next == (\E self \in Nodes: RT(self))