.

Route.tla

@@ -139,9 +139,9 @@ Spec == /\ Init /\ [][Next]_vars
 Terminated == \A q \in Queues : msgs[q] = << >>
 
 TypeOK ==
-        /\ depth \in [Nodes -> Nat \cup {Inf}]
+        /\ depth \in [Nodes -> 0..Cardinality(Nodes) \cup {Inf}]
         /\ parent \in [Nodes -> Nodes \cup {NoRoute}]
-        /\ msgs \in [Queues -> Seq(Nat)]
+        /\ msgs \in [Queues -> Seq(0..(Cardinality(Nodes)-1))]
 
 
 \* ParentPath returns path from node n to root constructed via parents.

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="97"/>
+    <intAttribute key="fpIndex" value="12"/>
     <intAttribute key="maxHeapSize" value="25"/>
     <stringAttribute key="modelBehaviorInit" value=""/>
     <stringAttribute key="modelBehaviorNext" value=""/>