.

Route.tla

@@ -15,7 +15,8 @@ ASSUME /\ root \in Nodes
 \* Connected is true if two nodes i and j are interconnected by some path.
 RECURSIVE _Connected(_,_,_)
 _Connected(i,j,Intra) ==
-        CASE {i,j} \in Edges -> TRUE
+        CASE i = j           -> TRUE
+          [] {i,j} \in Edges -> TRUE
           [] Intra = {}      -> FALSE
           [] OTHER           -> \E x \in Intra : ({i,x} \in Edges) /\ _Connected(x,j, Intra\{x})
 

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="72"/>
+    <intAttribute key="fpIndex" value="105"/>
     <intAttribute key="maxHeapSize" value="25"/>
     <stringAttribute key="modelBehaviorInit" value=""/>
     <stringAttribute key="modelBehaviorNext" value=""/>