.

Route.tla

@@ -138,11 +138,40 @@ Spec == /\ Init /\ [][Next]_vars
 
 Terminated == \A q \in Queues : msgs[q] = << >>
 
-(*
 TypeOK ==
-        /\ depth \in [Nodes -> Nat]
-        /\ parent \in [Nodes -> Nodes]
-*)
+        /\ depth \in [Nodes -> Nat \cup {Inf}]
+        /\ parent \in [Nodes -> Nodes \cup {NoRoute}]
+        /\ msgs \in [Queues -> Seq(Nat)]
+
+
+\* ParentPath returns path from node n to root constructed via parents.
+\* The path is of the form << n, ..., root | NoRoute >>.
+RECURSIVE ParentPath(_)
+ParentPath(n) ==
+    CASE n = root               -> << root >>
+      [] parent[n] = NoRoute    -> << n, NoRoute >>
+      [] OTHER                  -> << n >> \o ParentPath(parent[n])
+
+
+\* PathCorrect is true if p is correct path going through Edges.
+RECURSIVE PathCorrect(_)
+PathCorrect(p) ==
+    CASE p = << >>   -> FALSE
+      [] Len(p) = 1  -> p \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.
+PathMinimal(p) ==
+
+Correct == Terminated => (\A n \in Nodes :
+                                LET p == ParentPath(n)
+                                IN
+                                    /\ p[Len(p)-1] = root  \* not NoRoute
+                                    /\ PathIsValid(p)
+                                    /\ PathIsMinimal(p)) 
+
+
+
 
 --------
 

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="88"/>
+    <intAttribute key="fpIndex" value="20"/>
     <intAttribute key="maxHeapSize" value="25"/>
     <stringAttribute key="modelBehaviorInit" value=""/>
     <stringAttribute key="modelBehaviorNext" value=""/>
@@ -13,8 +13,10 @@
     <intAttribute key="modelBehaviorSpecType" value="1"/>
     <stringAttribute key="modelBehaviorVars" value="msgs, depth, parent"/>
     <stringAttribute key="modelComments" value=""/>
-    <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
-    <listAttribute key="modelCorrectnessInvariants"/>
+    <booleanAttribute key="modelCorrectnessCheckDeadlock" value="false"/>
+    <listAttribute key="modelCorrectnessInvariants">
+        <listEntry value="1TypeOK"/>
+    </listAttribute>
     <listAttribute key="modelCorrectnessProperties">
         <listEntry value="1&lt;&gt;Terminated"/>
     </listAttribute>