.

Route.tla

@@ -191,7 +191,7 @@ RECURSIVE _Dist(_, _)
 _Dist(n, S) ==
     IF n \in S THEN 1
     ELSE
-        LET S_ == S \cup {m \in Nodes : {n,m} \in Edges}
+        LET S_ == S \cup {x \in Nodes : \E y \in S : {x,y} \in Edges}
         IN
             IF S_ = S THEN Inf
                       ELSE

Route.toolbox/Route___Model_1.launch

@@ -5,7 +5,7 @@
     <stringAttribute key="distributedNetworkInterface" value="192.168.122.1"/>
     <intAttribute key="distributedNodesCount" value="1"/>
     <stringAttribute key="distributedTLC" value="off"/>
-    <intAttribute key="fpIndex" value="14"/>
+    <intAttribute key="fpIndex" value="15"/>
     <intAttribute key="maxHeapSize" value="25"/>
     <stringAttribute key="modelBehaviorInit" value=""/>
     <stringAttribute key="modelBehaviorNext" value=""/>
@@ -43,5 +43,6 @@
         <listEntry value="0[ n \in Nodes |-&gt; PathMinimal(ParentPath(n)) ]"/>
         <listEntry value="1[ n \in Nodes |-&gt; LET p == ParentPath(n) IN p[1] = n /\ p[Len(p)] = root]"/>
         <listEntry value="1PathsOK"/>
+        <listEntry value="1[ n \in Nodes |-&gt; Dist(n, root) ]"/>
     </listAttribute>
 </launchConfiguration>