add new Cycle_Unison expériment

test/Cycle_unison/Makefile

+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

test/Cycle_unison/Sh/search_config.sh

+#!/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

test/Cycle_unison/config.ml

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

test/Cycle_unison/state.lus

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

test/Cycle_unison/state.ml

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

test/Cycle_unison/unison.lus

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

test/Cycle_unison/unison.ml

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

test/Cycle_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;
+  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;

test/Cycle_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,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