.

Route.tla

@@ -157,7 +157,7 @@ ParentPath(n) ==
 RECURSIVE PathCorrect(_)
 PathCorrect(p) ==
     CASE p = << >>   -> FALSE
-      [] Len(p) = 1  -> p \in Nodes
+      [] Len(p) = 1  -> p[1] \in Nodes
       [] OTHER       -> {p[1],p[2]} \in Edges /\ PathCorrect(Tail(p))
 
 \* PathMinimal verifies that path p has minimal length in between p0 and pEND.

Route.toolbox/Route___Model_1.launch

@@ -35,4 +35,9 @@
     <stringAttribute key="result.mail.address" value=""/>
     <stringAttribute key="specName" value="Route"/>
     <stringAttribute key="tlcResourcesProfile" value="local custom"/>
+    <listAttribute key="traceExploreExpressions">
+        <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)) ]"/>
+    </listAttribute>
 </launchConfiguration>