.

Route.tla

@@ -62,7 +62,7 @@ EdgeQQ(e) == LET x == CHOOSE x \in e : TRUE
                 = [[n \in Nodes |-> NoRoute]  EXCEPT ![root] = root],
                 
             \* msgs[<<n,m>>] is message queue for n->m
-            msgs = [UNION {EdgeQQ(e) : e \in Edges} |-> <<>>];
+            msgs = [UNION {EdgeQQ(e) : e \in Edges}  |->  << >>];
 
   fair process (RT \in Nodes) {
     variables depth  = IF self = root THEN 0 ELSE Inf,