From 6e775acb8d1c89afab21f03c4f7cc19e5c362711 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr>
Date: Thu, 21 Jul 2022 17:54:15 +0200
Subject: [PATCH] refactor: minor file name changes
---
test/Cycle_unison/Makefile | 42 +------------------
.../{verify.lus => check_cycles.lus} | 2 +-
test/Cycle_unison/state.lus | 18 +-------
test/Cycle_unison/unison.lus | 35 +---------------
test/Cycle_unison/unison_oracle.lus | 32 --------------
test/unison/Makefile | 6 +++
test/unison/k.lus | 2 +
test/unison/unison.lus | 3 +-
8 files changed, 13 insertions(+), 127 deletions(-)
mode change 100644 => 120000 test/Cycle_unison/Makefile
rename test/Cycle_unison/{verify.lus => check_cycles.lus} (95%)
mode change 100644 => 120000 test/Cycle_unison/state.lus
mode change 100644 => 120000 test/Cycle_unison/unison.lus
delete mode 100644 test/Cycle_unison/unison_oracle.lus
create mode 100644 test/unison/k.lus
diff --git a/test/Cycle_unison/Makefile b/test/Cycle_unison/Makefile
deleted file mode 100644
index d78ba7b6..00000000
--- 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 00000000..6a67edd0
--- /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 eeaad435..db500c38 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 75a2c8ac..00000000
--- 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 00000000..226b86a2
--- /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 173f720c..00000000
--- 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 00000000..d0c34394
--- /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 ac39af1e..00000000
--- 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 d63959d4..696e9a1c 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 00000000..ffecb5d6
--- /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 9f43f86f..7daf4a10 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);
--
GitLab