.

Route.tla

@@ -138,17 +138,23 @@ Spec == /\ Init /\ [][Next]_vars
 
 Terminated == \A q \in Queues : msgs[q] = << >>
 
+\* SeqDecreasing is true if S is sequence with decreasing elements
 RECURSIVE SeqDecreasing(_)
 SeqDecreasing(S) ==
         CASE S = << >>  -> TRUE
           [] Len(S) = 1 -> TRUE
-          [] OTHER      -> (S[1] >= S[2])  /\  SeqDecreasing(Tail(S))
+          [] OTHER      -> (S[2] =< S[1])  /\  SeqDecreasing(Tail(S))
+
+\* SeqSet converts sequence S to set of its values.
+SeqSet(S) == {S[x]: x \in DOMAIN 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])
+        /\ \A q \in Queues :
+                /\ SeqDecreasing(msgs[q])
+                /\ \A d \in SeqSet(msgs[q]) : d >= depth[q[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="124"/>
+    <intAttribute key="fpIndex" value="115"/>
     <intAttribute key="maxHeapSize" value="25"/>
     <stringAttribute key="modelBehaviorInit" value=""/>
     <stringAttribute key="modelBehaviorNext" value=""/>