From 172243b333b57e60ccb182d4325092837ca4930c Mon Sep 17 00:00:00 2001
From: invite <invite@debian>
Date: Fri, 1 Jul 2022 10:00:39 +0200
Subject: [PATCH] add unison
---
test/unison/Makefile | 31 ++++++++++++++++++++++++
test/unison/config.ml | 1 +
test/unison/p.lus | 32 +++++++++++++++++++++++++
test/unison/p.ml | 1 +
test/unison/state.ml | 1 +
test/unison/unisson_oracle.lus | 44 ++++++++++++++++++++++++++++++++++
test/unison/verify.lus | 39 ++++++++++++++++++++++++++++++
7 files changed, 149 insertions(+)
create mode 100644 test/unison/Makefile
create mode 120000 test/unison/config.ml
create mode 100644 test/unison/p.lus
create mode 120000 test/unison/p.ml
create mode 120000 test/unison/state.ml
create mode 100644 test/unison/unisson_oracle.lus
create mode 100644 test/unison/verify.lus
diff --git a/test/unison/Makefile b/test/unison/Makefile
new file mode 100644
index 00000000..bfa5ea0c
--- /dev/null
+++ b/test/unison/Makefile
@@ -0,0 +1,31 @@
+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
diff --git a/test/unison/config.ml b/test/unison/config.ml
new file mode 120000
index 00000000..c5a3daf4
--- /dev/null
+++ b/test/unison/config.ml
@@ -0,0 +1 @@
+../../../test/unison/config.ml
\ No newline at end of file
diff --git a/test/unison/p.lus b/test/unison/p.lus
new file mode 100644
index 00000000..f85c2f31
--- /dev/null
+++ b/test/unison/p.lus
@@ -0,0 +1,32 @@
+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
diff --git a/test/unison/p.ml b/test/unison/p.ml
new file mode 120000
index 00000000..ff566f19
--- /dev/null
+++ b/test/unison/p.ml
@@ -0,0 +1 @@
+../../../test/unison/p.ml
\ No newline at end of file
diff --git a/test/unison/state.ml b/test/unison/state.ml
new file mode 120000
index 00000000..0d0c3082
--- /dev/null
+++ b/test/unison/state.ml
@@ -0,0 +1 @@
+../../../test/unison/state.ml
\ No newline at end of file
diff --git a/test/unison/unisson_oracle.lus b/test/unison/unisson_oracle.lus
new file mode 100644
index 00000000..e852c485
--- /dev/null
+++ b/test/unison/unisson_oracle.lus
@@ -0,0 +1,44 @@
+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
diff --git a/test/unison/verify.lus b/test/unison/verify.lus
new file mode 100644
index 00000000..0c4406c4
--- /dev/null
+++ b/test/unison/verify.lus
@@ -0,0 +1,39 @@
+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
--
GitLab