.

Route.toolbox/Route___Model_3.launch

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
+    <stringAttribute key="configurationName" value="Model_3"/>
+    <intAttribute key="distributedFPSetCount" value="0"/>
+    <stringAttribute key="distributedNetworkInterface" value="192.168.122.1"/>
+    <intAttribute key="distributedNodesCount" value="1"/>
+    <stringAttribute key="distributedTLC" value="off"/>
+    <intAttribute key="fpIndex" value="74"/>
+    <intAttribute key="maxHeapSize" value="25"/>
+    <stringAttribute key="modelBehaviorInit" value=""/>
+    <stringAttribute key="modelBehaviorNext" value=""/>
+    <stringAttribute key="modelBehaviorSpec" value="Spec"/>
+    <intAttribute key="modelBehaviorSpecType" value="1"/>
+    <stringAttribute key="modelBehaviorVars" value="msgs, depth, parent"/>
+    <stringAttribute key="modelComments" value=""/>
+    <booleanAttribute key="modelCorrectnessCheckDeadlock" value="false"/>
+    <listAttribute key="modelCorrectnessInvariants">
+        <listEntry value="1TypeOK"/>
+        <listEntry value="1Terminated =&gt; PathsOK"/>
+        <listEntry value="1Inv"/>
+    </listAttribute>
+    <listAttribute key="modelCorrectnessProperties">
+        <listEntry value="1&lt;&gt;Terminated"/>
+    </listAttribute>
+    <intAttribute key="modelEditorOpenTabs" value="8"/>
+    <stringAttribute key="modelExpressionEval" value=""/>
+    <listAttribute key="modelParameterConstants">
+        <listEntry value="root;;r;0;0"/>
+        <listEntry value="Edges;;{{r,n1}, {r,n2}, {n1,n2}};0;0"/>
+        <listEntry value="Nodes;;{r, n1, n2};1;0"/>
+        <listEntry value="NoRoute;;NoRoute;1;0"/>
+        <listEntry value="Inf;;Inf;1;0"/>
+    </listAttribute>
+    <intAttribute key="modelVersion" value="20191005"/>
+    <intAttribute key="numberOfWorkers" value="2"/>
+    <stringAttribute key="result.mail.address" value=""/>
+    <stringAttribute key="specName" value="Route"/>
+    <stringAttribute key="tlcResourcesProfile" value="local custom"/>
+    <listAttribute key="traceExploreExpressions">
+        <listEntry value="1Terminated"/>
+        <listEntry value="1[ n \in Nodes |-&gt; ParentPath(n) ]"/>
+        <listEntry value="1[ n \in Nodes |-&gt; LET p == ParentPath(n) IN &lt;&lt; PathCorrect(p), PathMinimal(p) &gt;&gt; ]"/>
+        <listEntry value="0[ n \in Nodes |-&gt; PathCorrect(ParentPath(n)) ]"/>
+        <listEntry value="0[ n \in Nodes |-&gt; PathMinimal(ParentPath(n)) ]"/>
+        <listEntry value="1[ n \in Nodes |-&gt; LET p == ParentPath(n) IN p[1] = n /\ p[Len(p)] = root]"/>
+        <listEntry value="1PathsOK"/>
+        <listEntry value="1[ n \in Nodes |-&gt; Dist(n, root) ]"/>
+    </listAttribute>
+</launchConfiguration>