diff --git a/test/rsp_tree/Makefile b/test/rsp_tree/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..0210a79a0d95b9f462938e956062af9d42f42952
--- /dev/null
+++ b/test/rsp_tree/Makefile
@@ -0,0 +1,27 @@
+TOPOLOGY ?= tree4
+DOT2LUSFLAGS ?=
+SASA_ALGOS := p.ml root.ml
+DECO_PATTERN="0:root.ml 1-:p.ml"
+
+
+include ../Makefile.inc
+-include ../Makefile.dot
+
+clean: genclean
+ rm -f
+
+## Some examples of use of ../Makefile.inc
+
+
+# run a simulation with luciole
+simu: $(TOPOLOGY).simu
+
+# Compare the ocaml version with the lustre one
+compare: $(TOPOLOGY).lurette
+ cat rsp_tree.rif
+
+# make diring4.simu
+kind2: $(TOPOLOGY).kind2
+
+## do not work because there is a modulo in p.lus, which is not (yet) implemented in ../../bit-blast/*.lus
+lesar: $(TOPOLOGY).lesar
diff --git a/test/rsp_tree/config.ml b/test/rsp_tree/config.ml
new file mode 100644
index 0000000000000000000000000000000000000000..494fdf2e9e9ea8cda840c0bfa9dcfbe65b216ad7
--- /dev/null
+++ b/test/rsp_tree/config.ml
@@ -0,0 +1,9 @@
+(* Automatically generated by /home/emile/.opam/4.12.0/bin/sasa version "v4.6.1" ("c3dfe95")*)
+(* on PC-Travail the 20/6/2022 at 14:52:03*)
+(*sasa -reg tree4.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 *)
+let init_search_utils = None (* To provide to use --init-search *)
diff --git a/test/rsp_tree/p.lus b/test/rsp_tree/p.lus
new file mode 100644
index 0000000000000000000000000000000000000000..660bcc314f82df2cba44aeb9063c6d9128d8a08d
--- /dev/null
+++ b/test/rsp_tree/p.lus
@@ -0,0 +1,147 @@
+-----------------------------------------------------------------
+--Get parent function:
+function parent<<const n:int; const count:int>>(this : state; neighbors : state^n)
+returns (res : state);
+let
+ res = if (n<=this.par) then neighbors[n-1]
+ else with (count = n ) then neighbors[n-1]
+ else if (count = this.par) then neighbors[count] else parent<<n,(count+1)>>(this,neighbors);
+tel;
+
+------------------------------------------------------------------
+--Reply function:
+function reply<<const n:int>>(v:state; neighbors: state^n; reply_l:int^n)
+returns (res : int);
+let
+ res = with (n=1) then reply_l[0] else
+ if (v = neighbors[0]) then reply_l[0] else reply<<n-1>>(v,neighbors[1..n-1],reply_l[1..n-1]);
+tel;
+
+------------------------------------------------------------------
+--Predicates:
+function children<<const n:int>>(u:state; neighbors:state^n; reply_l:int^n)
+returns ( res : bool^n );
+var v:state;
+let
+ v = neighbors[0];
+ res = with (n=1) then [ ((u.st <> I) and
+ (v.st <> I) and
+ (reply<<n>>(v,neighbors,reply_l) = v.par) and
+ (v.d >= u.d + 1) and
+ ((v.st = u.st) or (u.st = EB))) ]
+ else [ ((u.st <> I) and
+ (v.st <> I) and
+ (reply<<n>>(v,neighbors,reply_l) = v.par) and
+ (v.d >= u.d + 1) and
+ ((v.st = u.st) or (u.st = EB))) ] | children<<n-1>>(u,neighbors[1..n-1],reply_l[1..n-1]);
+tel;
+
+function abRoot<<const n:int>>(this : state; neighbors : state^n)
+returns(res : bool);
+var par_u: state;
+let
+ par_u= parent<<n,0>>(this, neighbors);
+ res = (this.st <> I) and ( (this.par > n) or
+ (par_u.st = I) or
+ (this.d < (par_u.d + (1))) or
+ (this.st <> par_u.st and par_u.st <> EB));
+tel;
+
+function p_reset<<const n:int>>(this : state; neighbors: state^n)
+returns (res : bool);
+let
+ res = ( (this.st = EF) and (abRoot<<n>>(this,neighbors)) );
+tel;
+
+function condition(elem:state; this:state) returns(res : bool);
+let
+ res = (elem.st = C) and (elem.d + 1 < this.d);
+tel;
+
+function p_correction<<const n:int>>(this : state; neighbors : state^n)
+returns(res : bool);
+let
+ res = n_or<<n>>(map<<condition,n>>(neighbors,(this^n)));
+tel;
+
+---------------------------------------------------------------------
+--Macro:
+function argmin<<const n:int; const count:int; const indice:int>>(min:state; nl : state^n)
+returns(res : int);
+let
+ res = with ( n = 1) then (if nl[0].st = C and min.st = C then
+ if (nl[0].d + 1) <= (min.d + 1) then count else indice
+ else if nl[0].st = C then count else indice)
+ else (if nl[0].st = C and min.st = C then
+ if (nl[0].d + 1) <= (min.d + 1) then argmin<<n-1,count+1,count>>(nl[0],nl[1..n-1])
+ else argmin<<n-1,count+1,indice>>(min,nl[1..n-1])
+ else
+ argmin<<n-1,count+1,count>>(nl[0],nl[1..n-1])
+ );
+tel;
+
+function computePath<<const n:int>>(this : state ; neighbors : state^n)
+returns(res : state);
+var par_u:state;
+let
+ par_u = parent<<n,0>>(this,neighbors);
+ res = state { st = C;
+ par = argmin<<n,0,-1>>((state { st=EB; par=-1; d=-1 }), neighbors);
+ d = (par_u.d + 1); };
+tel;
+
+---------------------------------------------------------------------
+--Enable Macro function:
+function for_all<<const n:int>>(neigh_list: state^n; bool_list: bool^n)
+returns (res : bool);
+let
+ res = with (n = 1) then (if bool_list[0] = true
+ then neigh_list[0].st = EF
+ else true)
+ else (if bool_list[0] = true
+ then (neigh_list[0].st = EF) and (for_all<<n-1>>(neigh_list[1 .. n-1], bool_list[1 .. n-1]))
+ else (for_all<<n-1>>(neigh_list[1 .. n-1], bool_list[1 .. n-1])));
+tel;
+
+function not_equal_c (elem:state)
+returns (res : bool);
+let
+ res = (elem.st<>C);
+tel;
+
+function equal_c (elem:state)
+returns (res : bool);
+let
+ res = (elem.st=C);
+tel;
+--------------------------------------------------------------------
+--Step and Enable functions:
+function p_enable<<const degree:int>>(this : state; neighbors : state^degree; reply_l: int^degree)
+returns (enabled : bool^actions_number);
+var
+ par_u:state;
+ bool_list:bool^degree;
+let
+ par_u = parent<<degree,0>>(this, neighbors);
+ bool_list = children<<degree>>(this, neighbors, reply_l);
+ enabled = [ ((this.st = C) and p_correction<<degree>>(this,neighbors)),
+ ((this.st = C) and (not (p_correction<<degree>>(this,neighbors))) and ((abRoot<<degree>>(this,neighbors)) or (par_u.st = EB))),
+ ((this.st = EB) and (for_all<<degree>>(neighbors, bool_list))),
+ ((p_reset<<degree>>(this, neighbors)) and boolred<<degree,degree,degree>>(map<< not_equal_c , degree>>(neighbors))),
+ (((p_reset<<degree>>(this,neighbors)) or this.st = I) and (boolred<<1,degree,degree>>(map<< equal_c , degree>>(neighbors))))
+ ];
+tel;
+
+function p_step<<const degree:int>>(
+ this : state;
+ neighbors : state^degree;
+ action : action)
+returns (new : state);
+let
+ new = if (action = Rc) then computePath<<degree>>(this, neighbors)
+ else if (action = Reb) then state { st = EB; par = this.par; d = this.d }
+ else if (action = Ref) then state { st = EF; par = this.par; d = this.d }
+ else if (action = Ri) then state { st = I; par = this.par; d = this.d }
+ else if (action = Rr) then computePath<<degree>>(this, neighbors)
+ else this;
+tel;
diff --git a/test/rsp_tree/p.ml b/test/rsp_tree/p.ml
new file mode 120000
index 0000000000000000000000000000000000000000..e13d0969a16d449d2c52597c117fe513d173090e
--- /dev/null
+++ b/test/rsp_tree/p.ml
@@ -0,0 +1 @@
+../../../test/rsp-tree/p.ml
\ No newline at end of file
diff --git a/test/rsp_tree/root.lus b/test/rsp_tree/root.lus
new file mode 100644
index 0000000000000000000000000000000000000000..cfece2221e7496b34ceb13dd0be0161c342f8827
--- /dev/null
+++ b/test/rsp_tree/root.lus
@@ -0,0 +1,33 @@
+-------------------------------------------------------
+--Settings:
+type status = enum { I, C, EB, EF };
+type state = struct { st:status; par:int; d:int };
+
+type action = enum { Rc,Reb,Ref,Ri,Rr };
+const actions_number = 5;
+
+function action_of_int(i : int ) returns (a : action);
+let
+ a = if i = 0 then Rc
+ else if i = 1 then Reb
+ else if i = 2 then Ref
+ else if i = 3 then Ri
+ else Rr;
+tel;
+
+-------------------------------------------------------
+--Step and Enable functions(for root):
+function root_enable<<const degree:int>>(this : state; neighbors : state^degree)
+returns (enabled : bool^actions_number);
+let
+ enabled = [ false, false, false, false, false ] ;
+tel;
+
+function root_step<<const degree:int>>(
+ this : state;
+ neighbors : state^degree;
+ action : action)
+returns (new : state);
+let
+ new = state { st=C; par=-1; d=0 };
+tel;
\ No newline at end of file
diff --git a/test/rsp_tree/root.ml b/test/rsp_tree/root.ml
new file mode 120000
index 0000000000000000000000000000000000000000..086c6666a388c7aa7ba8e824a16e6e6367017bbf
--- /dev/null
+++ b/test/rsp_tree/root.ml
@@ -0,0 +1 @@
+../../../test/rsp-tree/root.ml
\ No newline at end of file
diff --git a/test/rsp_tree/rsp_tree_oracle.lus b/test/rsp_tree/rsp_tree_oracle.lus
new file mode 100644
index 0000000000000000000000000000000000000000..7033662016cee16998e8e9885a4de1e3fa4d5964
--- /dev/null
+++ b/test/rsp_tree/rsp_tree_oracle.lus
@@ -0,0 +1,25 @@
+
+-- Here, we use the Lustre version of the algorithm as an oracle for the ocaml version
+
+include "../../lib/utils.lus"
+
+node rsp_tree_oracle(
+ legitimate : bool;
+ ocaml_enabled : bool^actions_number^card;
+ active : bool^actions_number^card;
+ ocaml_config : state^card;
+)
+returns (ok : bool; lustre_config : state^card;
+ lustre_enabled : bool^actions_number^card;);
+-- var
+
+let
+ lustre_config, lustre_enabled =
+ topology(active -> pre active, -- ignored at the first step
+ ocaml_config -- used at the first step only
+ );
+ ok = lustre_enabled = ocaml_enabled
+ -- compare the sasa dot interpretation and the salut dot to lustre compilation
+ and lustre_config = ocaml_config;
+ -- compare the lustre and the ocaml version of the processes
+tel
diff --git a/test/rsp_tree/state.ml b/test/rsp_tree/state.ml
new file mode 120000
index 0000000000000000000000000000000000000000..ac63100f73e5f8bcf1a59ba9a370819938e57871
--- /dev/null
+++ b/test/rsp_tree/state.ml
@@ -0,0 +1 @@
+../../../test/rsp-tree/state.ml
\ No newline at end of file
diff --git a/test/rsp_tree/tree4.lus b/test/rsp_tree/tree4.lus
new file mode 100644
index 0000000000000000000000000000000000000000..cee55d5150e7f4594fa41aa2f324b822f0f49aaa
--- /dev/null
+++ b/test/rsp_tree/tree4.lus
@@ -0,0 +1,77 @@
+-- automatically generated by salut
+include "p.lus"
+include "root.lus"
+
+
+function dot2lus_first_set<<const N:int>>(s : bool^N) returns (x : int);
+var
+ found : int;
+let
+ found =
+ with (N = 1) then (if s[0] then 0 else -1)
+ else dot2lus_first_set<<N-1>>(s[1 .. N-1]);
+ x =
+ if s[0] then 0
+ else if found < 0 then -1
+ else found + 1;
+tel;
+
+function dot2lus_action_of_activation(activation : bool^actions_number) returns (action : action);
+let
+ action = action_of_int(dot2lus_first_set<<actions_number>>(activation));
+tel;
+
+node tree4(p : bool^actions_number^card; initials : state^card)
+returns (p_c : state^card; Enab_p : bool^actions_number^card);
+var
+ prev_p_c : state^card;
+
+ sel_0 : bool;
+ sel_1 : bool;
+ sel_2 : bool;
+ sel_3 : bool;
+let
+ prev_p_c = initials -> pre(p_c);
+
+ sel_0 = false -> boolred<<1,actions_number,actions_number>>(p[0]);
+ sel_1 = false -> boolred<<1,actions_number,actions_number>>(p[1]);
+ sel_2 = false -> boolred<<1,actions_number,actions_number>>(p[2]);
+ sel_3 = false -> boolred<<1,actions_number,actions_number>>(p[3]);
+
+ p_c[0] =
+ if not sel_0 then prev_p_c[0]
+ else root_step<<2>>(
+ prev_p_c[0],
+ [ prev_p_c[1], prev_p_c[2] ],
+ dot2lus_action_of_activation(p[0])
+ );
+ Enab_p[0] = root_enable<<2>>(p_c[0], [ p_c[1], p_c[2] ]);
+
+ p_c[1] =
+ if not sel_1 then prev_p_c[1]
+ else p_step<<2>>(
+ prev_p_c[1],
+ [ prev_p_c[0], prev_p_c[3] ],
+ dot2lus_action_of_activation(p[1])
+ );
+ Enab_p[1] = p_enable<<2>>(p_c[1], [ p_c[0], p_c[3] ], [0,0]);
+
+ p_c[2] =
+ if not sel_2 then prev_p_c[2]
+ else p_step<<1>>(
+ prev_p_c[2],
+ [ prev_p_c[0] ],
+ dot2lus_action_of_activation(p[2])
+ );
+ Enab_p[2] = p_enable<<1>>(p_c[2], [ p_c[0] ],[1]);
+
+ p_c[3] =
+ if not sel_3 then prev_p_c[3]
+ else p_step<<1>>(
+ prev_p_c[3],
+ [ prev_p_c[1] ],
+ dot2lus_action_of_activation(p[3])
+ );
+ Enab_p[3] = p_enable<<1>>(p_c[3], [ p_c[1] ],[1]);
+tel;
+node topology = tree4;
diff --git a/test/rsp_tree/tree4_oracle.lus b/test/rsp_tree/tree4_oracle.lus
new file mode 100644
index 0000000000000000000000000000000000000000..deb6b80e61dc3a1f1cb22b8ed13466dd2bd70925
--- /dev/null
+++ b/test/rsp_tree/tree4_oracle.lus
@@ -0,0 +1,51 @@
+-- Automatically generated by /home/emile/.opam/4.12.0/bin/sasa version "v4.6.1" ("c3dfe95")
+-- on PC-Travail the 20/6/2022 at 14:52:03
+--sasa -glos tree4.dot
+
+include "rsp_tree_oracle.lus"
+const an=5; -- actions number
+const pn=4; -- processes number
+const degree=2;
+const min_degree=1;
+const mean_degree=1.500000;
+const diameter=3;
+const card=4;
+const links_number=3;
+const is_cyclic=false;
+const is_connected=true;
+const is_a_tree=true;
+const f=false;
+const t=true;
+const adjacency=[
+ [f,t,t,f],
+ [t,f,f,t],
+ [t,f,f,f],
+ [f,t,f,f]];
+const mean_deg=1.5;
+const max_deg=2;
+const is_tree=true;
+const is_rooted=false;
+const min_deg=1;
+
+node oracle(legitimate:bool;
+ Root_d:int;Root_par:int;Root_st:status;p1_d:int;p1_par:int;p1_st:status;p2_d:int;p2_par:int;p2_st:status;p3_d:int;p3_par:int;p3_st:status;
+ Enab_Root_Rcu,Enab_Root_Rebu,Enab_Root_Refu,Enab_Root_Riu,Enab_Root_Rru,Enab_p1_Rcu,Enab_p1_Rebu,Enab_p1_Refu,Enab_p1_Riu,Enab_p1_Rru,Enab_p2_Rcu,Enab_p2_Rebu,Enab_p2_Refu,Enab_p2_Riu,Enab_p2_Rru,Enab_p3_Rcu,Enab_p3_Rebu,Enab_p3_Refu,Enab_p3_Riu,Enab_p3_Rru:bool;
+ Root_Rcu,Root_Rebu,Root_Refu,Root_Riu,Root_Rru,p1_Rcu,p1_Rebu,p1_Refu,p1_Riu,p1_Rru,p2_Rcu,p2_Rebu,p2_Refu,p2_Riu,p2_Rru,p3_Rcu,p3_Rebu,p3_Refu,p3_Riu,p3_Rru:bool)
+returns (ok:bool; lustre_config:state^4; lustre_enab:bool^an^pn);
+var
+ Acti:bool^an^pn;
+ Enab:bool^an^pn;
+ Config:state^4;
+ a,b,c,d:state;
+let
+ Acti = [[Root_Rcu,Root_Rebu,Root_Refu,Root_Riu,Root_Rru],[p1_Rcu,p1_Rebu,p1_Refu,p1_Riu,p1_Rru],[p2_Rcu,p2_Rebu,p2_Refu,p2_Riu,p2_Rru],[p3_Rcu,p3_Rebu,p3_Refu,p3_Riu,p3_Rru]];
+ Enab = [[Enab_Root_Rcu,Enab_Root_Rebu,Enab_Root_Refu,Enab_Root_Riu,Enab_Root_Rru],[Enab_p1_Rcu,Enab_p1_Rebu,Enab_p1_Refu,Enab_p1_Riu,Enab_p1_Rru],[Enab_p2_Rcu,Enab_p2_Rebu,Enab_p2_Refu,Enab_p2_Riu,Enab_p2_Rru],[Enab_p3_Rcu,Enab_p3_Rebu,Enab_p3_Refu,Enab_p3_Riu,Enab_p3_Rru]];
+ a=state { d=Root_d; par=Root_par; st=Root_st };
+ b=state { d=p1_d; par=p1_par; st=p1_st };
+ c=state { d=p2_d; par=p2_par; st=p2_st };
+ d=state { d=p3_d; par=p3_par; st=p3_st };
+ Config = [a,b,c,d];
+
+ ok,lustre_config, lustre_enab = rsp_tree_oracle(legitimate, Enab, Acti, Config);
+tel
+node to_state(int,int,int) returns (res:status);
\ No newline at end of file
diff --git a/test/rsp_tree/verify.lus b/test/rsp_tree/verify.lus
new file mode 100644
index 0000000000000000000000000000000000000000..afb12854e8a17ff37d6e281120bc2e6b6762ec7b
--- /dev/null
+++ b/test/rsp_tree/verify.lus
@@ -0,0 +1,50 @@
+include "../../lib/sas.lus"
+
+node verify(activations : bool^actions_number^card; inits : state^card) returns (ok : bool);
+var
+ config : state^card;
+ enables : bool^actions_number^card;
+ legitimate, closure, Round : bool;
+ RoundNb : int;
+let
+-- assert(true -> daemon_is_locally_central<<actions_number,card>>(activations, pre enables, adjacency));
+ assert(true -> daemon_is_central<<actions_number,card>>(activations, pre enables));
+ assert(rangei<<0,card>>(inits));
+
+ config, enables = topology(activations, inits);
+
+ legitimate = silent<<actions_number,card>>(enables);
+ closure = true -> (pre(legitimate) => legitimate);
+ Round = round <<actions_number,card>>(enables,activations);
+ RoundNb = round_count(Round, legitimate);
+
+ -- verify that the execution terminates after at most |N|−1 moves:
+ ok = closure
+ and ( not(legitimate) and is_connected => (RoundNb < 3*card+diameter) )
+;
+tel;
+
+----------------------------------------------------------------------------
+function lower_or_egal(x:state; y:state)
+returns(res : bool);
+let
+ res = (x.d <= y.d) and (x.par <= y.d);
+tel;
+
+function lower(x:state; y:state)
+returns(res : bool);
+let
+ res = (x.d < y.d) and (x.par < y.d);
+tel;
+
+-- all states are initially in [0; card|[
+node rangei<<const low:int; const card:int>>(c:state^card) returns (res:bool);
+var
+ ranges_min, ranges_max : bool^card;
+const low_state = state { d = low; par = low; st = I};
+const card_state = state { d = card; par = card; st = EF };
+let
+ ranges_min = map<< lower_or_egal , card>>(low_state^card, c);
+ ranges_max = map<< lower , card>>(c, card_state^card);
+ res = boolall<<card>>(ranges_min) and boolall<<card>>(ranges_max);
+tel