.

Route.tla

@@ -135,6 +135,9 @@ Spec == /\ Init /\ [][Next]_vars
 
 \* END TRANSLATION
 
+
+Terminated == \A q \in Queues : msgs[q] = << >>
+
 (*
 TypeOK ==
         /\ depth \in [Nodes -> Nat]

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="93"/>
+    <intAttribute key="fpIndex" value="88"/>
     <intAttribute key="maxHeapSize" value="25"/>
     <stringAttribute key="modelBehaviorInit" value=""/>
     <stringAttribute key="modelBehaviorNext" value=""/>
@@ -15,7 +15,9 @@
     <stringAttribute key="modelComments" value=""/>
     <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
     <listAttribute key="modelCorrectnessInvariants"/>
-    <listAttribute key="modelCorrectnessProperties"/>
+    <listAttribute key="modelCorrectnessProperties">
+        <listEntry value="1&lt;&gt;Terminated"/>
+    </listAttribute>
     <intAttribute key="modelEditorOpenTabs" value="8"/>
     <stringAttribute key="modelExpressionEval" value=""/>
     <listAttribute key="modelParameterConstants">