Add rsp-tree algo but kind2 isn't working and with weight at 1 and reply manually enter (tree4.lus)

test/rsp_tree/Makefile

+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

test/rsp_tree/config.ml

+(* 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 *)

test/rsp_tree/p.lus

+-----------------------------------------------------------------
+--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;

test/rsp_tree/p.ml

+../../../test/rsp-tree/p.ml
\ No newline at end of file

test/rsp_tree/root.lus

+-------------------------------------------------------
+--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

test/rsp_tree/root.ml

+../../../test/rsp-tree/root.ml
\ No newline at end of file

test/rsp_tree/rsp_tree_oracle.lus

+
+-- 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

test/rsp_tree/state.ml

+../../../test/rsp-tree/state.ml
\ No newline at end of file

test/rsp_tree/tree4.lus

+-- 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;

test/rsp_tree/tree4_oracle.lus

+-- 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

test/rsp_tree/verify.lus

+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