diff --git a/salut/test/coloring/coloring_oracle.lus b/salut/test/coloring/coloring_oracle.lus
index 03e0929abd6cf3d0a4312bb1557b32b579b92a6d..7dc9b10324f33034b67de377bcded519f80074b4 100644
--- a/salut/test/coloring/coloring_oracle.lus
+++ b/salut/test/coloring/coloring_oracle.lus
@@ -1,17 +1,17 @@
 
 -- Here, we use the  Lustre version of the algorithm as an oracle for the ocaml version
- 
+
 include "../../lib/utils.lus"
 
 node coloring_oracle(
   legitimate : bool;
   ocaml_cost : real;
   ocaml_enabled : bool^actions_number^card;
-  active : bool^actions_number^card; 
+  active : bool^actions_number^card;
   ocaml_config : state^card;
   round:bool;
-  round_nb:int;                   
-)  
+  round_nb:int;
+)
 returns (ok : bool);
 var
   lustre_config : state^card;
@@ -20,18 +20,18 @@ var
   lustre_round_nb : int;
 --  lustre_cost:int;
 let
-  lustre_config, lustre_enabled, lustre_round, lustre_round_nb = 
+  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
              );
 --  lustre_cost = cost(lustre_enabled, lustre_config);
-  ok =     lustre_enabled = ocaml_enabled 
+  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
 --       and Lustre::real2int(ocaml_cost) = lustre_cost
 --       and lustre_round = round
---       and lustre_round_nb = round_nb
+       and lustre_round_nb = round_nb
 ;
-         -- compare the cost functions 
+         -- compare the cost functions
 tel
diff --git a/salut/test/ghosh/Makefile b/salut/test/ghosh/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..3e253ff3168bc2aade2fcc34244f49e7ae34a7ec
--- /dev/null
+++ b/salut/test/ghosh/Makefile
@@ -0,0 +1,32 @@
+TOPOLOGY ?= ghosh8
+DOT2LUSFLAGS ?=
+SASA_ALGOS := p0.ml p_odd.ml p_even.ml p_last
+DECO_PATTERN="not possible with this algo"
+
+
+include ./Makefile.inc
+include ./Makefile.dot
+
+##############################################################################
+# Non-regression tests
+
+test: ghosh8.kind2-test ghosh8.lurette
+
+clean: genclean
+
+##############################################################################
+# Other examples of use
+
+## Some examples of use of ../Makefile.inc
+
+# run a simulation with luciole
+simu: ghosh8.simu
+
+# make diring4.simu
+kind2: ghosh8.kind2
+
+## do not work because there is a modulo in p.lus, which is not (yet) implemented in ../../bit-blast/*.lus
+lesar: ghosh8.lesar
+##############################################################################
+
+-include ./Makefile.untrack
diff --git a/salut/test/ghosh/Makefile.dot b/salut/test/ghosh/Makefile.dot
new file mode 120000
index 0000000000000000000000000000000000000000..618c8ab02bdfa1c158e4fda4241e5fc0187b611c
--- /dev/null
+++ b/salut/test/ghosh/Makefile.dot
@@ -0,0 +1 @@
+../Makefile.dot
\ No newline at end of file
diff --git a/salut/test/ghosh/Makefile.inc b/salut/test/ghosh/Makefile.inc
new file mode 120000
index 0000000000000000000000000000000000000000..b9a83c9dae3121bce33a41c0e052c2c405b90e26
--- /dev/null
+++ b/salut/test/ghosh/Makefile.inc
@@ -0,0 +1 @@
+../Makefile.inc
\ No newline at end of file
diff --git a/salut/test/ghosh/config.ml b/salut/test/ghosh/config.ml
new file mode 120000
index 0000000000000000000000000000000000000000..5cda87c8eb5cef483f87c3e0dc61cb6714497a40
--- /dev/null
+++ b/salut/test/ghosh/config.ml
@@ -0,0 +1 @@
+../../../test/ghosh/config.ml
\ No newline at end of file
diff --git a/salut/test/ghosh/dune b/salut/test/ghosh/dune
new file mode 120000
index 0000000000000000000000000000000000000000..a1ef974a7f8b8c10affe9255f54c64f91430171d
--- /dev/null
+++ b/salut/test/ghosh/dune
@@ -0,0 +1 @@
+../../../test/dune2copy
\ No newline at end of file
diff --git a/salut/test/ghosh/dune-project b/salut/test/ghosh/dune-project
new file mode 120000
index 0000000000000000000000000000000000000000..f539fb462993123645b56b6670732a7198c756a4
--- /dev/null
+++ b/salut/test/ghosh/dune-project
@@ -0,0 +1 @@
+../../../test/dune-project2copy
\ No newline at end of file
diff --git a/salut/test/ghosh/dune-workspace b/salut/test/ghosh/dune-workspace
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/salut/test/ghosh/ghosh10.dot b/salut/test/ghosh/ghosh10.dot
new file mode 120000
index 0000000000000000000000000000000000000000..ea4036e14b318aa27bd98628b2fc945dbeeb2680
--- /dev/null
+++ b/salut/test/ghosh/ghosh10.dot
@@ -0,0 +1 @@
+../../../test/ghosh/ghosh10.dot
\ No newline at end of file
diff --git a/salut/test/ghosh/ghosh12.dot b/salut/test/ghosh/ghosh12.dot
new file mode 120000
index 0000000000000000000000000000000000000000..b6017deaf1e0048d8ae64e6f765aae39f538ee89
--- /dev/null
+++ b/salut/test/ghosh/ghosh12.dot
@@ -0,0 +1 @@
+../../../test/ghosh/ghosh12.dot
\ No newline at end of file
diff --git a/salut/test/ghosh/ghosh14.dot b/salut/test/ghosh/ghosh14.dot
new file mode 120000
index 0000000000000000000000000000000000000000..72843d0edc17b88b5a3de0412e6935b5bdb50eac
--- /dev/null
+++ b/salut/test/ghosh/ghosh14.dot
@@ -0,0 +1 @@
+../../../test/ghosh/ghosh14.dot
\ No newline at end of file
diff --git a/salut/test/ghosh/ghosh2.dot b/salut/test/ghosh/ghosh2.dot
new file mode 120000
index 0000000000000000000000000000000000000000..ff6438ace4a98990d70a283421254310384efbd0
--- /dev/null
+++ b/salut/test/ghosh/ghosh2.dot
@@ -0,0 +1 @@
+../../../test/ghosh/ghosh2.dot
\ No newline at end of file
diff --git a/salut/test/ghosh/ghosh4.dot b/salut/test/ghosh/ghosh4.dot
new file mode 120000
index 0000000000000000000000000000000000000000..71448e59b7b4a466e8f43104761b3422d1786b33
--- /dev/null
+++ b/salut/test/ghosh/ghosh4.dot
@@ -0,0 +1 @@
+../../../test/ghosh/ghosh4.dot
\ No newline at end of file
diff --git a/salut/test/ghosh/ghosh6.dot b/salut/test/ghosh/ghosh6.dot
new file mode 120000
index 0000000000000000000000000000000000000000..7166bcc2c20e3cedd054380bb82e24cdc8b6f491
--- /dev/null
+++ b/salut/test/ghosh/ghosh6.dot
@@ -0,0 +1 @@
+../../../test/ghosh/ghosh6.dot
\ No newline at end of file
diff --git a/salut/test/ghosh/ghosh8.dot b/salut/test/ghosh/ghosh8.dot
new file mode 120000
index 0000000000000000000000000000000000000000..9664d73ad00f85101e0f9c81874badaf8d915402
--- /dev/null
+++ b/salut/test/ghosh/ghosh8.dot
@@ -0,0 +1 @@
+../../../test/ghosh/ghosh8.dot
\ No newline at end of file
diff --git a/salut/test/ghosh/ghosh_oracle.lus b/salut/test/ghosh/ghosh_oracle.lus
new file mode 100644
index 0000000000000000000000000000000000000000..b57288cceacb97d37f016c0f774e1c378fc9902a
--- /dev/null
+++ b/salut/test/ghosh/ghosh_oracle.lus
@@ -0,0 +1,38 @@
+
+-- Here, we use the  Lustre version of the algorithm as an oracle for the ocaml version
+
+include "../../lib/utils.lus"
+-- include "cost.lus"
+
+node ghosh_oracle(
+  legitimate : bool;
+--  ocaml_cost : real;
+  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_cost:int;
+  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 round = lustre_round
+       and round_nb = lustre_round_nb
+;
+tel
diff --git a/salut/test/ghosh/p0.lus b/salut/test/ghosh/p0.lus
new file mode 100644
index 0000000000000000000000000000000000000000..ace493a7656203b0c741719a71b213c97a9b296e
--- /dev/null
+++ b/salut/test/ghosh/p0.lus
@@ -0,0 +1,15 @@
+
+
+function p0_enable<<const degree:int>>(this : state; neighbors : neigh^degree)
+returns (enabled : bool^actions_number);
+let
+  enabled = [ this <> state(neighbors[0]) ];
+tel;
+
+function p0_step<<const degree:int>>(
+  this : state;
+  neighbors : neigh^degree; action : action)
+returns (new : state);
+let
+  new = not this;
+tel;
diff --git a/salut/test/ghosh/p0.ml b/salut/test/ghosh/p0.ml
new file mode 120000
index 0000000000000000000000000000000000000000..7608d5439e6ebcfb1675a8aea4cd5aaa929911ca
--- /dev/null
+++ b/salut/test/ghosh/p0.ml
@@ -0,0 +1 @@
+../../../test/ghosh/p0.ml
\ No newline at end of file
diff --git a/salut/test/ghosh/p_even.lus b/salut/test/ghosh/p_even.lus
new file mode 100644
index 0000000000000000000000000000000000000000..1b6d21afbd4e0496cdce4ddcc69da90a3d923c03
--- /dev/null
+++ b/salut/test/ghosh/p_even.lus
@@ -0,0 +1,18 @@
+
+
+function p_even_enable<<const degree:int>>(s1 : state; neighbors : neigh^degree)
+returns (enabled : bool^actions_number);
+let
+  enabled = [ state(neighbors[0+if degree=3 then 0 else 1]) = s1 and
+              s1 = state(neighbors[1+if degree=3 then 0 else 1]) and
+              state(neighbors[2+if degree=3 then 0 else 1]) = not state(neighbors[1+if degree=3 then 0 else 1])
+             ];
+tel;
+
+function p_even_step<<const degree:int>>(
+  this : state;
+  neighbors : neigh^degree; action : action)
+returns (new : state);
+let
+  new = not this;
+tel;
diff --git a/salut/test/ghosh/p_even.ml b/salut/test/ghosh/p_even.ml
new file mode 120000
index 0000000000000000000000000000000000000000..bb954ccbea71162d70f99953f83c0b587e921fb4
--- /dev/null
+++ b/salut/test/ghosh/p_even.ml
@@ -0,0 +1 @@
+../../../test/ghosh/p_even.ml
\ No newline at end of file
diff --git a/salut/test/ghosh/p_last.lus b/salut/test/ghosh/p_last.lus
new file mode 100644
index 0000000000000000000000000000000000000000..05eada0e16ef3e170dcad6046486010c31a7f2cf
--- /dev/null
+++ b/salut/test/ghosh/p_last.lus
@@ -0,0 +1,15 @@
+
+
+function p_last_enable<<const degree:int>>(s2 : state; neighbors : neigh^degree)
+returns (enabled : bool^actions_number);
+let
+  enabled = [ state(neighbors[1]) = s2 ];
+tel;
+
+function p_last_step<<const degree:int>>(
+  this : state;
+  neighbors : neigh^degree; action : action)
+returns (new : state);
+let
+  new = not this;
+tel;
diff --git a/salut/test/ghosh/p_last.ml b/salut/test/ghosh/p_last.ml
new file mode 120000
index 0000000000000000000000000000000000000000..8218527ff89cd52c9c8ac4344871b5b819072c84
--- /dev/null
+++ b/salut/test/ghosh/p_last.ml
@@ -0,0 +1 @@
+../../../test/ghosh/p_last.ml
\ No newline at end of file
diff --git a/salut/test/ghosh/p_odd.lus b/salut/test/ghosh/p_odd.lus
new file mode 100644
index 0000000000000000000000000000000000000000..fb65a18caa74bd54370c90c8f8d7da19ecd23371
--- /dev/null
+++ b/salut/test/ghosh/p_odd.lus
@@ -0,0 +1,18 @@
+
+
+function p_odd_enable<<const degree:int>>(s2 : state; neighbors : neigh^degree)
+returns (enabled : bool^actions_number);
+let
+  enabled = [ state(neighbors[0]) = state(neighbors[1]) and
+              state(neighbors[2]) = state(neighbors[1]) and
+              s2 = not state(neighbors[0])
+             ];
+tel;
+
+function p_odd_step<<const degree:int>>(
+  this : state;
+  neighbors : neigh^degree; action : action)
+returns (new : state);
+let
+  new = not this;
+tel;
diff --git a/salut/test/ghosh/p_odd.ml b/salut/test/ghosh/p_odd.ml
new file mode 120000
index 0000000000000000000000000000000000000000..6fc6bcbe51c3c2470d58ecc68a7f422be7339239
--- /dev/null
+++ b/salut/test/ghosh/p_odd.ml
@@ -0,0 +1 @@
+../../../test/ghosh/p_odd.ml
\ No newline at end of file
diff --git a/salut/test/ghosh/state.lus b/salut/test/ghosh/state.lus
new file mode 100644
index 0000000000000000000000000000000000000000..e2711eaaae1030988947941f120beb696a171ae9
--- /dev/null
+++ b/salut/test/ghosh/state.lus
@@ -0,0 +1,16 @@
+
+type state = bool;
+
+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=n_xor<<card>>(map<<n_or<<actions_number>>,card>> (enables));
+tel;
diff --git a/salut/test/ghosh/state.ml b/salut/test/ghosh/state.ml
new file mode 120000
index 0000000000000000000000000000000000000000..11d1e919dae2cff646d7dffc64b06111529fb741
--- /dev/null
+++ b/salut/test/ghosh/state.ml
@@ -0,0 +1 @@
+../../../test/ghosh/state.ml
\ No newline at end of file
diff --git a/salut/test/ghosh/verify.lus b/salut/test/ghosh/verify.lus
new file mode 100644
index 0000000000000000000000000000000000000000..2bf4b1cf36bd19eb5b01116ce994ef7ed42a478c
--- /dev/null
+++ b/salut/test/ghosh/verify.lus
@@ -0,0 +1,42 @@
+
+
+const n = card;
+
+-- Theorem XXX
+
+ const worst_case=100;
+
+node verify(
+  active : bool^actions_number^card;
+  init_config : state^card
+)
+returns (ok : bool);
+var
+  config : state^card;
+  enabled : bool^actions_number^card;
+  legitimate, closure, theorem : bool;
+  steps : int;
+  round:bool; round_nb:int;
+let
+-- the worst-case in necessarily central
+--	assert(true -> daemon_is_central<<actions_number,card>>(active, pre enabled));
+	assert(true -> daemon_is_distributed<<actions_number,card>>(active, pre enabled));
+--	assert(true -> daemon_is_synchronous<<actions_number,card>>(active, pre enabled));
+
+	config, enabled, round, round_nb = topology(active, init_config);
+        assert(config = init_config -> true);
+
+	-- stability = mutual exclusion: exactly 1 node is enabled at a time
+        legitimate = legitimate<<actions_number,card>>(enabled,config);
+
+	closure = true -> (pre(legitimate) => legitimate);
+
+	steps = 0 -> (pre(steps) + 1);
+        theorem  = (steps >= worst_case) => legitimate;
+
+
+	ok =  true
+	     and closure
+             and theorem
+;
+tel;
diff --git a/salut/test/run-kind2.sh b/salut/test/run-kind2.sh
index 8e34bd26889616e1fd0a03b77377bd5ebfa12acc..aa7ec28e1cbd0f220413034fbbaf7b31baf0a22d 100755
--- a/salut/test/run-kind2.sh
+++ b/salut/test/run-kind2.sh
@@ -100,7 +100,7 @@ fi
 kind2_opt="--timeout 36000 -json -v "
 kind2_opt="--enable BMC --enable IND --timeout 36000 -json -v"
 kind2_opt="--enable BMC --enable IND --enable IC3 --timeout 36000"
-kind2_opt="--smt_solver $solver --enable BMC --enable IND --timeout 36000 $@"
+kind2_opt="--smt_solver $solver --enable BMC --enable IND  --timeout 36000 $@"
 
 # --qe_method {precise|impl|cooper}
 
@@ -111,11 +111,12 @@ cp Makefile ${TMP}
 cp ${GITROOT}/salut/test/Makefile.inc  ${TMP}
 cp ${GITROOT}/salut/test/Makefile.dot  ${TMP}
 cp *.lus ${TMP}
+cp $main.dot ${TMP} -f
 cp ${LIB_LUS} ${TMP}
 cd  ${TMP}
 
-make $main.dot || (echo "E: is Makefile.dot included from Makefile?"; exit 2)
-make ${main}_const.lus
+make $main.dot || [ -f $main.dot ] || (echo "E: is Makefile.dot included from Makefile?"; exit 2)
+salut $main.dot
 
 # Get rif of the lutre v6 constructs that kind2 does not handle
 lv6 -eei ${LIB_LUS} $main.lus verify.lus ${main}_const.lus -n verify --lustre-v4 -en -knc -o $main.verify.lv4
diff --git a/test/Makefile b/test/Makefile
index 55d5a915237f8a8ead368b3b4f72a5edc2b98424..f312b03d888a91aa2f91e09711846a2bbed28022 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -18,6 +18,7 @@ test:
 	cd rsp-tree/ && make test
 	cd toy-example-a5sf/ && make test
 	cd k-clustering/ && make test
+	cd ghosh/ && make test
 	echo "Every test went fine!"
 
 clean:
@@ -40,6 +41,7 @@ clean:
 	cd rsp-tree/ && make clean
 	cd toy-example-a5sf/ && make clean
 	cd k-clustering/ && make clean
+	cd ghosh/ && make clean
 
 utest:
 	cd skeleton/ &&	make test
@@ -60,5 +62,6 @@ utest:
 	cd rsp-tree/ && make utest
 	cd toy-example-a5sf/ && make utest
 	cd k-clustering/ && make utest
+	cd ghosh/ && make utest
 
 -include Makefile.untracked
diff --git a/test/dijkstra-ring/state.ml b/test/dijkstra-ring/state.ml
index 55242149cd02056f213efecaf91dc0e73ae1aa33..dda9bb4cecaaa9f0be992d33a53ef4580ff43d1a 100644
--- a/test/dijkstra-ring/state.ml
+++ b/test/dijkstra-ring/state.ml
@@ -1,6 +1,8 @@
 
-(* semi-anonymous network: each node knows if its neighbors is the root! *)
-type t = { root: bool ; v : int } 
+(* semi-anonymous network: each node knows if its neighbors is the root!
+Actually only necessary to define the legitimate predicate
+*)
+type t = { root: bool ; v : int }
 let to_string s = Printf.sprintf "c=%i" s.v
 let first = ref true
 let (of_string: (string -> t) option) =
@@ -23,8 +25,8 @@ let (of_string: (string -> t) option) =
       in
       (* Printf.printf "state.ml: { root = %b ; c = %d }\n%!" res.root res.v; *)
       res
-    
+
     )
-    
+
 let copy x = x
 let actions = ["T"]
diff --git a/test/ghosh/Makefile b/test/ghosh/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..4addd7d599e4d02d920554dda726d86961df6aac
--- /dev/null
+++ b/test/ghosh/Makefile
@@ -0,0 +1,22 @@
+# Time-stamp: <modified the 30/05/2023 (at 17:13) by Erwan Jahier>
+
+DECO_PATTERN="0-:p.ml"
+-include ./Makefile.dot
+-include ./Makefile.inc
+
+##############################################################################
+# Non-regression tests
+
+test:  ghosh8.gm_test clean
+
+# update golden-master tests (if necessary)
+utest:
+	make ghosh8.ugm_test || echo "grid4 ok"
+
+##############################################################################
+# Other examples of use
+
+gui: ghosh8.rdbgui
+
+clean: genclean
+	rm -f grid*.* diring*.* clique*.* er*.*
diff --git a/test/ghosh/Makefile.dot b/test/ghosh/Makefile.dot
new file mode 120000
index 0000000000000000000000000000000000000000..618c8ab02bdfa1c158e4fda4241e5fc0187b611c
--- /dev/null
+++ b/test/ghosh/Makefile.dot
@@ -0,0 +1 @@
+../Makefile.dot
\ No newline at end of file
diff --git a/test/ghosh/Makefile.inc b/test/ghosh/Makefile.inc
new file mode 100644
index 0000000000000000000000000000000000000000..0924984dc3f27522d820c9bdb873260c9f512c26
--- /dev/null
+++ b/test/ghosh/Makefile.inc
@@ -0,0 +1,114 @@
+# Time-stamp: <modified the 27/02/2023 (at 16:05) by Erwan Jahier>
+#
+# Define some default rules that ought to work most of the time
+#
+
+sasa=sasa
+
+LIB=-package algo
+
+ifndef DAEMON
+# some rules uses this one
+DAEMON=
+endif
+
+
+
+# obselete: use 'dune build' instead
+#%.ml: %.dot
+# 	sasa -reg $<
+
+# ifndef OCAMLOPT
+# 	OCAMLOPT=ocamlfind ocamlopt -bin-annot
+# endif
+#%.cmxs: %.ml
+#	$(OCAMLOPT) $(LIB) -shared state.ml $(shell sasa -algo $*.dot) config.ml $< -o $@
+# ifndef OCAMLC
+# 	OCAMLC=ocamlfind ocamlc -bin-annot
+# endif
+# %.cma: %.ml
+# 	$(OCAMLC) $(LIB) -a state.ml $(shell sasa -algo $*.dot) $< -o $@
+
+%.cmxs:
+	[ -f $*.ml ] && rm $*.ml || true
+	topology=$* dune build
+%.cma:
+	[ -f $*.ml ] && rm $*.ml || true
+	topology=$* dune build
+%.cmxa:
+	[ -f $*.ml ] && rm $*.ml || true
+	topology=$* dune build
+%.a:
+	[ -f $*.ml ] && rm $*.ml || true
+	topology=$* dune build
+
+
+genclean:
+	rm -f *.cmxs sasa *.cm* *.o *.pdf *.rif *.gp *.log *.dro *.seed *.c *.h sasa-*.dot *.cmt *.annot
+	rm -rf .rdbg-session*.ml rdbg-session*.ml luretteSession* a.out *.cov .read_dot.ml
+	rm -f *.exec  grid*.ml  rdbg-history .rdbg-cmds.ml rdbg-cmds.ml my-rdbg-tuning.ml
+	dune clean
+
+clean: genclean
+.PRECIOUS: %.dot
+
+##################################################################################
+#
+-include Makefile.untracked
+
+g:gnuplot
+s:sim2chrogtk
+
+
+%.lut: %.dot %.cmxs
+	sasa -gld $< || echo "==> ok, I'll use the existing $@ file"
+
+%_oracle.lus: %.dot %.cmxs
+	sasa -glos $< || echo "==> ok, I'll use the existing $@ file"
+
+%.rif: %.cmxs %.dot
+	$(sasa) $(sasaopt) $*.dot > $*.rif
+
+%.pdf:
+	dot -Tpdf $*.dot -o $*.pdf
+	xpdf $*.pdf
+
+%.ocd: %.ml
+	rdbg -camldebug -sut "sasa $.dot" -l 1000
+
+%.test: %.dot %.cmxs
+	sasa  $<
+
+############################################################################################
+# Golden master tests
+# compare the generated rif file with a previously generated reference
+EXPDIR=`rdbg --ocaml-version`
+$(EXPDIR):
+	[ -d $(EXPDIR) ] || (mkdir -p $(EXPDIR) ; make utest)
+
+%.gm_test: %.cmxs $(EXPDIR)
+	sasa  $*.dot -seed 42 -l 1000 > $*.rif && \
+	diff -I "# on" -I " version " -B -u -i -w $(EXPDIR)/$*.rif.exp $*.rif > $*.res
+	[ ! -s $*.res ]  && echo "\n\n==> $*.gm_test went fine"
+
+# update the reference
+%.ugm_test: %.cmxs $(EXPDIR)
+	sasa  $*.dot -seed 42 -l 1000 > $*.rif && \
+	cp $*.rif $(EXPDIR)/$*.rif.exp
+
+# fix the seed (used, e.g., in Makefile.dot) for the non-regression tests
+ifndef SEED
+  SEED = --seed 42
+endif
+############################################################################################
+
+%.rdbg: %.cma
+	ledit -h rdbg-history -x rdbg --sasa -sut "sasa $* $(DAEMON)"  -l 10000
+
+%.rdbg-test: %.cma
+	rdbg --sasa -sut "sasa $*.dot $(DAEMON)" -go --input some_session -l 10000 \
+		| grep Error > $*.rdbg-test.log && echo "Error: 'make $@' failed" \
+		  && cat $*.rdbg-test.log && exit 2  || echo "'make $@' suceeds"
+
+%.rdbgui: %.cma
+	ledit -h rdbg-history -x rdbgui4sasa -sut "sasa $*.dot"  -l 10000
diff --git a/test/ghosh/config.ml b/test/ghosh/config.ml
new file mode 100644
index 0000000000000000000000000000000000000000..e82eec4b1094f490a400d1f5ef1bbd9dcaf4289a
--- /dev/null
+++ b/test/ghosh/config.ml
@@ -0,0 +1,37 @@
+open Algo
+open State
+
+let (legitimate: pid list -> (pid -> t * (t neighbor * pid) list) -> bool) =
+  fun  pidl get ->
+  (* increment the token number i if pid is enabled *)
+  let incr_token i pid =
+    let s, nl = get pid in
+    let nl = List.map fst  nl in
+    let have_token =
+      match s.kind with
+      | Bottom -> P0.enable_f s nl <> []
+      | Odd -> P_odd.enable_f s nl <> []
+      | Even -> P_even.enable_f s nl <> []
+      | Top -> P_last.enable_f s nl <> []
+    in
+    if have_token then i+1 else i
+  in
+  (* Now let's iterate on all the nodes starting from |tokens|=0 *)
+  let token_nb = List.fold_left incr_token 0 pidl in
+  (* if there is 1 token, returns true *)
+  token_nb = 1
+let legitimate = Some legitimate
+
+let potential = None
+let fault = None (* None => the simulation stop once a legitimate configuration is reached *)
+
+open Algo
+
+let n2s nl n =
+  match nl with
+  | [B(b)] -> { n with s = b }
+  | _ -> assert false
+
+let s2vl b = [B(b.s)]
+
+let init_search_utils = Some(s2vl, n2s)
diff --git a/test/ghosh/dune b/test/ghosh/dune
new file mode 100644
index 0000000000000000000000000000000000000000..70215208089c9d9c670b32e71b446192ae1f79f7
--- /dev/null
+++ b/test/ghosh/dune
@@ -0,0 +1,59 @@
+;; dune file to build the cmxs (resp the cma) needed by sasa (resp rdbgui4sasa)
+
+(library
+ (name user_algo_files) ;; a fake name because "%{env:topology=ring4}" is rejected
+ (libraries algo)
+; (wrapped false) ; so that user_algo_files is not used in the .cm*
+ (library_flags -linkall)
+)
+
+;; copy the <topology>.dot to the build dir if it already exists
+;; or create it via make otherwise
+(rule
+ (mode (promote (until-clean)))
+ (target %{env:topology=ring4}.dot)
+ (deps
+  (:makefile Makefile)
+  (:makefiledot Makefile.dot)
+ )
+ (action
+  (bash "[ -f ../../%{env:topology=ring4}.dot ] && cp ../../%{env:topology=ring4}.dot . || \
+            make %{env:topology=ring4}.dot")
+ )
+)
+
+;; generate the registration file (out of the dot file)
+(rule
+ (target %{env:topology=ring4}.ml)
+ (deps (:dotfile ./%{env:topology=ring4}.dot))
+ (action
+  (bash "sasa -reg %{dotfile}")
+ )
+)
+
+(rule
+ (mode (promote (until-clean)))
+ (action
+  (progn
+    ;; give them back the rigth name
+    (copy user_algo_files.cmxs %{env:topology=ring4}.cmxs)
+    (copy user_algo_files.cmxa  %{env:topology=ring4}.cmxa)
+    (copy user_algo_files.cma  %{env:topology=ring4}.cma)
+    (copy user_algo_files.a  %{env:topology=ring4}.a)
+    ;; we can have only one registering file in the build dir
+    (bash "rm %{env:topology=ring4}.ml")
+   )
+ )
+ (deps (:src ./%{env:topology=ring4}.dot))
+)
+
+;; The glue lustre code between the oracle and the topology
+(rule
+ (target %{env:topology=ring4}_oracle.lus)
+ (mode (promote (until-clean)))
+ (deps
+  (:dotfile ./%{env:topology=ring4}.dot)
+  (:cmxs ./%{env:topology=ring4}.cmxs)
+  )
+ (action (bash "sasa -glos %{dotfile} -o $(basename $(realpath $PWD/../..))"))
+ )
diff --git a/test/ghosh/dune-project b/test/ghosh/dune-project
new file mode 100644
index 0000000000000000000000000000000000000000..37f995d6492934bb2174bfbda93670ac438e5844
--- /dev/null
+++ b/test/ghosh/dune-project
@@ -0,0 +1 @@
+(lang dune 3.0)
diff --git a/test/ghosh/dune-workspace b/test/ghosh/dune-workspace
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/test/ghosh/ghosh10.dot b/test/ghosh/ghosh10.dot
new file mode 100644
index 0000000000000000000000000000000000000000..25848a256dcdd385691bed110c25505bafe9db63
--- /dev/null
+++ b/test/ghosh/ghosh10.dot
@@ -0,0 +1,27 @@
+graph g8 {
+
+
+  p0 [algo="p0.ml"]
+  p1 [algo="p_even.ml"]
+  p2 [algo="p_odd.ml"]
+  p3 [algo="p_even.ml"]
+  p4 [algo="p_odd.ml"]
+  p5 [algo="p_even.ml"]
+  p6 [algo="p_odd.ml"]
+  p7 [algo="p_even.ml"]
+  p8 [algo="p_odd.ml"]
+  p9 [algo="p_last.ml"]
+
+  p1 -- p0
+  p2 -- p1
+  p3 -- p2
+  p4 -- p3
+  p5 -- p4
+  p6 -- p5
+  p7 -- p6
+  p8 -- p7
+  p9 -- p8
+
+  p1 -- p3 -- p5 -- p7 -- p9
+  p0 -- p2 -- p4 -- p6 -- p8
+}
diff --git a/test/ghosh/ghosh12.dot b/test/ghosh/ghosh12.dot
new file mode 100644
index 0000000000000000000000000000000000000000..2f16ad7401bc24d53e180271112fa4c007d33c55
--- /dev/null
+++ b/test/ghosh/ghosh12.dot
@@ -0,0 +1,31 @@
+graph g {
+
+
+  p0 [algo="p0.ml"]
+  p1 [algo="p_even.ml"]
+  p2 [algo="p_odd.ml"]
+  p3 [algo="p_even.ml"]
+  p4 [algo="p_odd.ml"]
+  p5 [algo="p_even.ml"]
+  p6 [algo="p_odd.ml"]
+  p7 [algo="p_even.ml"]
+  p8 [algo="p_odd.ml"]
+  p9 [algo="p_even.ml"]
+  p10 [algo="p_odd.ml"]
+  p11 [algo="p_last.ml"]
+
+  p1 -- p0
+  p2 -- p1
+  p3 -- p2
+  p4 -- p3
+  p5 -- p4
+  p6 -- p5
+  p7 -- p6
+  p8 -- p7
+  p9 -- p8
+  p10-- p9
+  p11-- p10
+
+  p1 -- p3 -- p5 -- p7 -- p9 -- p11
+  p0 -- p2 -- p4 -- p6 -- p8 -- p10
+}
diff --git a/test/ghosh/ghosh14.dot b/test/ghosh/ghosh14.dot
new file mode 100644
index 0000000000000000000000000000000000000000..d20899037fbe35d071199ec75a9ca9701c4129fa
--- /dev/null
+++ b/test/ghosh/ghosh14.dot
@@ -0,0 +1,35 @@
+graph g {
+
+
+  p0 [algo="p0.ml"]
+  p1 [algo="p_even.ml"]
+  p2 [algo="p_odd.ml"]
+  p3 [algo="p_even.ml"]
+  p4 [algo="p_odd.ml"]
+  p5 [algo="p_even.ml"]
+  p6 [algo="p_odd.ml"]
+  p7 [algo="p_even.ml"]
+  p8 [algo="p_odd.ml"]
+  p9 [algo="p_even.ml"]
+  p10 [algo="p_odd.ml"]
+  p11 [algo="p_even.ml"]
+  p12 [algo="p_odd.ml"]
+  p13 [algo="p_last.ml"]
+
+  p1 -- p0
+  p2 -- p1
+  p3 -- p2
+  p4 -- p3
+  p5 -- p4
+  p6 -- p5
+  p7 -- p6
+  p8 -- p7
+  p9 -- p8
+  p10-- p9
+  p11-- p10
+  p12-- p11
+  p13-- p12
+
+  p1 -- p3 -- p5 -- p7 -- p9 -- p11 -- p13
+  p0 -- p2 -- p4 -- p6 -- p8 -- p10 -- p12
+}
diff --git a/test/ghosh/ghosh2.dot b/test/ghosh/ghosh2.dot
new file mode 100644
index 0000000000000000000000000000000000000000..69d8b47dcdb8551092581db9160968ed1e38ae2e
--- /dev/null
+++ b/test/ghosh/ghosh2.dot
@@ -0,0 +1,8 @@
+graph g {
+
+
+  p0 [algo="p0.ml"]
+  p1 [algo="p_last.ml"]
+
+  p1 -- p0
+}
diff --git a/test/ghosh/ghosh4.dot b/test/ghosh/ghosh4.dot
new file mode 100644
index 0000000000000000000000000000000000000000..3722181cf2ac75562c9269bf11ee690c8ac07a55
--- /dev/null
+++ b/test/ghosh/ghosh4.dot
@@ -0,0 +1,15 @@
+graph g8 {
+
+
+  p0 [algo="p0.ml"]
+  p1 [algo="p_even.ml"]
+  p2 [algo="p_odd.ml"]
+  p3 [algo="p_last.ml"]
+
+  p1 -- p0
+  p2 -- p1
+  p3 -- p2
+
+  p1 -- p3
+  p0 -- p2
+}
diff --git a/test/ghosh/ghosh6.dot b/test/ghosh/ghosh6.dot
new file mode 100644
index 0000000000000000000000000000000000000000..25b51570f8ebfd6833fa7eef9cd4c38b12e2cf5b
--- /dev/null
+++ b/test/ghosh/ghosh6.dot
@@ -0,0 +1,19 @@
+graph g8 {
+
+
+  p0 [algo="p0.ml"]
+  p1 [algo="p_even.ml"]
+  p2 [algo="p_odd.ml"]
+  p3 [algo="p_even.ml"]
+  p4 [algo="p_odd.ml"]
+  p5 [algo="p_last.ml"]
+
+  p1 -- p0
+  p2 -- p1
+  p3 -- p2
+  p4 -- p3
+  p5 -- p4
+
+  p1 -- p3 -- p5
+  p0 -- p2 -- p4
+}
diff --git a/test/ghosh/ghosh8.dot b/test/ghosh/ghosh8.dot
new file mode 100644
index 0000000000000000000000000000000000000000..9a9f6aac2907c4777f1be1289f22f95180c09e19
--- /dev/null
+++ b/test/ghosh/ghosh8.dot
@@ -0,0 +1,23 @@
+graph g8 {
+
+
+  p0 [algo="p0.ml"]
+  p1 [algo="p_even.ml"]
+  p2 [algo="p_odd.ml"]
+  p3 [algo="p_even.ml"]
+  p4 [algo="p_odd.ml"]
+  p5 [algo="p_even.ml"]
+  p6 [algo="p_odd.ml"]
+  p7 [algo="p_last.ml"]
+
+  p1 -- p0
+  p2 -- p1
+  p3 -- p2
+  p4 -- p3
+  p5 -- p4
+  p6 -- p5
+  p7 -- p6
+
+  p1 -- p3 -- p5 --p7
+  p0 -- p2 -- p4 -- p6
+}
diff --git a/test/ghosh/p0.ml b/test/ghosh/p0.ml
new file mode 100644
index 0000000000000000000000000000000000000000..09dd55a8949bba6f919adec91ae0e4e2d724b26a
--- /dev/null
+++ b/test/ghosh/p0.ml
@@ -0,0 +1,25 @@
+(* Time-stamp: <modified the 31/05/2023 (at 16:51) by Erwan Jahier> *)
+
+(* The Ghosh mutual exclusion algo: first node (a.k.a., bottom machine)
+
+Sukumar Ghosh, Binary self-stabilization in distributed systems,
+Information Processing Letters, Volume 40, Issue 3, 1991,Pages 153-159,
+ISSN 0020-0190, https://doi.org/10.1016/0020-0190(91)90172-E.  *)
+
+open Algo
+open State
+
+let (init_state: int -> string -> t) =
+  fun _ _ -> { s = (Random.bool ()) ; kind = Bottom }
+
+let (enable_f: t -> t neighbor list -> action list) =
+  fun s0 nl ->
+  let state n = (Algo.state n).s in
+  let s0 = s0.s in
+    match nl with
+    | [s1] | [s1; _]  -> if s0 = not (state s1)  then ["a"] else []
+    | _ ->  failwith "invalid topology"
+
+let (step_f : t -> t neighbor list -> action -> t ) =
+  fun s0 _nl _ ->
+  { s0 with s = not s0.s }
diff --git a/test/ghosh/p_even.ml b/test/ghosh/p_even.ml
new file mode 100644
index 0000000000000000000000000000000000000000..1760d8f686f8508d202c9f6ad99014140c2262fa
--- /dev/null
+++ b/test/ghosh/p_even.ml
@@ -0,0 +1,25 @@
+(* Time-stamp: <modified the 31/05/2023 (at 16:51) by Erwan Jahier> *)
+
+(* The Ghosh mutual exclusion algo: even nodes (a.k.a., y-machines)
+
+Sukumar Ghosh, Binary self-stabilization in distributed systems,
+Information Processing Letters, Volume 40, Issue 3, 1991,Pages 153-159,
+ISSN 0020-0190, https://doi.org/10.1016/0020-0190(91)90172-E.  *)
+
+open Algo
+open State
+
+let (init_state: int -> string -> t) =
+  fun _ _ -> { s = (Random.bool ()) ; kind = Even }
+
+let (enable_f: t -> t neighbor list -> action list) =
+  fun s1 nl ->
+  let state n = (Algo.state n).s in
+  let s1 = s1.s in
+    match List.map state nl with
+    | [s0; s2; s3] | [_;s0; s2; s3] -> if s0 = s1 && s1 = s2 && s3 = not s0  then ["a"] else []
+    | _ ->  failwith "invalid topology"
+
+let (step_f : t -> t neighbor list -> action -> t ) =
+  fun s0 _nl _ ->
+  { s0 with s = not s0.s }
diff --git a/test/ghosh/p_last.ml b/test/ghosh/p_last.ml
new file mode 100644
index 0000000000000000000000000000000000000000..c6c210b3c3a3f5faf4f865edf7d960ffe92450af
--- /dev/null
+++ b/test/ghosh/p_last.ml
@@ -0,0 +1,25 @@
+(* Time-stamp: <modified the 31/05/2023 (at 16:51) by Erwan Jahier> *)
+
+(* The Ghosh mutual exclusion algo: last node (a.k.a., top machine)
+
+Sukumar Ghosh, Binary self-stabilization in distributed systems,
+Information Processing Letters, Volume 40, Issue 3, 1991,Pages 153-159,
+ISSN 0020-0190, https://doi.org/10.1016/0020-0190(91)90172-E.  *)
+
+open Algo
+open State
+
+let (init_state: int -> string -> t) =
+  fun _ _ -> { s = (Random.bool ()) ; kind = Top }
+
+let (enable_f: t -> t neighbor list -> action list) =
+  fun s2 nl ->
+  let state n = (Algo.state n).s in
+  let s2 = s2.s in
+    match nl with
+    | [_;s1] | [s1] -> if s2 = state s1 then ["a"] else []
+    | _ ->  failwith "invalid topology"
+
+let (step_f : t -> t neighbor list -> action -> t ) =
+  fun s0 _nl _ ->
+  { s0 with s = not s0.s }
diff --git a/test/ghosh/p_odd.ml b/test/ghosh/p_odd.ml
new file mode 100644
index 0000000000000000000000000000000000000000..39df34f5b6fc1ec9c68c654632f17b3b36a5d2d3
--- /dev/null
+++ b/test/ghosh/p_odd.ml
@@ -0,0 +1,27 @@
+(* Time-stamp: <modified the 31/05/2023 (at 16:52) by Erwan Jahier> *)
+
+(* The Ghosh mutual exclusion algo: odd nodes (a.k.a., x-machines)
+
+Sukumar Ghosh, Binary self-stabilization in distributed systems,
+Information Processing Letters, Volume 40, Issue 3, 1991,Pages 153-159,
+ISSN 0020-0190, https://doi.org/10.1016/0020-0190(91)90172-E.  *)
+
+open Algo
+open State
+
+let (init_state: int -> string -> t) =
+  fun _ _ -> { s = (Random.bool ()) ; kind = Odd }
+
+
+let (enable_f: t -> t neighbor list -> action list) =
+  fun s2 nl ->
+  let state n = (Algo.state n).s in
+  let s2 = s2.s in
+    match List.map state nl with
+    | [s0; s1; s3] | [s0; s1; s3; _] -> if s0=s1 && s1 = s3 && s2 = not s0  then ["a"] else []
+    | _ ->  failwith "invalid topology"
+
+
+let (step_f : t -> t neighbor list -> action -> t ) =
+  fun s0 _nl _ ->
+  { s0 with s = not s0.s }
diff --git a/test/ghosh/state.ml b/test/ghosh/state.ml
new file mode 100644
index 0000000000000000000000000000000000000000..095654b2d267cbd57cbe639d360ef0536bfb642a
--- /dev/null
+++ b/test/ghosh/state.ml
@@ -0,0 +1,11 @@
+
+(* It  is necessary to be  able to distinguish between  node kinds to
+   define the legitimate predicate
+*)
+type node_kind = Bottom | Odd | Even | Top
+type t = { s : bool; kind : node_kind }
+
+let to_string = (fun s -> Printf.sprintf "%b" s.s)
+let of_string = Some (fun _ -> failwith "not yet implemented")
+let copy x = x
+let actions = ["a"]