diff --git a/test/Cycle_unison/Makefile b/test/Cycle_unison/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..d78ba7b61a9ae253f560f1618e75e6ab92f8f975
--- /dev/null
+++ b/test/Cycle_unison/Makefile
@@ -0,0 +1,41 @@
+TOPOLOGY ?= diring6
+DOT2LUSFLAGS ?=
+SASA_ALGOS := unison.ml
+DECO_PATTERN="0-:unison.ml"
+
+include ../Makefile.inc
+-include ../Makefile.dot
+
+##############################################################################
+# Non-regression tests
+
+test: clique3.kind2-test clique3.lurette #lesar not work because of the modulo.
+
+clean: genclean
+ rm -f $(TOPOLOGY)*.* clique3*.*
+
+##############################################################################
+# Other examples of use
+
+## Some examples of use of ../Makefile.inc
+
+# run a simulation with luciole
+simu: $(TOPOLOGY).simu
+
+# Compare the ocaml version with the lustre one (with seed)
+compare_seed: $(TOPOLOGY).lurette
+ cat unison.rif
+
+# Compare the ocaml version with the lustre one (no seed)
+compare: $(TOPOLOGY).lurette_no_seed
+ cat unison.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
+
+%.kind2: %.dot
+ make $*_verify.noexpand.lv4
+ time kind2 --color $(color) --modular true --compositional true $*_verify.noexpand.lv4
diff --git a/test/Cycle_unison/Sh/search_config.sh b/test/Cycle_unison/Sh/search_config.sh
new file mode 100755
index 0000000000000000000000000000000000000000..6f28973f0941ec08c43d0c9fdf24efedf56542dd
--- /dev/null
+++ b/test/Cycle_unison/Sh/search_config.sh
@@ -0,0 +1,29 @@
+#!/bin/bash
+# Prends en argument k n topologie
+# Exemple : ./search_config.sh 3 7 ring
+if [ $# -ne 3 ]
+then echo "Not enought arguments"
+ exit 1
+fi
+
+clean(){
+ rm -f *.cmxs *.cmx *.cmi *.o
+ rm -f $1.ml
+ rm -f *.rif *.seed
+ rm -f $1.lus
+ rm -f *_verify.lv4
+ rm -f *.c *.h *_const.lus *.cmt *.exec *.sh rdbg-session* *.log *.pdf
+ rm -f $1*
+ rm k.lus
+}
+
+cd ..
+clean $3$2
+echo "const k = $1 ;" > k.lus
+make $3$2.dot
+salut $3$2.dot
+lv6 -eei $3$2.lus verify.lus $3$2_const.lus -n verify -rnc --lustre-v4 -o $3$2_verify.noexpand.lv4
+cat $3$2_verify.noexpand.lv4 | tr '\n' '@' |sed "s/tel@/tel/g" | sed "s/@/\\n/g" | sed "s/tel-- end of node verify/--%MAIN ;\n--%PROPERTY ok;\ntel\n/" > $3$2_verify.noexpand.lv4.tmp
+mv $3$2_verify.noexpand.lv4.tmp $3$2_verify.noexpand.lv4
+time kind2 --color false --modular true --compositional true $3$2_verify.noexpand.lv4 > Log/$3$1_$2.log
+clean $3$2
diff --git a/test/Cycle_unison/config.ml b/test/Cycle_unison/config.ml
new file mode 120000
index 0000000000000000000000000000000000000000..c5a3daf4b1203ee5c4262ed4509944ea10bd920b
--- /dev/null
+++ b/test/Cycle_unison/config.ml
@@ -0,0 +1 @@
+../../../test/unison/config.ml
\ No newline at end of file
diff --git a/test/Cycle_unison/state.lus b/test/Cycle_unison/state.lus
new file mode 100644
index 0000000000000000000000000000000000000000..75a2c8acae6504e68e84d3a365c94322322faedd
--- /dev/null
+++ b/test/Cycle_unison/state.lus
@@ -0,0 +1,17 @@
+-- automatically generated by salut
+
+type state = int;
+
+type action = enum {T};
+const actions_number = 1;
+
+function action_of_int(i : int) returns (a : action);
+let
+ a = T;
+tel;
+
+function legitimate<<const actions_number:int; const card:int>>(enables : bool^actions_number^card; config: state^card)
+returns (res : bool);
+let
+ res=same_value<<card>>(config);
+tel;
diff --git a/test/Cycle_unison/state.ml b/test/Cycle_unison/state.ml
new file mode 120000
index 0000000000000000000000000000000000000000..0d0c3082ca12a60b790f8e0ffd2a51c3dfb6f200
--- /dev/null
+++ b/test/Cycle_unison/state.ml
@@ -0,0 +1 @@
+../../../test/unison/state.ml
\ No newline at end of file
diff --git a/test/Cycle_unison/unison.lus b/test/Cycle_unison/unison.lus
new file mode 100644
index 0000000000000000000000000000000000000000..173f720cc0ff7915592ca45447b94679faef780a
--- /dev/null
+++ b/test/Cycle_unison/unison.lus
@@ -0,0 +1,34 @@
+include "k.lus"
+
+
+const m0 = 2*diameter -1;
+--const k = 5 --if m0 < 2 then 2 else m0
+--;
+function min_clock<<const n:int>> (this : int; neighbors : neigh^n)
+returns (new: int);
+var min:int;
+let
+ min = if this <= state(neighbors[0]) then this else state(neighbors[0]) ;
+ new = with (n = 1) then min
+ else min_clock<< n-1 >> (min, neighbors[1 .. n-1]);
+tel;
+
+function newClockValue<<const n:int>> (this : int ; neighbors : neigh^n)
+returns (new: state);
+let
+ new = (min_clock<<n>>(this,neighbors)+1) mod k;
+tel;
+
+function unison_enable<<const degree:int>> (this : state; neighbors : neigh^degree)
+returns (enabled : bool^actions_number);
+let
+ enabled= [ this <> (newClockValue<<degree>>(this,neighbors)) ];
+tel;
+
+function unison_step<<const degree:int>>(
+ this : state;
+ neighbors : neigh^degree; action : action)
+returns (new : state);
+let
+ new = newClockValue<<degree>>(this,neighbors);
+tel;
diff --git a/test/Cycle_unison/unison.ml b/test/Cycle_unison/unison.ml
new file mode 120000
index 0000000000000000000000000000000000000000..a0ad03b587427e13bb7504cff3ca12412f60cc39
--- /dev/null
+++ b/test/Cycle_unison/unison.ml
@@ -0,0 +1 @@
+../../../test/unison/unison.ml
\ No newline at end of file
diff --git a/test/Cycle_unison/unison_oracle.lus b/test/Cycle_unison/unison_oracle.lus
new file mode 100644
index 0000000000000000000000000000000000000000..ac39af1e697e4f4820ddb061c9334d84148fc3fc
--- /dev/null
+++ b/test/Cycle_unison/unison_oracle.lus
@@ -0,0 +1,32 @@
+-- Here, we use the Lustre version of the algorithm as an oracle for the ocaml version
+
+include "../../lib/utils.lus"
+
+node unison_oracle(
+ legitimate : bool;
+ ocaml_enabled : bool^actions_number^card;
+ active : bool^actions_number^card;
+ ocaml_config : state^card;
+ round:bool;
+ round_nb:int;
+)
+returns (ok : bool);
+var
+ lustre_config : state^card;
+ lustre_enabled : bool^actions_number^card;
+ lustre_round:bool;
+ lustre_round_nb:int;
+let
+ lustre_config, lustre_enabled, lustre_round, lustre_round_nb =
+ 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
+ and lustre_round = round
+ and lustre_round_nb = round_nb
+
+;
+ -- compare the lustre and the ocaml version of the processes
+tel;
diff --git a/test/Cycle_unison/verify.lus b/test/Cycle_unison/verify.lus
new file mode 100644
index 0000000000000000000000000000000000000000..eeaad4352a607d0795b0c923c0a266d61b4f63a7
--- /dev/null
+++ b/test/Cycle_unison/verify.lus
@@ -0,0 +1,64 @@
+include "../../lib/sas.lus"
+
+
+
+node verify(activations : bool^actions_number^card; inits : state^card) returns (ok : bool);
+var nb_step: int;
+var config,mirror_inits : state^card;
+var enables : bool^actions_number^card;
+var legitimate, noinit : bool;
+ lustre_round : bool;
+ lustre_round_nb : int;
+-- all_permuts: state^card^(card-1);
+let
+ assert(not (legitimate<<actions_number, card>>(enables, inits)));
+ assert(true -> daemon_is_synchronous<<actions_number,card>>(activations, pre enables));
+ assert(rangei<<0,card,k>>(inits));
+ assert(true -> inits = pre inits);
+
+ config, enables,lustre_round, lustre_round_nb = topology(activations, inits);
+
+ legitimate = legitimate<<actions_number, card>>(enables, config);
+ -- closure = true -> (pre(legitimate) => legitimate);
+ nb_step = (-1) -> pre(nb_step) + 1;
+ mirror_inits = mirror<<card>>(inits);
+
+ noinit = true -> not (config=inits or
+ config=mirror_inits
+or
+ eq_forall_permutations<<card,card-1>>(inits,mirror_inits,config)
+);
+ -- verify that the execution terminates after at most |N|−1 moves:
+ ok = -- closure
+ ( noinit or legitimate )
+-- and (nb_step>=(3*diameter-2) => legitimate)
+;
+tel;
+--type state = int;
+--node test = permutation<<2,3>>;
+
+function mirror<<const card:int>>(config: state^card) returns (res: state^card);
+let
+ res = with (card=1) then [config[0]]
+ else mirror<<card-1>>(config[1..card-1]) | [config[0]];
+tel
+
+function eq_forall_permutations<< const card:int; const N:int>>
+(inits,mir_inits, c:state^card) returns (res:bool);
+var cp:state^card;
+let
+ cp = c[1..card-1] | [c[0]];
+ res =
+ with (N=1) then (cp=inits or cp=mir_inits)
+ else (cp=inits or cp=mir_inits) or eq_forall_permutations<<card, N-1>>(inits,mir_inits,cp);
+tel
+
+-- all states are initially in [0; card|[
+node rangei<<const low:int; const card:int; const k:int>>(c:state^card) returns (res:bool);
+var
+ ranges_min, ranges_max : bool^card;
+let
+ ranges_min = map<< <= , card>>(low^card, c);
+ ranges_max = map<< < , card>>(c, k^card);
+ res = boolall<<card>>(ranges_min) and boolall<<card>>(ranges_max);
+tel