diff --git a/test/bfs-spanning-tree/Makefile b/test/bfs-spanning-tree/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..610dd54eedc5d1167320211b2314fd7c36609f4c
--- /dev/null
+++ b/test/bfs-spanning-tree/Makefile
@@ -0,0 +1,27 @@
+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
diff --git a/test/bfs-spanning-tree/bfstreelus_oracle.lus b/test/bfs-spanning-tree/bfstreelus_oracle.lus
new file mode 100644
index 0000000000000000000000000000000000000000..fc3062b816d33d918d445f01a966a26c46b796da
--- /dev/null
+++ b/test/bfs-spanning-tree/bfstreelus_oracle.lus
@@ -0,0 +1,37 @@
+-- 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
diff --git a/test/bfs-spanning-tree/config.ml b/test/bfs-spanning-tree/config.ml
new file mode 120000
index 0000000000000000000000000000000000000000..def7dd2f79f63597acab00aca14403f91b53e534
--- /dev/null
+++ b/test/bfs-spanning-tree/config.ml
@@ -0,0 +1 @@
+../../../test/bfs-spanning-tree/config.ml
\ No newline at end of file
diff --git a/test/bfs-spanning-tree/p.lus b/test/bfs-spanning-tree/p.lus
new file mode 100644
index 0000000000000000000000000000000000000000..f0c10fc3aff8da074d762599af83ab7e8a4ec172
--- /dev/null
+++ b/test/bfs-spanning-tree/p.lus
@@ -0,0 +1,58 @@
+ 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
diff --git a/test/bfs-spanning-tree/p.ml b/test/bfs-spanning-tree/p.ml
new file mode 120000
index 0000000000000000000000000000000000000000..ad883bb0a7b336432c0328cb553f0ef9719ef451
--- /dev/null
+++ b/test/bfs-spanning-tree/p.ml
@@ -0,0 +1 @@
+../../../test/bfs-spanning-tree/p.ml
\ No newline at end of file
diff --git a/test/bfs-spanning-tree/root.lus b/test/bfs-spanning-tree/root.lus
new file mode 100644
index 0000000000000000000000000000000000000000..82a6ae95a32d2f5c3c6dd767c04fe6633cff8448
--- /dev/null
+++ b/test/bfs-spanning-tree/root.lus
@@ -0,0 +1,20 @@
+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
diff --git a/test/bfs-spanning-tree/root.ml b/test/bfs-spanning-tree/root.ml
new file mode 120000
index 0000000000000000000000000000000000000000..daedbf7bbd9eb869eebca1e9ba8ee08d69222e27
--- /dev/null
+++ b/test/bfs-spanning-tree/root.ml
@@ -0,0 +1 @@
+../../../test/bfs-spanning-tree/root.ml
\ No newline at end of file
diff --git a/test/bfs-spanning-tree/state.ml b/test/bfs-spanning-tree/state.ml
new file mode 120000
index 0000000000000000000000000000000000000000..740ce359fd6da1ac92013e6d5d86eaccef5884a9
--- /dev/null
+++ b/test/bfs-spanning-tree/state.ml
@@ -0,0 +1 @@
+../../../test/bfs-spanning-tree/state.ml
\ No newline at end of file
diff --git a/test/bfs-spanning-tree/verify.lus b/test/bfs-spanning-tree/verify.lus
new file mode 100644
index 0000000000000000000000000000000000000000..cf0aacdcc20a8afe2e329784bcf3899bf1c3acc1
--- /dev/null
+++ b/test/bfs-spanning-tree/verify.lus
@@ -0,0 +1,46 @@
+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
+