.

Route.tla

@@ -160,8 +160,12 @@ PathCorrect(p) ==
       [] Len(p) = 1  -> p[1] \in Nodes
       [] OTHER       -> {p[1],p[2]} \in Edges /\ PathCorrect(Tail(p))
 
+\* SeqN is like Seq but produces sequences with Len =< N
+SeqN(S, N) == UNION {[1..n -> S] : n \in 1..N}
+
+
 \* PathMinimal verifies that path p has minimal length in between p0 and pEND.
-PathMinimal(p) == ~ \E pp \in Seq(Nodes) :
+PathMinimal(p) == ~ \E pp \in SeqN(Nodes, Cardinality(Nodes)) :
                         /\ pp /= << >>
                         /\ Len(pp) < Len(p)
                         /\ pp[1] = p[1]

Route.toolbox/Route___Model_1.launch

@@ -39,5 +39,6 @@
         <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)) ]"/>
     </listAttribute>
 </launchConfiguration>