.

Route.tla

@@ -215,6 +215,12 @@ PathsOK == \A n \in Nodes :
 THEOREM Terminated => PathsOK
 
 
+Inv == \A n \in Nodes :
+            /\ depth[n] >= Dist(n, root)
+            /\ (depth[n] /= Inf) => (LET p == ParentPath(n) IN
+                                        /\ p[Len(p)] = root
+                                        /\ Len(p) =< depth[n])
+
 --------
 
 RECURSIVE SumSeq(_)

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="15"/>
+    <intAttribute key="fpIndex" value="60"/>
     <intAttribute key="maxHeapSize" value="25"/>
     <stringAttribute key="modelBehaviorInit" value=""/>
     <stringAttribute key="modelBehaviorNext" value=""/>
@@ -17,6 +17,7 @@
     <listAttribute key="modelCorrectnessInvariants">
         <listEntry value="1TypeOK"/>
         <listEntry value="1Terminated =&gt; PathsOK"/>
+        <listEntry value="1Inv"/>
     </listAttribute>
     <listAttribute key="modelCorrectnessProperties">
         <listEntry value="1&lt;&gt;Terminated"/>