add bfs spt

test/bfs-spanning-tree/Makefile

+TOPOLOGY ?= tree3
+DOT2LUSFLAGS ?=
+SASA_ALGOS := p.ml root.ml
+DECO_PATTERN="0:root.ml 1-:p.ml"
+
+
+include  ~/sasa/salut/test/Makefile.inc
+-include ~/sasa/salut/test/Makefile.dot
+
+clean: genclean
+	rm -f tree*.*
+
+## Some examples of use of ../Makefile.inc
+
+
+# run a simulation with luciole
+simu: tree3.simu
+
+# Compare the ocaml version with the lustre one 
+compare: tree3.lurette
+	cat bfstreelus.rif
+
+# make diring4.simu
+kind2: tree3.kind2
+
+## do not work because there is a modulo in p.lus, which is not (yet) implemented in ../../bit-blast/*.lus
+lesar: tree3.lesar

test/bfs-spanning-tree/bfstreelus_oracle.lus

+-- Here, we use the  Lustre version of the algorithm as an oracle for the ocaml version
+ 
+include "../../sasa/salut/lib/utils.lus"
+
+
+node bfstreelus_oracle(
+  legitimate : bool;
+  ocaml_enabled : bool^actions_number^card;
+  active : bool^actions_number^card; 
+  ocaml_config : int^(card*2);                   
+) 
+returns (ok : bool);
+var
+  lustre_config : state^card;
+  lustre_enabled : bool^actions_number^card;
+let
+  lustre_config, lustre_enabled = 
+    topology(active -> pre active, -- ignored at the first step
+             iVstate(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 stateVi(lustre_config) =ocaml_config;
+          -- compare the lustre and the ocaml version of the processes
+     
+         -- compare the cost functions 
+tel
+
+function iVstate (oc:int^(card*2)) returns (ocs:state^card);
+let
+ocs=[state{d=oc[1];par=oc[0]} , state{d=oc[3];par=oc[2]}, state{d=oc[5];par=oc[4]}];
+tel
+function stateVi (lc:state^card) returns (lci:int^(card*2));
+let
+lci=[lc[0].par,lc[0].d,lc[1].par,lc[1].d,lc[2].par,lc[2].d];
+tel
\ No newline at end of file

test/bfs-spanning-tree/config.ml

+../../../test/bfs-spanning-tree/config.ml
\ No newline at end of file

test/bfs-spanning-tree/p.lus

+  const D=diameter;
+
+function minl<<const degree:int>>(nl:state^degree) returns (m:int);
+let
+m=with (degree=1) then nl[0].d
+  else if nl[0].d <= minl<<degree-1>>(nl[1..(degree-1)]) then nl[0].d
+ else  minl<<degree-1>>(nl[1..(degree-1)]);
+tel
+
+function distp<<const degree:int>>(p:state; nl:state^degree) returns (dp:int);
+var min:int;
+let
+min=minl<<degree>>(nl);
+dp=if (D-1)< min then (D-1)+1 else min +1 ;
+tel
+
+function dist_Ok<<const degree:int>>(p:state; nl:state^degree) returns (ok:bool);
+let
+ok= p.d -1 = minl<<degree>>(nl);
+tel
+
+function parentd<<const degree:int;const n:int>>(p:state ; nl:state^degree) returns (parp:state);
+let
+parp=with (degree=n) then nl[degree-1]
+  else if p.par=n then nl[n] else parentd<<degree,(n+1)>>(p,nl);
+tel
+
+function p_enable<<const degree:int>>(p:state; nl:state^degree) returns
+(a:bool^actions_number);
+var parp:state;
+let
+parp=parentd<<degree;0>>(p,nl);
+a=[p.d<>distp<<degree>>(p,nl) , dist_Ok<<degree>>(p,nl) and parp.d <> p.d - 1];
+tel
+
+function truelist<<const degree:int>>(p:state;nl:state^degree) returns (bl:bool^degree);
+let
+bl=with (degree=1) then [p.d-1=nl[0].d]
+  else [p.d-1=nl[0].d] | truelist<<degree-1>>(p,nl[1..(degree-1)]);
+tel
+
+function indicefsttrue<<const degree:int>> (bl:bool^degree) returns (i:int);
+let
+i= with (degree=1) then if bl[0]=true then 0 else -1
+  else if bl[0]=true then 0 else  1+ indicefsttrue<<degree-1>>(bl[1..(degree-1)]);
+tel
+
+function p_step<<const degree:int>>(p:state; nl:state^degree; a:action) returns
+(pnew:state);
+var bl:bool^degree;
+var i:int;
+let
+bl=truelist<<degree>>(p,nl);
+i=indicefsttrue<<degree>>(bl);
+pnew= if a= CD then state{d=distp<<degree>>(p,nl); par=p.par}
+     else if a=CP then state{d=p.d; par=i}
+  else p;
+tel

test/bfs-spanning-tree/p.ml

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

test/bfs-spanning-tree/root.lus

+type state=struct {d:int; par:int} ;
+type action=enum{CD,CP};
+const actions_number=2;
+
+function action_of_int (i:int) returns (a:action);
+let 
+a=CD;
+tel
+
+function root_enable<<const degree:int>> (r:state ; nl:state^degree) returns
+ (al: bool^actions_number) ;
+let
+al=[r.d<>0,false];
+tel
+
+function root_step <<const degree:int>> (r:state ; nl:state^degree ; a:action)
+returns (rnew:state);
+let
+rnew= state {d=0; par=r.par};
+tel

test/bfs-spanning-tree/root.ml

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

test/bfs-spanning-tree/state.ml

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

test/bfs-spanning-tree/verify.lus

+include "../../sasa/salut/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 : bool;
+	steps : int;
+        
+ 
+let
+--	assert(true -> daemon_is_locally_central<<actions_number,card>>(activations, pre enables, adjacency));
+	assert(true -> daemon_is_synchronous<<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);
+	steps = 0-> pre(steps) +1;
+
+	-- verify that the execution terminates after at most |N|−1 moves:
+	ok = closure
+         --and (true -> legitimate or pre(pot) > pot) -- much easier to prove
+        and (steps >= card => legitimate)
+;
+tel;
+
+
+node stVint<<const card:int>>(c:state^card) returns (cd:int^card);
+let
+cd=with (card=1) then [c[0].d]
+  else [c[0].d] | stVint<<card-1>>(c[1..(card-1)]);
+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; cd:int^card;
+let
+ cd=stVint<<card>>(c);
+   ranges_min = map<< <= , card>>(low^card, cd);
+   ranges_max = map<< < , card>>(cd, card^card);
+   res = boolall<<card>>(ranges_min) and boolall<<card>>(ranges_max);
+tel
+