.

Route.tla

@@ -72,33 +72,35 @@ QueuesTo(n)   == {q \in Queues : q[2] = n}
 
   fair process (RT \in Nodes)
     variables depth  =  IF self = root THEN 0 ELSE Inf,
-              parent =  IF self = root THEN root ELSE NoRoute,
-
-              m = -1; \* XXX must be temp.only (LET ... IN ...)
+              parent =  IF self = root THEN root ELSE NoRoute;
   {
     loop: while (TRUE) {
             with (q \in {r \in QueuesTo(self) : msgs[r] /= << >>}) {
-              m := Head(msgs[q]);
-              msgs[q] := Tail(msgs[q]);
-       x:     if (m < depth - 1) {
+              with (m = Head(msgs[q])) {
+              with (msgs_ = [msgs EXCEPT ![q] = Tail(msgs[q])]) {
+                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 |->
+                  with (msgs__ = [t \in Queues |->
                             IF t \in QueuesFrom(self) \ {<<self, parent>>}
-                                THEN Append(msgs[t], depth)
-                                ELSE msgs[t] ]
+                                THEN Append(msgs_[t], depth)
+                                ELSE msgs_[t] ])
+                    msgs := msgs__;
                 }
+                else {
+                  msgs := msgs_
+                }
+              }}
             }
-
           }
   }
 };
 ********)
-\* BEGIN TRANSLATION (chksum(pcal) = "1b3e9734" /\ chksum(tla) = "76d3f425")
-VARIABLES msgs, depth, parent, m
+\* BEGIN TRANSLATION (chksum(pcal) = "ef4913a" /\ chksum(tla) = "2e68ab65")
+VARIABLES msgs, depth, parent
 
-vars == << msgs, depth, parent, m >>
+vars == << msgs, depth, parent >>
 
 ProcSet == (Nodes)
 
@@ -109,15 +111,19 @@ 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) == \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]
+              LET m == Head(msgs[q]) IN
+                LET msgs_ == [msgs EXCEPT ![q] = Tail(msgs[q])] IN
+                  IF m < depth[self] - 1
+                     THEN /\ depth' = [depth EXCEPT ![self] = m + 1]
                           /\ parent' = [parent EXCEPT ![self] = q[1]]
-                    ELSE /\ TRUE
+                          /\ LET msgs__ ==      [t \in Queues |->
+                                           IF t \in QueuesFrom(self) \ {<<self, parent'[self]>>}
+                                               THEN Append(msgs_[t], depth'[self])
+                                               ELSE msgs_[t] ] IN
+                               msgs' = msgs__
+                     ELSE /\ msgs' = msgs_
                           /\ UNCHANGED << depth, parent >>
 
 Next == (\E self \in Nodes: RT(self))