.

Route.tla

@@ -216,10 +216,10 @@ THEOREM Terminated => PathsOK
 
 
 Inv == \A n \in Nodes :
-            /\ depth[n] >= Dist(n, root)
+            /\ depth[n] = Inf \/ depth[n]+1 >= Dist(n, root)
             /\ (depth[n] /= Inf) => (LET p == ParentPath(n) IN
                                         /\ p[Len(p)] = root
-                                        /\ Len(p) =< depth[n])
+                                        /\ Len(p) =< depth[n]+1)
 
 --------
 

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="60"/>
+    <intAttribute key="fpIndex" value="72"/>
     <intAttribute key="maxHeapSize" value="25"/>
     <stringAttribute key="modelBehaviorInit" value=""/>
     <stringAttribute key="modelBehaviorNext" value=""/>