.

1Bit.tla

@@ -7,15 +7,15 @@ ASSUME N \in Nat
 
 Procs == 0..N
 
-         
+
 
 (********
 --algorithm 1BitProtocol {
     variables flag = [i \in Procs |-> FALSE], turn = 0 ;
     fair process (P \in Procs) {
      ncs:- while (TRUE) {
-            skip ; 
-     enter: flag[self] := TRUE ; 
+            skip ;
+     enter: flag[self] := TRUE ;
         e2: if (flag[1-self]) {
         e3:   if (self /= turn) {
         e4:     flag[self] := FALSE;
@@ -27,7 +27,7 @@ Procs == 0..N
             };
         cs: skip ;
       exit: flag[self] := FALSE ;
-        x2: turn := 1-self;            
+        x2: turn := 1-self;
     }
   }
 }
@@ -108,7 +108,7 @@ ME == INSTANCE MutualExclusionSpec WITH
                 pc <- [proc \in Procs  |->  CASE pc[proc] = "cs"             ->  "cs"
                                               [] pc[proc] \in {"enter","e2","e3","e4","e5"} ->  "csentry"
                                               [] OTHER                       ->  "non-cs"]
-                                              
+
 Live0 == (pc[0] = "enter") ~> (pc[0] = "cs")
 Live1 == (pc[1] = "enter") ~> (pc[1] = "cs")
 

Route.tla

@@ -25,11 +25,63 @@ ASSUME \A i,j \in Nodes : Connected(i,j)
 
 \* ReachableFrom returns set of nodes reachable from nodes in S.
 RECURSIVE ReachableFrom(_)
-ReachableFrom(S) == S \cup ReachableFrom({n \in Nodes : \E x \in S : {x,n} \in Edges})
+ReachableFrom(S) ==
+        LET S_ == S \cup {n \in (Nodes \ S) : \E x \in S : {x,n} \in Edges}
+        IN
+            IF S_ = S THEN S
+                      ELSE ReachableFrom(S_)
+
 
 ASSUME ReachableFrom({root}) = Nodes
 
 
+--------
+
+\* < on Nat \cup {∞}
+CONSTANT Inf    \* = Inf
+m \prec n  ==  IF m = Inf THEN FALSE
+                          ELSE IF n = Inf THEN TRUE ELSE m < n
+
+CONSTANT NoRoute \* = NoRoute
+
+(********
+--algorithm Route {
+  variables depth       \* node -> depth
+                = [[n \in Nodes |-> Inf]  EXCEPT ![root] = 0],
+            parent      \* node -> parent node
+                = [n \in Node |->  IF n = root THEN root ELSE NoRoute];
+  process (RT \in Nodes) {
+    loop: while (TRUE) {
+            skip;
+          }
+  } 
+};
+********)
+\* BEGIN TRANSLATION (chksum(pcal) = "9a717d8a" /\ chksum(tla) = "9b3808dd")
+VARIABLES depth, parent
+
+vars == << depth, parent >>
+
+ProcSet == (Nodes)
+
+Init == (* Global variables *)
+        /\ depth = [[n \in Nodes |-> Inf]  EXCEPT ![root] = 0]
+        /\ parent = [n \in Node |->  IF n = root THEN root ELSE NoRoute]
+
+RT(self) == /\ TRUE
+            /\ UNCHANGED << depth, parent >>
+
+Next == (\E self \in Nodes: RT(self))
+
+Spec == Init /\ [][Next]_vars
+
+\* END TRANSLATION 
+
+(*
+TypeOK ==
+        /\ depth \in [Nodes -> Nat]
+        /\ parent \in [Nodes -> Nodes]
+*)
 
 --------
 

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