add unison

test/unison/Makefile

+TOPOLOGY ?= ring3
+DOT2LUSFLAGS ?=
+SASA_ALGOS := p.ml
+SASAFLAGS += --locally-central-daemon
+DECO_PATTERN="0-:p.ml"
+
+include ../Makefile.inc
+-include ../Makefile.dot
+
+clean: genclean
+	rm -f ring*.* er*.* grid*.* 
+
+.PRECIOUS: %.lus
+.PRECIOUS: %.dot
+
+## Some examples of use of ../Makefile.inc
+
+
+# run a simulation with luciole
+simu: ring3.simu
+
+# Compare the ocaml version with the lustre one
+# XXX todo : write a coloring_oracle.lus similar to ../dijkstra-ring/dijkstra_ring_oracle.lus
+compare: ring3.lurette
+	cat unisson.rif
+
+# make clique3.simu
+kind2: ring3.kind2
+
+## do not work because there is a modulo in p.lus, which is not (yet) implemented in ../../bit-blast/*.lus
+lesar: ring3.lesar

test/unison/config.ml

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

test/unison/p.lus

+type state=int;
+type action=enum{g};
+const actions_number=1;
+const m= diameter;
+
+function action_of_int (i:int) returns (a:action);
+let
+a=g;
+tel
+
+function min <<const degree:int>> (nl:state^degree) returns (n:state);
+let
+n= with (degree=1) then nl[0]
+   else if nl[0] < (min <<degree-1>> (nl[1..(degree-1)])) then nl[0] else 
+         min <<degree-1>> (nl[1..(degree-1)]);
+tel
+
+function newclockvalue<<const degree:int>>(p:state ; nl:state^degree) returns (pnew:state);
+let
+pnew= if p < (min <<degree>>(nl)) then (p + 1) mod m else ((min <<degree>>(nl))+1) mod m ;
+tel 
+
+function p_enable <<const degree:int>>(p:state ; nl:state^degree) returns 
+(a:bool^actions_number);
+let
+a= [p<> (newclockvalue <<degree>>(p,nl))];
+tel
+
+function p_step  <<const degree:int>>(p:state ; nl:state^degree; a:action) returns (pc:state);
+let
+pc= (newclockvalue <<degree>>(p,nl)) ;
+tel

test/unison/p.ml

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

test/unison/state.ml

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

test/unison/unisson_oracle.lus

+include "../../lib/utils.lus"
+
+node _unisson_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
+       
+         -- compare the cost functions 
+tel
+
+node unisson_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
+    ok= lustre_enabled[0][0] or true;
+   lustre_config, lustre_enabled = 
+    topology(active -> pre active, -- ignored at the first step
+             ocaml_config -- used at the first step only
+             );
+tel 
\ No newline at end of file

test/unison/verify.lus

+include "../../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;
+	moves : int;
+        pot :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);
+	moves = move_count<<actions_number,card>>(activations);
+
+  pot = pop_count<<card>>(map<<n_or<<actions_number>>, card>>(enables));
+
+	-- 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 (moves >= card => 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