add the unison example, is legitimate state and the diameter constant.

lib/sas.lus

@@ -8,6 +8,13 @@ let
 	y = boolnone<<pn>>(map<<boolany<<an>>, pn>>(enab));
 tel;
 
+-- All nodes enabled.
+function all_active<<const an:int; const pn:int>>(enab: bool^an^pn)
+returns (y : bool);
+let
+        y = boolall<<pn>>(map<<boolany<<an>>, pn>>(enab));
+tel;
+
 -- Any activation Ai implies Ei was previously enabled.
 node activation_is_valid<<const an:int>>(acti, enab : bool^an) returns (y : bool);
 let

lib/utils.lus

@@ -50,6 +50,14 @@ let
 	    else (not member<<T,N-1>>(A[0], A[1 .. N-1])) and
 	         all_different<<T,N-1>>(A[1 .. N-1]);
 tel;
+
+-- All element have the same value.
+function same_value <<const N:int>>(T: int^N)
+returns (y : bool);
+let
+  y = boolred<<N,N,N>>(map<< = , N >>( T , (T[1..N-1] | [T[0]]) ));
+tel;
+
 function mini(x,y:int) returns (z:int);
 let
  z = if x < y then x else y;

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);

test/unison/Makefile

+TOPOLOGY ?= ring3
+DOT2LUSFLAGS ?=
+SASA_ALGOS := unison.ml
+DECO_PATTERN="0-:unison.ml"
+
+
+include ../Makefile.inc
+-include ../Makefile.dot
+
+clean: genclean
+	rm -f $(TOPOLOGY)*.*
+
+## Some examples of use of ../Makefile.inc
+
+
+# run a simulation with luciole
+simu: $(TOPOLOGY).simu
+
+# Compare the ocaml version with the lustre one 
+compare: $(TOPOLOGY).lurette
+	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

test/unison/config.ml

+../../../test/unison/config.ml
\ No newline at end of file

test/unison/state.ml

+../../../test/unison/state.ml
\ No newline at end of file

test/unison/unison.lus

+type state = int;
+
+type action = enum { T };
+const actions_number = 1;
+const m = 2*diameter -1;
+
+function action_of_int(i : int) returns (a : action);
+let
+  a = T;
+tel;
+
+function min_clock<<const n:int>> (this : int; neighbors : int^n)
+returns (new: int);
+var min:int;
+let
+  min = if this <= neighbors[0] then this else 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 : int^n)
+returns (new: state);
+let
+  new = (min_clock<<n>>(this,neighbors)+1) mod m;
+tel
+ 
+function unison_enable<<const degree:int>> (this : state; neighbors : state^degree)
+returns (enabled : bool^actions_number);
+let
+  enabled= [ this <> (newClockValue<<degree>>(this,neighbors)) ];
+tel;
+
+function unison_step<<const degree:int>>(
+  this : state;
+  neighbors : state^degree; action : action)
+returns (new : state);
+let
+  new = newClockValue<<degree>>(this,neighbors);
+tel;

test/unison/unison.ml

+../../../test/unison/unison.ml
\ No newline at end of file

test/unison/unison_oracle.lus

+
+-- 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;                   
+) 
+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
+             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;
+          -- compare the lustre and the ocaml version of the processes
+tel;
+

test/unison/verify.lus

+include "../../lib/sas.lus"
+
+node verify(activations : bool^actions_number^card; inits : state^card) returns (ok : bool);
+var nb_step: int;
+var config : state^card;
+var enables : bool^actions_number^card;
+var legitimate, closure : bool;
+let
+	assert(true -> daemon_is_synchronous<<actions_number,card>>(activations, pre enables));
+        assert(rangei<<0,card>>(inits));   
+
+	config, enables = topology(activations, inits);
+
+	legitimate = same_value<<card>>(config);
+	closure = true -> (pre(legitimate) => legitimate);
+	nb_step = 0 -> pre(nb_step) + 1;
+
+	-- verify that the execution terminates after at most |N|−1 moves:
+	ok = closure
+             and (nb_step>=(3*diameter-2) => legitimate)
+;
+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;
+let
+   ranges_min = map<< <= , card>>(low^card, c);
+   ranges_max = map<< < , card>>(c, card^card);
+   res = boolall<<card>>(ranges_min) and boolall<<card>>(ranges_max);
+tel