.

Route.tla

@@ -186,6 +186,21 @@ PathMinimal(p) == ~ \E pp \in SeqN(Nodes, Cardinality(Nodes)) :
                         /\ PathCorrect(pp)
 
 
+\* Dist is len of minimal path in between n-m.
+RECURSIVE _Dist(_, _)
+_Dist(n, S) ==
+    IF n \in S THEN 1
+    ELSE
+        LET S_ == S \cup {m \in Nodes : {n,m} \in Edges}
+        IN
+            IF S_ = S THEN Inf
+                      ELSE
+                           LET d == _Dist(n, S_)
+                           IN
+                                IF d = Inf THEN Inf
+                                           ELSE 1 + d
+Dist(n,m) == _Dist(n, {m})
+
 \* Paths are OK if they are all correct and minimal.
 PathsOK == \A n \in Nodes :
                  LET p == ParentPath(n)
@@ -194,6 +209,7 @@ PathsOK == \A n \in Nodes :
                      /\ p[Len(p)] = root  \* not NoRoute
                      /\ PathCorrect(p)
                      /\ PathMinimal(p)
+                     /\ Len(p) = Dist(n, root)
 
 \* 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="115"/>
+    <intAttribute key="fpIndex" value="14"/>
     <intAttribute key="maxHeapSize" value="25"/>
     <stringAttribute key="modelBehaviorInit" value=""/>
     <stringAttribute key="modelBehaviorNext" value=""/>