.

Route.tla

@@ -165,18 +165,21 @@ PathMinimal(p) == ~ \E pp \in Seq(Nodes) :
                         /\ pp /= << >>
                         /\ Len(pp) < Len(p)
                         /\ pp[1] = p[1]
-                        /\ pp[Len(pp)-1] = p[Len(p)-1]
+                        /\ pp[Len(pp)] = p[Len(p)]
                         /\ PathCorrect(pp)
 
 
-Correct == Terminated => (\A n \in Nodes :
-                                LET p == ParentPath(n)
-                                IN
-                                    /\ p[Len(p)-1] = root  \* not NoRoute
-                                    /\ PathCorrect(p)
-                                    /\ PathMinimal(p))
-
+\* Paths are OK if they are all correct and minimal.
+PathsOK == (\A n \in Nodes :
+                 LET p == ParentPath(n)
+                 IN
+                     /\ p[1] = n
+                     /\ p[Len(p)] = root  \* not NoRoute
+                     /\ PathCorrect(p)
+                     /\ PathMinimal(p))
 
+\* Paths must be all OK when terminated.
+THEOREM Terminated => PathsOK
 
 
 --------

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="20"/>
+    <intAttribute key="fpIndex" value="9"/>
     <intAttribute key="maxHeapSize" value="25"/>
     <stringAttribute key="modelBehaviorInit" value=""/>
     <stringAttribute key="modelBehaviorNext" value=""/>
@@ -16,6 +16,7 @@
     <booleanAttribute key="modelCorrectnessCheckDeadlock" value="false"/>
     <listAttribute key="modelCorrectnessInvariants">
         <listEntry value="1TypeOK"/>
+        <listEntry value="1Terminated =&gt; PathsOK"/>
     </listAttribute>
     <listAttribute key="modelCorrectnessProperties">
         <listEntry value="1&lt;&gt;Terminated"/>