diff --git a/src/dot2lus.ml b/src/dot2lus.ml
index 5ccbad4830cd19e4cbdf87dd5c378f02ca81b193..5a2c38c493d9fb1657c8a48b2c493695f176aa0d 100644
--- a/src/dot2lus.ml
+++ b/src/dot2lus.ml
@@ -47,6 +47,7 @@ let output_prelude lustre_topology lustre_const (graph : Topology.t) =
  Printf.fprintf lustre_const "const max_degree = %d;\n" dmax;
  Printf.fprintf lustre_const "const min_degree = %d;\n" dmin;
  Printf.fprintf lustre_const "const mean_degree = %f;\n" (Topology.get_mean_degree graph);
+ Printf.fprintf lustre_const "const diameter = %d;\n" (Diameter.get graph);
  Printf.fprintf lustre_const "const is_directed = %b;\n" graph.directed;
  Printf.fprintf lustre_const "const is_cyclic = %b;\n" (Topology.is_cyclic graph);
  Printf.fprintf lustre_const "const is_connected = %b;\n" (Topology.is_connected graph);
@@ -58,6 +59,7 @@ let output_prelude lustre_topology lustre_const (graph : Topology.t) =
   | "max_degree"
   | "min_degree"
   | "mean_degree"
+  | "diameter"
   | "is_directed"
   | "is_cyclic"
   | "is_connected"
@@ -122,16 +124,19 @@ let output_topology lustre_topology (graph : Topology.t) name =
   name action_number state_type;
  
  Printf.fprintf lustre_topology
-  "returns (p_c : %s^card; Enab_p : bool^%s^card);\n"
+  "returns (p_c : %s^card; Enab_p : bool^%s^card; round:bool; round_nb:int);\n"
   state_type action_number;
  
- output_string lustre_topology "var\n";
+ output_string lustre_topology "var";
  
  Printf.fprintf lustre_topology "\tprev_p_c : %s^card;\n\n" state_type;
  graph.nodes
  |> List.iteri (fun i _ -> Printf.fprintf lustre_topology "\tsel_%d : bool;\n" i);
  
- output_string lustre_topology "let\n";
+ output_string lustre_topology "let
+    round = round<<actions_number,card>>(Enab_p, p);
+    round_nb = round_count(round, silent<<actions_number,card>>(Enab_p));
+";
  
  output_string lustre_topology "\tprev_p_c = initials -> pre(p_c);\n\n";
  graph.nodes
diff --git a/test/Makefile.inc b/test/Makefile.inc
index 9713d0bf5502fb0d2e13e57a5518f687647c624a..aaa0b1702b1071c1dcb25958a4c5f2c90e5cc112 100644
--- a/test/Makefile.inc
+++ b/test/Makefile.inc
@@ -22,7 +22,7 @@ genclean:
 	rm -f *.rif *.seed
 	rm -f $(TOPOLOGY).lus
 	rm -f *_verify.lv4
-	rm -f *.c *.h *_const.lus *.cmt *.exec *.sh
+	rm -f *.c *.h *_const.lus *.cmt *.exec *.sh rdbg-session* *.log *.pdf
 
 # generating lv6 files of out dot files
 %_const.lus: %.dot
@@ -31,6 +31,9 @@ genclean:
 
 LIB=-package algo
 OCAMLOPT=ocamlfind ocamlopt -bin-annot
+LIB_LUS=$(HOME)/sasa/test/lustre/round.lus $(HOME)/sasa/salut/lib/sas.lus
+
+# $(HOME)/sasa/test/lustre/oracle_utils.lus 
 
 
 ##########################################################################################"
@@ -38,14 +41,19 @@ OCAMLOPT=ocamlfind ocamlopt -bin-annot
 
 %.simu:
 	make $*.dot $*_const.lus
-	luciole-rif lv6 $*.lus $*_const.lus -n $* -exec 
+	luciole-rif lv6 $(LIB_LUS) $*.lus $*_const.lus -n $* -exec 
+
+%.rdbg:
+	make $*.dot $*_const.lus
+	rdbgui4sasa -sut-nd "lv6 $(LIB_LUS) $*_const.lus $*.lus  -n $* -exec"
 
 ##########################################################################################"
 # Use lurette to compare the lustre and the ocaml version of the algorithm
+# nb : <dirname>/<dirname>_oracle.lus should be written
 
-%.lurette:
-	make $*.dot $*_const.lus $*.cmxs $*_oracle.lus
-	lurette -sut "sasa $*.dot $(SASAFLAGS)" -oracle "lv6 $*.lus $*_oracle.lus -n oracle -2c-exec"
+%.lurette:  %_oracle.lus
+	make $*.dot $*_const.lus $*.cmxs
+	lurette -sut "sasa -seed 4 $*.dot $(SASAFLAGS)" -oracle "lv6  $(LIB_LUS) $*.lus $*_oracle.lus -n oracle -2c-exec"
 
 %.cmxs: %.ml
 	$(OCAMLOPT) $(LIB) -shared state.ml $(shell sasa -algo $*.dot) config.ml $< -o $@
@@ -65,7 +73,7 @@ prop = verify
 endif
 
 %.expand.kind2: %_verify.lv4
-	time kind2  $<
+	time kind2  --modular true --compositional true $<
 
 %.kind2: %.dot
 	make $*_verify.noexpand.lv4
@@ -74,13 +82,13 @@ endif
 
 # XXX: this method of adding kind2 annotations is brittle
 %_verify.lv4: %.lus %_const.lus  verify.lus
-	lv6 $^ -n $(prop) --lustre-v4 -en -o $@
+	lv6 $(LIB_LUS) $*.lus $^ $*_const.lus -n $(prop) --lustre-v4 -en -o $@
 	sed -i -e "s/tel/--%MAIN ;\n--%PROPERTY ok;\ntel/" $@
 
 # Do not expand nodes 
 %_verify.noexpand.lv4:  verify.lus
 	make $*_const.lus
-	lv6 $*.lus $^ $*_const.lus -n $(prop) -rnc --lustre-v4 -o $@
+	lv6 $(LIB_LUS) $*.lus $^ $*_const.lus -n $(prop) -rnc --lustre-v4 -o $@
 	tac $@ | sed  -z "s/tel/tel\n--%MAIN ;\n--%PROPERTY ok;/" | tac > $@.tmp
 	mv $@.tmp $@
 
@@ -90,7 +98,7 @@ endif
 # to use lesar, perform bit-blasting via ec2ec -usrint
 %_verify.ec: %.dot verify.lus
 	make $*_const.lus
-	lv6 $*.lus $*_const.lus verify.lus -n $(prop) -ec -o $@.tmp
+	lv6  $(LIB_LUS) $*.lus $*_const.lus verify.lus -n $(prop) -ec -o $@.tmp
 	echo "include \"../../lib/bit-blast/signed_binary5.lus\"" > $@.tmp2
 	echo "include \"../../lib/bit-blast/binary.lus\"" >> $@.tmp2
 	ec2ec -usrint $@.tmp >> $@.tmp2
diff --git a/test/coloring/Makefile b/test/coloring/Makefile
index 1022a28faca57c0710714ca130d6b8102983a919..952d8bca338163b4c9b098928e1698e4d7076bf2 100644
--- a/test/coloring/Makefile
+++ b/test/coloring/Makefile
@@ -7,8 +7,13 @@ DECO_PATTERN="0-:p.ml"
 include ../Makefile.inc
 -include ../Makefile.dot
 
+##############################################################################
+# Non-regression tests
+
+test: clique3.kind2 clique3.lesar #  clique3.lurette 
+
 clean: genclean
-	rm -f ring*.* er*.* grid*.* 
+	rm -f ring*.* er*.* grid*.* clique*.*
 
 .PRECIOUS: %.lus
 .PRECIOUS: %.dot
@@ -24,8 +29,6 @@ simu: clique3.simu
 #compare: clique3.lurette
 #	cat dijkstra-ring.rif
 
-# make clique3.simu
 kind2: clique3.kind2
 
-## do not work because there is a modulo in p.lus, which is not (yet) implemented in ../../bit-blast/*.lus
 lesar: clique3.lesar
diff --git a/test/coloring/clique3.dot b/test/coloring/clique3.dot
deleted file mode 100644
index 1672a3b5fc62988ec103c8229c36296c538160eb..0000000000000000000000000000000000000000
--- a/test/coloring/clique3.dot
+++ /dev/null
@@ -1,12 +0,0 @@
-graph graph0 {
-graph [min_deg=2 mean_deg=2. max_deg=2 is_connected=true is_cyclic=true is_tree=false links_number=3]
-  p0 [algo="p.ml"]
-  p1 [algo="p.ml"]
-  p2 [algo="p.ml"]
-
-
-  p0 -- p1
-  p0 -- p2
-  p1 -- p2
-}
-
diff --git a/test/coloring/clique3_oracle.lus b/test/coloring/clique3_oracle.lus
deleted file mode 100644
index 42222151ac27b36aa6585a2c26ba1db5b7072bc5..0000000000000000000000000000000000000000
--- a/test/coloring/clique3_oracle.lus
+++ /dev/null
@@ -1,26 +0,0 @@
-include "clique3.lus"
-include "verify.lus"
-
-node topology = clique3;
-const an = actions_number;
-const pn = card;
-
-node oracle(
-	p0_color:int;p1_color:int;p2_color:int;
-	Enab_p0_recolor,Enab_p1_recolor,Enab_p2_recolor:bool;
-	p0_recolor,p1_recolor,p2_recolor:bool)
-returns (ok:bool);
-var
-	Acti:bool^an^pn;
-	Enab:bool^an^pn;
-	Stat : state^pn;
-	nodes : state^pn;
-	enables : bool^an^pn;
-let
-	Acti = [[p0_recolor],[p1_recolor],[p2_recolor]];
-	Enab = [[Enab_p0_recolor],[Enab_p1_recolor],[Enab_p2_recolor]];
-	Stat = [ p0_color, p1_color, p2_color ];
-
-	nodes, enables = topology(pre(Acti), Stat);
-	ok = enables = Enab and boolred<<pn,pn,pn>>(map<<=,pn>>(nodes, Stat));
-tel
diff --git a/test/coloring/verify.lus b/test/coloring/verify.lus
index 4ca7b836163d2198cccf29b85c6f321167f6ee22..7c98d767d0a714b5f488f34f860bc29836a9c2af 100644
--- a/test/coloring/verify.lus
+++ b/test/coloring/verify.lus
@@ -7,12 +7,13 @@ var
 	legitimate, closure : bool;
 	moves : int;
         pot :int;
+  r:bool;rn: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);
+	config, enables,r,rn = topology(activations, inits);
 
 	legitimate = silent<<actions_number,card>>(enables);
 	closure = true -> (pre(legitimate) => legitimate);
diff --git a/test/dijkstra-ring/Makefile b/test/dijkstra-ring/Makefile
index 6b4f54edb15a5aac076c7a17b5164d6fdf880fb2..747d395c6339e9ad5b00344db340baa3f05cfb67 100644
--- a/test/dijkstra-ring/Makefile
+++ b/test/dijkstra-ring/Makefile
@@ -7,11 +7,18 @@ DECO_PATTERN="0:root.ml 1-:p.ml"
 include ../Makefile.inc
 -include ../Makefile.dot
 
+##############################################################################
+# Non-regression tests
+
+test: diring4.lurette diring4.kind2
+
 clean: genclean
 	rm -f diring*.*
 
-## Some examples of use of ../Makefile.inc
+##############################################################################
+# Other examples of use
 
+## Some examples of use of ../Makefile.inc
 
 # run a simulation with luciole
 simu: diring4.simu
diff --git a/test/dijkstra-ring/dijkstra_ring_oracle.lus b/test/dijkstra-ring/dijkstra_ring_oracle.lus
index c71f7b8a69366a4228320cc62473d0ffbf87ca62..c870b89df7ca391f4d45c52bee952c67521ae152 100644
--- a/test/dijkstra-ring/dijkstra_ring_oracle.lus
+++ b/test/dijkstra-ring/dijkstra_ring_oracle.lus
@@ -4,20 +4,25 @@
 include "../../lib/utils.lus"
 include "cost.lus"
 
-node _dijkstra_ring_oracle(
+node dijkstra_ring_oracle(
   legitimate : bool;
   ocaml_cost : real;
   ocaml_enabled : bool^actions_number^card;
   active : bool^actions_number^card; 
-  ocaml_config : state^card;                   
+  ocaml_config : state^card;
+  round:bool;
+  round_nb:int;
 ) 
-returns (ok : bool);
+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_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
              );
@@ -26,11 +31,14 @@ let
            -- 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::real2int(ocaml_cost) = lustre_cost
+       and round = lustre_round
+       and round_nb = lustre_round_nb
+;
          -- compare the cost functions 
 tel
 
-node dijkstra_ring_oracle(
+node _dijkstra_ring_oracle(
   legitimate : bool;
   ocaml_cost : real;
   ocaml_enabled : bool^actions_number^card;
@@ -41,9 +49,11 @@ returns (ok : bool);
 var
   lustre_config : state^card;
   lustre_enabled : bool^actions_number^card;
+  lustre_round:bool; 
+  lustre_round_nb:int;
 let
     ok= lustre_enabled[0][0] or true;
-   lustre_config, lustre_enabled = 
+   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
              );
diff --git a/test/dijkstra-ring/verify.lus b/test/dijkstra-ring/verify.lus
index d38ce87b8d3a3b94379d96fcd1b44af8241b116c..59e96fe29dcc6045610865d6951751b1691a7b06 100644
--- a/test/dijkstra-ring/verify.lus
+++ b/test/dijkstra-ring/verify.lus
@@ -14,12 +14,13 @@ var
   enabled : bool^actions_number^card;
   legitimate, at_least_1, closure, converge : bool;
   steps, cost : int;
+  round:bool; round_nb:int;
 let
 	assert(true -> daemon_is_distributed<<actions_number,card>>(active, pre enabled));
 --	assert(true -> daemon_is_synchronous<<actions_number,card>>(active, pre enabled));
         assert(rangei<<0,card>>(init_config));   
 
-	config, enabled = topology(active, init_config);
+	config, enabled, round, round_nb = topology(active, init_config);
         assert(config = init_config -> true);
 
 	-- stability in this algo means mutual exclusion: exactly 1 node is enabled at a time