.

Route.tla

@@ -138,10 +138,17 @@ Spec == /\ Init /\ [][Next]_vars
 
 Terminated == \A q \in Queues : msgs[q] = << >>
 
+RECURSIVE SeqDecreasing(_)
+SeqDecreasing(S) ==
+        CASE S = << >>  -> TRUE
+          [] Len(S) = 1 -> TRUE
+          [] OTHER      -> (S[1] >= S[2])  /\  SeqDecreasing(Tail(S))
+
 TypeOK ==
         /\ depth \in [Nodes -> 0..Cardinality(Nodes) \cup {Inf}]
         /\ parent \in [Nodes -> Nodes \cup {NoRoute}]
         /\ msgs \in [Queues -> Seq(0..(Cardinality(Nodes)-1))]
+        /\ \A q \in Queues : SeqDecreasing(msgs[q])
 
 
 \* 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="12"/>
+    <intAttribute key="fpIndex" value="124"/>
     <intAttribute key="maxHeapSize" value="25"/>
     <stringAttribute key="modelBehaviorInit" value=""/>
     <stringAttribute key="modelBehaviorNext" value=""/>