.

Route.tla

@@ -57,10 +57,13 @@ EdgeQQ(e) == LET x == CHOOSE x \in e : TRUE
 \* All n->m and m<-n queues
 Queues == {e \in Nodes \X Nodes : {e[1],e[2]} \in Edges}
 
+QueuesFrom(n) == {q \in Queues : q[1] = n}
+QueuesTo(n)   == {q \in Queues : q[2] = n}
+
 
 (********
 --algorithm Route {
-  variables  
+  variables
     \* msgs[<<n,m>>] is message queue for n->m
 \*  msgs = [q \in (UNION {EdgeQQ(e) : e \in Edges})  |->
     msgs = [q \in Queues  |->
@@ -69,18 +72,33 @@ Queues == {e \in Nodes \X Nodes : {e[1],e[2]} \in Edges}
 
   fair process (RT \in Nodes)
     variables depth  =  IF self = root THEN 0 ELSE Inf,
-              parent =  IF self = root THEN root ELSE NoRoute;
+              parent =  IF self = root THEN root ELSE NoRoute,
+
+              m = -1; \* XXX must be temp.only (LET ... IN ...)
   {
     loop: while (TRUE) {
-            skip;
+            with (q \in {r \in QueuesTo(self) : msgs[r] /= << >>}) {
+              m := Head(msgs[q]);
+              msgs[q] := Tail(msgs[q]);
+       x:     if (m < depth - 1) {
+                depth := m + 1;
+                parent := q[1];
+                \* send m further to all neighbours except from whom we received it
+                msgs := [t \in Queues |->
+                            IF t \in QueuesFrom(self) \ {<<self, parent>>}
+                                THEN Append(msgs[t], depth)
+                                ELSE msgs[t] ]
+              }
+            }
+
           }
-  } 
+  }
 };
 ********)
-\* BEGIN TRANSLATION (chksum(pcal) = "c4d34ca9" /\ chksum(tla) = "7195f9d9")
-VARIABLES msgs, depth, parent
+\* BEGIN TRANSLATION (chksum(pcal) = "1b3e9734" /\ chksum(tla) = "76d3f425")
+VARIABLES msgs, depth, parent, m
 
-vars == << msgs, depth, parent >>
+vars == << msgs, depth, parent, m >>
 
 ProcSet == (Nodes)
 
@@ -91,16 +109,23 @@ Init == (* Global variables *)
         (* Process RT *)
         /\ depth = [self \in Nodes |-> IF self = root THEN 0 ELSE Inf]
         /\ parent = [self \in Nodes |-> IF self = root THEN root ELSE NoRoute]
+        /\ m = [self \in Nodes |-> -1]
 
-RT(self) == /\ TRUE
-            /\ UNCHANGED << msgs, depth, parent >>
+RT(self) == \E q \in {r \in QueuesTo(self) : msgs[r] /= << >>}:
+              /\ m' = [m EXCEPT ![self] = Head(msgs[q])]
+              /\ msgs' = [msgs EXCEPT ![q] = Tail(msgs[q])]
+              /\ IF m'[self] < depth[self] - 1
+                    THEN /\ depth' = [depth EXCEPT ![self] = m'[self] + 1]
+                         /\ parent' = [parent EXCEPT ![self] = q[1]]
+                    ELSE /\ TRUE
+                         /\ UNCHANGED << depth, parent >>
 
 Next == (\E self \in Nodes: RT(self))
 
 Spec == /\ Init /\ [][Next]_vars
         /\ \A self \in Nodes : WF_vars(RT(self))
 
-\* END TRANSLATION 
+\* END TRANSLATION
 
 (*
 TypeOK ==