.

Route.tla

@@ -161,14 +161,20 @@ PathCorrect(p) ==
       [] OTHER       -> {p[1],p[2]} \in Edges /\ PathCorrect(Tail(p))
 
 \* PathMinimal verifies that path p has minimal length in between p0 and pEND.
-PathMinimal(p) ==
+PathMinimal(p) == ~ \E pp \in Seq(Nodes) :
+                        /\ pp /= << >>
+                        /\ Len(pp) < Len(p)
+                        /\ pp[1] = p[1]
+                        /\ pp[Len(pp)-1] = p[Len(p)-1]
+                        /\ PathCorrect(pp)
+
 
 Correct == Terminated => (\A n \in Nodes :
                                 LET p == ParentPath(n)
                                 IN
                                     /\ p[Len(p)-1] = root  \* not NoRoute
-                                    /\ PathIsValid(p)
-                                    /\ PathIsMinimal(p)) 
+                                    /\ PathCorrect(p)
+                                    /\ PathMinimal(p))