test: add yet another example in the test directory

(disconnect component detection)

test/Makefile

@@ -13,6 +13,7 @@ test:
 	cd st-KK06-algo1/ && make 
 	cd st-KK06-algo2/ && make 
 	cd bfs-st-HC92/ && make 
+	cd rsp-tree/ && make 
 	echo "Every test went fine!"
 
 clean:
@@ -32,5 +33,6 @@ clean:
 	cd st-KK06-algo1/ && make  clean
 	cd st-KK06-algo2/ && make  clean
 	cd bfs-st-HC92/ && make clean
+	cd rsp-tree/ && make clean
 
 -include Makefile.untracked

test/README.org

@@ -30,8 +30,13 @@ literature:
    Tree in a Polynomial Number of Moves" by Kosowski and Kuszner, 2006)
 4. =test/dfs/=: a Depth  First Search using arrays  (the ``atomic state
    model'' version of a [[http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.57.1100&rep=rep1&type=pdf][Depth First Search algorithm proposed by Collin and Dolev in 1994]])
-5.  =test/dfs-list/=:  the same  Depth First  Search, but  using lists
-   instead or arrays
+5. =test/dfs-list/=:  the same  Depth First  Search, but  using lists
+  instead or arrays
+6. =test/rsp-tree/=: The Algorithm 1 of "Self-Stabilizing Disconnected
+   Components Detection  and Rooted Shortest-Path Tree  Maintenance in
+   Polynomial  Steps" by  Stéphane Devismes,  David Ilcinkas,  Colette
+   Johnen.
+
 
 Each directories contains working examples, which are checked using the
 Continuous  Integration facilities  of Gitlab  (cf the  [[https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/.gitlab-ci.yml][.gitlab-ci.yml]]

test/rsp-tree/Makefile

+# Time-stamp: <modified the 04/11/2020 (at 08:43) by Erwan Jahier>
+
+
+test: grid4.test er30.test udg100.test ba100.test
+
+DECO_PATTERN="0:root.ml 1-:p.ml" 
+-include ../Makefile.dot
+
+rdbg: er100.rdbg
+
+%.lurette: %.dot %.cmxs %_oracle.lus rsp_tree_oracle.lus
+	lurette -sut "sasa $< -dd"  -oracle "lv6 -2c-exec $*_oracle.lus -n oracle"
+
+%.lurette2: %.dot %.cmxs %_oracle.lus rsp_tree_oracle.lus
+	lurette -sut "sasa $< -dd"  -oracle "lv6 $*_oracle.lus -n oracle"
+
+
+clean: genclean cleandot
+
+-include ../Makefile.inc
+

test/rsp-tree/config.ml

+(* Automatically generated by /home/jahier/.opam/4.10.0/bin/sasa version "4.3.5" ("a6897fa")*)
+(* on crevetete the 4/11/2020 at 8:39:07*)
+(*sasa -reg grid4.dot*)
+
+
+let potential = None (* None => only -sd, -cd, -lcd, -dd, or -custd are possible *)
+let legitimate = None (* None => only silent configuration are legitimate *)
+let fault = None (* None => the simulation stop once a legitimate configuration is reached *)

test/rsp-tree/p.ml

+(* Time-stamp: <modified the 26/03/2020 (at 10:56) by Erwan Jahier> *)
+
+(*  The  Algorithm  1  of  "Self-Stabilizing  Disconnected  Components
+   Detection and  Rooted Shortest-Path Tree Maintenance  in Polynomial
+   Steps" by Stéphane Devismes, David Ilcinkas, Colette Johnen
+
+    https://hal.archives-ouvertes.fr/hal-01485652v4 
+
+    Hyp: 
+    - semi-anonymous network (there is a root + no pid)
+    - indirect naming (Algo.reply is available, but not Algo.spid)
+    - weigthed network (positive integers)
+    - distributed  daemon
+
+*)
+
+open Algo
+open State
+
+let (init_state: int -> string -> 'st) =
+  fun s _ ->
+  if s = 0 then { st=C; par=(-1);d=0 } else
+  {
+    st = (match Random.int 4 with
+        | 0 -> I
+        | 1 -> C 
+        | 2 -> EB
+        | _ -> EF);
+    par = Random.int s;
+    d   = Random.int s
+  }
+  
+(***************************************************************)
+(* Predicates and macros *)
+
+let parent u nl = List.nth nl u.par
+
+(* children(u) = {v ∈ Γ(u) | stu != I ∧ stv != I ∧ parv = u ∧ 
+                              dv ≥ du + ω(v, u) ∧ (stv = stu ∨ stu = EB)}  *)
+
+let (children: t -> t Algo.neighbor list -> t Algo.neighbor list) =
+  fun u nl -> 
+  List.filter
+    (fun v -> u.st <> I && (state v).st <> I &&
+              (state v).par = reply v &&
+              (state v).d >= u.d + weight v &&
+              ((state v).st = u.st || u.st = EB))
+    nl
+
+(*  abRoot(u) ≡ stu != I ∧ 
+         [paru not_in Γ(u) ∨ stparu = I ∨ 
+          du < dparu + ω(u, paru ) ∨ (stu != stparu ∧ stparu != EB) ]
+*)
+let abRoot u nl =
+  let paru = parent u nl in
+  let stparu = (state paru).st in
+  let dparu = (state paru).d in
+  u.st <> I && (
+    (u.par > List.length nl)  ||
+    stparu = I ||
+    u.d < dparu + weight paru ||
+    (u.st <> stparu && stparu <> EB)
+  )
+ 
+(*  p_reset(u) ≡  stu = EF ∧ abRoot(u) *)
+let p_reset u nl = u.st = EF && abRoot u nl
+  
+(*  P_correction(u) ≡  (∃v ∈ Γ(u) | stv = C ∧ dv + ω(u, v) < du ) *)
+let p_correction u nl =
+  List.exists (fun v -> (state v).st = C && (state v).d + weight v < u.d) nl 
+
+
+let min1 (d1,u) (d2,v) = if d1 < d2 then (d1,u) else (d2,v)
+let minimum l =
+  match l with
+  | [] -> assert false
+  | x::t -> List.fold_left min1 x t
+
+(*  computePath(u) : paru := argmin_{v∈Γ(u)∧stv =C} (dv + ω(u, v)); 
+                     du := dparu + ω(u, paru ); 
+                     stu := C *)
+let computePath u nl =
+  let paru = parent u nl in
+  let nli = List.mapi (fun i x -> i,x) nl in
+  let nli_C = List.filter (fun (_,v) -> (state v).st = C) nli in
+  let d_n_l = List.map (fun (i,v) -> (state v).d + weight v, i) nli_C in
+  {
+    st = C ;
+    par = snd (minimum d_n_l);
+    d = (state paru).d + weight paru;
+  }
+  
+(***************************************************************)
+(* Rules
+  
+ RR (u)  : (P_reset(u) ∨ stu = I) ∧ (∃v ∈ Γ(u) | stv = C) → computePath(u)
+ *)
+let (enable_f: 'st -> 'st neighbor list -> action list) =
+  fun u nl ->
+  if nl=[] then [] else
+    let al = if
+      (*  RC (u)  : stu = C ∧ P_correction(u)             → computePath(u) *)
+      u.st = C && p_correction u nl then ["Rc(u)"] else []
+    in
+    let al = if
+      (* REB (u) : stu = C ∧ ¬P_correction(u)∧          → stu := EB
+                  (abRoot(u) ∨ stparu = EB) *)
+      u.st = C && not (p_correction u nl) &&
+      (abRoot u nl || (state (parent u nl)).st = EB)
+    then "Reb(u)"::al else al
+  in
+  let al = if
+    (* REF (u) : stu = EB ∧ (∀v ∈ children(u) | stv = EF )       → stu := EF *)
+    u.st = EB && List.for_all (fun v -> (state v).st = EF) (children u nl)
+    then "Ref(u)"::al else al
+  in
+  let al = if
+    (* RI (u)  : P_reset(u) ∧ (∀v ∈ Γ(u) | stv != C)             → stu := I *)
+    p_reset u nl && List.for_all (fun v -> (state v).st <> C) nl
+    then "Ri(u)"::al else al
+  in
+  let al = if
+    (* RR (u)  : (P_reset(u) ∨ stu = I) ∧ (∃v ∈ Γ(u) | stv = C) → computePath(u)*)
+    (p_reset u nl || u.st = I) && List.exists (fun v -> (state v).st = C) nl
+    then "Rr(u)"::al else al
+  in
+  al
+
+  
+let (step_f : 'st -> 'st neighbor list -> action -> 'st ) =
+  fun u nl ->
+    function
+    | "Rc(u)"  -> computePath u nl
+    | "Reb(u)" -> { u with st = EB }
+    | "Ref(u)" -> { u with st = EF } 
+    | "Ri(u)"  -> { u with st = I  } 
+    | "Rr(u)"  -> computePath u nl
+    | _ -> u

test/rsp-tree/root.ml

+(* Time-stamp: <modified the 06/03/2020 (at 11:13) by Erwan Jahier> *)
+
+open Algo
+open State
+let (init_state: int -> string -> 'st) =
+  fun _ _ ->
+  {
+    st = C;
+    par = -1;
+    d  = 0
+  }
+
+let (enable_f: 'st -> 'st neighbor list -> action list) =
+  fun _e _nl -> []
+        
+  
+let (step_f : 'st -> 'st neighbor list -> action -> 'st ) =
+  fun s _nl _a -> s

test/rsp-tree/rsp_tree_oracle.lus

+include "../lustre/oracle_utils.lus"
+
+type string;
+
+node rsp_tree_oracle(Enab, Acti:bool^an^pn) returns (res:bool);
+var
+  Silent,Round:bool;
+  RoundNb:int;
+let
+  Round = round <<an,pn>>(Enab,Acti);
+  Silent = silent<<an,pn>>(Enab);
+  RoundNb = count(Round); 
+
+  -- Theorem 3 in the case of connected graphs
+  res = (not(Silent) and is_connected) => (RoundNb < 3*card+diameter);
+tel
+  -- end of some_node

test/rsp-tree/state.ml

+
+type status = I | C | EB | EF 
+let status2string = function 
+  | I  -> "I"
+  | C  -> "C"
+  | EB -> "EB"
+  | EF -> "EF"
+    
+type t = {
+  st : status;
+  par : int;
+  d  : int
+}
+let to_string s =
+  Printf.sprintf "st=%s par=%d d=%d" (status2string s.st) s.par s.d
+let of_string = None
+let copy x = x
+let actions = ["Rc(u)"; "Reb(u)"; "Ref(u)"; "Ri(u)";  "Rr(u)"]
+let potential = None
+let legitimate = None
+let fault = None