diff --git a/test/Cycle_unison/Makefile b/test/Cycle_unison/Makefile deleted file mode 100644 index d78ba7b61a9ae253f560f1618e75e6ab92f8f975..0000000000000000000000000000000000000000 --- a/test/Cycle_unison/Makefile +++ /dev/null @@ -1,41 +0,0 @@ -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 diff --git a/test/Cycle_unison/Makefile b/test/Cycle_unison/Makefile new file mode 120000 index 0000000000000000000000000000000000000000..6a67edd0c6ce2c3ce3847291aaa7d9fae10d3d6c --- /dev/null +++ b/test/Cycle_unison/Makefile @@ -0,0 +1 @@ +../unison/Makefile \ No newline at end of file diff --git a/test/Cycle_unison/verify.lus b/test/Cycle_unison/check_cycles.lus similarity index 95% rename from test/Cycle_unison/verify.lus rename to test/Cycle_unison/check_cycles.lus index eeaad4352a607d0795b0c923c0a266d61b4f63a7..db500c38e830d24491725c03eafa7ba84cd535ac 100644 --- a/test/Cycle_unison/verify.lus +++ b/test/Cycle_unison/check_cycles.lus @@ -2,7 +2,7 @@ include "../../lib/sas.lus" -node verify(activations : bool^actions_number^card; inits : state^card) returns (ok : bool); +node check_cycles(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; diff --git a/test/Cycle_unison/state.lus b/test/Cycle_unison/state.lus deleted file mode 100644 index 75a2c8acae6504e68e84d3a365c94322322faedd..0000000000000000000000000000000000000000 --- a/test/Cycle_unison/state.lus +++ /dev/null @@ -1,17 +0,0 @@ --- 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; diff --git a/test/Cycle_unison/state.lus b/test/Cycle_unison/state.lus new file mode 120000 index 0000000000000000000000000000000000000000..226b86a299064c8d85a7598c7411e8c52777e517 --- /dev/null +++ b/test/Cycle_unison/state.lus @@ -0,0 +1 @@ +../unison/state.lus \ No newline at end of file diff --git a/test/Cycle_unison/unison.lus b/test/Cycle_unison/unison.lus deleted file mode 100644 index 173f720cc0ff7915592ca45447b94679faef780a..0000000000000000000000000000000000000000 --- a/test/Cycle_unison/unison.lus +++ /dev/null @@ -1,34 +0,0 @@ -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; diff --git a/test/Cycle_unison/unison.lus b/test/Cycle_unison/unison.lus new file mode 120000 index 0000000000000000000000000000000000000000..d0c343947c9412b94449a41e8e1760f0a3909cb3 --- /dev/null +++ b/test/Cycle_unison/unison.lus @@ -0,0 +1 @@ +../unison/unison.lus \ No newline at end of file diff --git a/test/Cycle_unison/unison_oracle.lus b/test/Cycle_unison/unison_oracle.lus deleted file mode 100644 index ac39af1e697e4f4820ddb061c9334d84148fc3fc..0000000000000000000000000000000000000000 --- a/test/Cycle_unison/unison_oracle.lus +++ /dev/null @@ -1,32 +0,0 @@ --- 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; diff --git a/test/unison/Makefile b/test/unison/Makefile index d63959d42b49a88e2d5f8c09416572eb0cfbb17f..696e9a1c59feca9ae2c1ec927a0bae52253cbee1 100644 --- a/test/unison/Makefile +++ b/test/unison/Makefile @@ -35,3 +35,9 @@ 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 + +org: + echo "| Topology | n | k | inutile (car faux) | step | Resultat | time |" > resultat.org + echo "|-|" >> resultat.org + cat Log/*.org >> resultat.org + echo "|-|" >> resultat.org diff --git a/test/unison/k.lus b/test/unison/k.lus new file mode 100644 index 0000000000000000000000000000000000000000..ffecb5d682c0a21502b85752e69ad37add7d28ac --- /dev/null +++ b/test/unison/k.lus @@ -0,0 +1,2 @@ +const m0 = 2*diameter -1; +const k = if m0<2 then 2 else m0; diff --git a/test/unison/unison.lus b/test/unison/unison.lus index 9f43f86ffef98ceaa5ab15e5e8a1ebea0e73f356..7daf4a102b0ee65918d118e51396b2f37a5f110d 100644 --- a/test/unison/unison.lus +++ b/test/unison/unison.lus @@ -1,5 +1,4 @@ -const m0 = 2*diameter -1; -const k = if m0<2 then 2 else m0; +include "k.lus" function min_clock<<const n:int>> (this : int; neighbors : neigh^n) returns (new: int);