.

Route.tla

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

Route.toolbox/Route___Model_1.launch

@@ -36,9 +36,12 @@
     <stringAttribute key="specName" value="Route"/>
     <stringAttribute key="tlcResourcesProfile" value="local custom"/>
     <listAttribute key="traceExploreExpressions">
+        <listEntry value="1Terminated"/>
         <listEntry value="1[ n \in Nodes |-&gt; ParentPath(n) ]"/>
-        <listEntry value="0[ n \in Nodes |-&gt; LET p == ParentPath(n) IN &lt;&lt; PathCorrect(p), PathMinimal(p) &gt;&gt; ]"/>
-        <listEntry value="1[ n \in Nodes |-&gt; PathCorrect(ParentPath(n)) ]"/>
-        <listEntry value="1[ n \in Nodes |-&gt; PathMinimal(ParentPath(n)) ]"/>
+        <listEntry value="1[ n \in Nodes |-&gt; LET p == ParentPath(n) IN &lt;&lt; PathCorrect(p), PathMinimal(p) &gt;&gt; ]"/>
+        <listEntry value="0[ n \in Nodes |-&gt; PathCorrect(ParentPath(n)) ]"/>
+        <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"/>
     </listAttribute>
 </launchConfiguration>