.

Route.tla

+------------------------------- MODULE Route -------------------------------
+EXTENDS FiniteSets
+
+CONSTANT Nodes, Edges, root
+
+\* Has2Items(e) is true when e is set with exactly 2 elements.
+\*Has2Items(s) == \E a, b \in s : (a /= b) /\ (s = {a,b})
+\*Has2Items(s) == Cardinality(s) = 2
+
+
+ASSUME /\ root \in Nodes
+       /\ \A e \in Edges : (e \subseteq Nodes) /\ (Cardinality(e) = 2)
+
+
+\* Connected is true if two nodes i and j are interconnected by some path.
+RECURSIVE Connected(_,_)
+Connected(i,j) ==
+        \/ {i,j} \in Edges
+        \/ \E x \in Nodes : ({i,x} \in Edges) /\ Connected(x,j)
+
+\* All nodes must be connected
+ASSUME \A i,j \in Nodes : Connected(i,j)
+
+
+=============================================================================

Route.toolbox/.project

+<?xml version="1.0" encoding="UTF-8"?>
+<projectDescription>
+	<name>Route</name>
+	<comment></comment>
+	<projects>
+	</projects>
+	<buildSpec>
+		<buildCommand>
+			<name>toolbox.builder.TLAParserBuilder</name>
+			<arguments>
+			</arguments>
+		</buildCommand>
+	</buildSpec>
+	<natures>
+		<nature>toolbox.natures.TLANature</nature>
+	</natures>
+	<linkedResources>
+		<link>
+			<name>Route.tla</name>
+			<type>1</type>
+			<locationURI>PARENT-1-PROJECT_LOC/Route.tla</locationURI>
+		</link>
+	</linkedResources>
+</projectDescription>

Route.toolbox/.settings/org.lamport.tla.toolbox.prefs

+ProjectRootFile=PARENT-1-PROJECT_LOC/Route.tla
+eclipse.preferences.version=1

Route.toolbox/Route___Model_1.launch

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
+    <stringAttribute key="configurationName" value="Model_1"/>
+    <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="62"/>
+    <intAttribute key="maxHeapSize" value="25"/>
+    <stringAttribute key="modelBehaviorInit" value=""/>
+    <stringAttribute key="modelBehaviorNext" value=""/>
+    <stringAttribute key="modelBehaviorSpec" value=""/>
+    <intAttribute key="modelBehaviorSpecType" value="0"/>
+    <stringAttribute key="modelBehaviorVars" value=""/>
+    <stringAttribute key="modelComments" value=""/>
+    <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
+    <listAttribute key="modelCorrectnessInvariants"/>
+    <listAttribute key="modelCorrectnessProperties"/>
+    <intAttribute key="modelEditorOpenTabs" value="8"/>
+    <stringAttribute key="modelExpressionEval" value=""/>
+    <listAttribute key="modelParameterConstants">
+        <listEntry value="root;;n1;0;0"/>
+        <listEntry value="Edges;;{{n1, n2}};0;0"/>
+        <listEntry value="Nodes;;{n1, n2, n3};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"/>
+</launchConfiguration>