.

Route.tla

@@ -31,7 +31,6 @@ ReachableFrom(S) ==
             IF S_ = S THEN S
                       ELSE ReachableFrom(S_)
 
-
 ASSUME ReachableFrom({root}) = Nodes
 
 
@@ -83,7 +82,7 @@ QueuesTo(n)   == {q \in Queues : q[2] = n}
                   parent := q[1];
                   \* send m further to all neighbours except from whom we received it
                   with (msgs__ = [t \in Queues |->
-                            IF t \in QueuesFrom(self) \ {<<self, parent>>}
+                            IF t \in QueuesFrom(self) \ {<<self, q[1]>>}  \* XXX not q[1]->parent would be incorrect
                                 THEN Append(msgs_[t], depth)
                                 ELSE msgs_[t] ])
                     msgs := msgs__;
@@ -97,7 +96,7 @@ QueuesTo(n)   == {q \in Queues : q[2] = n}
   }
 };
 ********)
-\* BEGIN TRANSLATION (chksum(pcal) = "ef4913a" /\ chksum(tla) = "2e68ab65")
+\* BEGIN TRANSLATION (chksum(pcal) = "a6173f58" /\ chksum(tla) = "9d62fe6c")
 VARIABLES msgs, depth, parent
 
 vars == << msgs, depth, parent >>
@@ -119,7 +118,7 @@ RT(self) == \E q \in {r \in QueuesTo(self) : msgs[r] /= << >>}:
                      THEN /\ depth' = [depth EXCEPT ![self] = m + 1]
                           /\ parent' = [parent EXCEPT ![self] = q[1]]
                           /\ LET msgs__ ==      [t \in Queues |->
-                                           IF t \in QueuesFrom(self) \ {<<self, parent'[self]>>}
+                                           IF t \in QueuesFrom(self) \ {<<self, q[1]>>}
                                                THEN Append(msgs_[t], depth'[self])
                                                ELSE msgs_[t] ] IN
                                msgs' = msgs__