diff --git a/test/Makefile.inc b/test/Makefile.inc
index bb7781da9ed4e821b1a03d9dec75652c2058f163..06aff70275d6d5e473b95de497319c92301eaa78 100644
--- a/test/Makefile.inc
+++ b/test/Makefile.inc
@@ -1,4 +1,4 @@
-# Time-stamp: <modified the 05/07/2019 (at 15:18) by Erwan Jahier>
+# Time-stamp: <modified the 08/07/2019 (at 17:10) by Erwan Jahier>
DIR=../../_build/install/default
@@ -29,6 +29,6 @@ s:sim2chrogtk
clean:
rm -f *.cmxs sasa *.cm* *.o *.pdf *.rif *.gp *.log *.dro *.seed *.c sasa-*.dot
- rm -f rdbg-session*.ml luretteSession*.ml *.lut a.out
+ rm -f rdbg-session*.ml luretteSession*.ml *.lut a.out *.cov
##################################################################################
diff --git a/test/bfs-spanning-tree/Makefile b/test/bfs-spanning-tree/Makefile
index 3df7594730d0247afd5f28498075d9d45207ce27..f14aaa5e318316195bc165cc5e1d24f3c99047e3 100644
--- a/test/bfs-spanning-tree/Makefile
+++ b/test/bfs-spanning-tree/Makefile
@@ -1,4 +1,4 @@
-# Time-stamp: <modified the 05/07/2019 (at 15:30) by Erwan Jahier>
+# Time-stamp: <modified the 08/07/2019 (at 17:09) by Erwan Jahier>
test: test0 test2 lurette0 lurette1
@@ -36,13 +36,6 @@ lurette1:cmxs fig5.1.lut fig5.1_oracle.lus
-env "$(sasa) fig5.1.dot -dd -rif" \
-oracle "lv6 fig5.1_oracle.lus -n oracle"
-lemma5.16:cmxs fig5.1-noinit.lut
- rdbg -lurette -o lurette.rif \
- -env "$(sasa) fig5.1-noinit.dot -custd -rif" \
- -sut "lutin fig5.1-noinit.lut -n distributed" \
- -oracle "lv6 oracle_lemma5_16.lus -n oracle"
-
-
lurette: lurette0
sim2chrogtk -ecran -in lurette.rif > /dev/null
gnuplot-rif lurette.rif
diff --git a/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus b/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus
index 0077fb439b0655a62ea51c556a7e74039559471e..5c9ce4ae8f2cfc58c828d1e0403cee00c15d0e99 100644
--- a/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus
+++ b/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus
@@ -8,6 +8,7 @@ let
theorem_5_18<<an,pn>> (Enab, Acti);
tel
+-----------------------------------------------------------------------------
function first_element<<const an : int>> (X:bool^an) returns (res:bool);
let
res = X[0];
diff --git a/test/bfs-spanning-tree/fig5.1-noinit_oracle.lus b/test/bfs-spanning-tree/fig5.1-noinit_oracle.lus
index 285de9c6cbd028d97bd4bcc2caa1aff332adb6d3..5c81c8cda9cdd6fce8f994525bd96ec7ffdb1f8f 100644
--- a/test/bfs-spanning-tree/fig5.1-noinit_oracle.lus
+++ b/test/bfs-spanning-tree/fig5.1-noinit_oracle.lus
@@ -1,28 +1,36 @@
+-- Automatically generated by /home/jahier/sasa/_build/default/src/sasaMain.exe version "2.10.0" ("a331f5b")
+-- on crevetete the 8/7/2019 at 17:11:11
+--../../_build/install/default/bin/sasa -seed 42 -l 100 -glos fig5.1-noinit.dot
include "bfs_spanning_tree_oracle.lus"
+const an=2; -- actions number
+const pn=8; -- processes number
+const degree=3;
+const min_degree=2;
+const mean_degree=2.250000;
+const diameter=4;
+const card=8;
+const links_number=9;
+const is_cyclic=true;
+const is_connected=true;
+const is_a_tree=false;
+const adjency=[
+ [f,t,f,f,f,f,f,t],
+ [t,f,t,f,f,f,f,f],
+ [f,t,f,t,f,f,t,f],
+ [f,f,t,f,t,f,f,f],
+ [f,f,f,t,f,t,f,f],
+ [f,f,f,f,t,f,t,f],
+ [f,f,t,f,f,t,f,t],
+ [t,f,f,f,f,f,t,f]];
-const n=8;
-const m=2;
-const degree=2;
-const diameter=8;
-
-node oracle(root_CD,root_CP,p1_CD,p1_CP,p2_CD,p2_CP,p3_CD,p3_CP,p4_CD,p4_CP,p5_CD,p5_CP,
- p6_CD,p6_CP,p7_CD,p7_CP,
- Enab_root_CD,Enab_root_CP,Enab_p1_CD,Enab_p1_CP,Enab_p2_CD,Enab_p2_CP,
- Enab_p3_CD,Enab_p3_CP,Enab_p4_CD,Enab_p4_CP,Enab_p5_CD,Enab_p5_CP,
- Enab_p6_CD,Enab_p6_CP,Enab_p7_CD,Enab_p7_CP
- :bool)
-returns (ok:bool);
+node oracle(root_CD,root_CP,p1_CD,p1_CP,p2_CD,p2_CP,p3_CD,p3_CP,p4_CD,p4_CP,p5_CD,p5_CP,p6_CD,p6_CP,p7_CD,p7_CP,Enab_root_CD,Enab_root_CP,Enab_p1_CD,Enab_p1_CP,Enab_p2_CD,Enab_p2_CP,Enab_p3_CD,Enab_p3_CP,Enab_p4_CD,Enab_p4_CP,Enab_p5_CD,Enab_p5_CP,Enab_p6_CD,Enab_p6_CP,Enab_p7_CD,Enab_p7_CP:bool) returns (ok:bool);
var
Acti:bool^2^8;
Enab:bool^2^8;
let
- Acti = [[root_CD,root_CP],[p1_CD,p1_CP],[p2_CD,p2_CP],[p3_CD,p3_CP],[p4_CD,p4_CP],
- [p5_CD,p5_CP],[p6_CD,p6_CP],[p7_CD,p7_CP]];
-
- Enab = [[Enab_root_CD,Enab_root_CP],[Enab_p1_CD,Enab_p1_CP],[Enab_p2_CD,Enab_p2_CP],
- [Enab_p3_CD,Enab_p3_CP],[Enab_p4_CD,Enab_p4_CP],[Enab_p5_CD,Enab_p5_CP],
- [Enab_p6_CD,Enab_p6_CP],[Enab_p7_CD,Enab_p7_CP]];
+ Acti = [[root_CD,root_CP],[p1_CD,p1_CP],[p2_CD,p2_CP],[p3_CD,p3_CP],[p4_CD,p4_CP],[p5_CD,p5_CP],[p6_CD,p6_CP],[p7_CD,p7_CP]];
+ Enab = [[Enab_root_CD,Enab_root_CP],[Enab_p1_CD,Enab_p1_CP],[Enab_p2_CD,Enab_p2_CP],[Enab_p3_CD,Enab_p3_CP],[Enab_p4_CD,Enab_p4_CP],[Enab_p5_CD,Enab_p5_CP],[Enab_p6_CD,Enab_p6_CP],[Enab_p7_CD,Enab_p7_CP]];
- ok = theorem_5_18<<m,n>>(Enab,Acti); -- from theorem 5.18 page 57
+ ok = bfs_spanning_tree_oracle<<an,pn>>(Enab,Acti);
tel
diff --git a/test/bfs-spanning-tree/oracle_lemma5_16.lus b/test/bfs-spanning-tree/oracle_lemma5_16.lus
deleted file mode 100644
index e1f1cd2139a2cd1d49cfd44228ef4ced842e6234..0000000000000000000000000000000000000000
--- a/test/bfs-spanning-tree/oracle_lemma5_16.lus
+++ /dev/null
@@ -1,21 +0,0 @@
-include "bfs_spanning_tree_oracle.lus"
-
-const n=8;
-const m=2;
-const degree=2;
-const diameter=4;
-
-
-
-node oracle(root_CD,root_CP,p1_CD,p1_CP,p2_CD,p2_CP,p3_CD,p3_CP,p4_CD,p4_CP,p5_CD,p5_CP,p6_CD,p6_CP,p7_CD,p7_CP,Enab_root_CD,Enab_root_CP,Enab_p1_CD,Enab_p1_CP,Enab_p2_CD,Enab_p2_CP,Enab_p3_CD,Enab_p3_CP,Enab_p4_CD,Enab_p4_CP,Enab_p5_CD,Enab_p5_CP,Enab_p6_CD,Enab_p6_CP,Enab_p7_CD,Enab_p7_CP:bool) returns (ok:bool;);
-
-var
- Acti:bool^2^8;
- Enab:bool^2^8;
-let
- Acti = [[root_CD,root_CP],[p1_CD,p1_CP],[p2_CD,p2_CP],[p3_CD,p3_CP],[p4_CD,p4_CP],[p5_CD,p5_CP],[p6_CD,p6_CP],[p7_CD,p7_CP]];
-
- Enab = [[Enab_root_CD,Enab_root_CP],[Enab_p1_CD,Enab_p1_CP],[Enab_p2_CD,Enab_p2_CP],[Enab_p3_CD,Enab_p3_CP],[Enab_p4_CD,Enab_p4_CP],[Enab_p5_CD,Enab_p5_CP],[Enab_p6_CD,Enab_p6_CP],[Enab_p7_CD,Enab_p7_CP]];
-
- ok = lemma_5_16<<m,n>>(Enab,Acti) ;
-tel
diff --git a/test/coloring/Makefile b/test/coloring/Makefile
index 6fdf340499bf96f4d9d0548b52ef71220bac9dc9..5417f0176f92acea4b5da0520a12a0d74360dba6 100644
--- a/test/coloring/Makefile
+++ b/test/coloring/Makefile
@@ -1,4 +1,4 @@
-# Time-stamp: <modified the 25/06/2019 (at 13:28) by Erwan Jahier>
+# Time-stamp: <modified the 08/07/2019 (at 17:03) by Erwan Jahier>
test: p.cmxs ring.lut lurette
@@ -28,20 +28,10 @@ rdbg3: p.cma g.lut
-env "$(sasa) g.dot -custd" \
-sut-nd "lutin g.lut -n distributed"
-lurette:cmxs ring.lut
+lurette:cmxs ring.lut ring_oracle.lus
lurette \
-env "$(sasa) ring.dot -custd " \
-sut "lutin ring.lut -n distributed" \
+ -oracle "lv6 ring_oracle.lus -n oracle "
-lemma3.14:cmxs ring.lut
- lurette \
- -env "$(sasa) ring.dot -custd " \
- -sut "lutin ring.lut -n distributed" \
- -oracle "lv6 oracle_lemma3_14.lus -n oracle "
-
-theorem3.17:cmxs ring.lut
- lurette \
- -env "$(sasa) ring.dot -custd " \
- -sut "lutin ring.lut -n distributed" \
- -oracle "lv6 oracle_theorem3_17.lus -n oracle "
-include ../Makefile.inc
diff --git a/test/coloring/coloring_oracle.lus b/test/coloring/coloring_oracle.lus
index b85f5c69a166272300c64e9e9665f12e484df42c..467302257313aa23abdf359e025fe916049cb34f 100644
--- a/test/coloring/coloring_oracle.lus
+++ b/test/coloring/coloring_oracle.lus
@@ -1,24 +1,31 @@
-include "../lustre/round.lus"
+include "../lustre/oracle_utils.lus"
-----------------------------------------------------------------------------
-node lemma_3_14<<const m : int; const n: int>> (Enab, Acti: bool^m^n) returns (res:bool);
+node lemma_3_14<<const an:int; const pn: int>> (Enab, Acti: bool^an^pn) returns (res:bool);
var
MoveNb:int;
let
MoveNb = move_count(Acti);
- res = MoveNb <= n-1;
+ res = MoveNb <= pn-1;
tel
-----------------------------------------------------------------------------
-node theorem_3_17<<const m : int; const n: int>> (Enab, Acti: bool^m^n) returns (res:bool);
+node theorem_3_17<<const an:int; const pn:int>> (Enab, Acti: bool^an^pn) returns (res:bool);
var
Round:bool;
RoundNb:int;
let
- Round = round <<m,n>>(Enab,Acti);
+ Round = round <<an,pn>>(Enab,Acti);
RoundNb = count(Round);
res = RoundNb <= 1; -- from theorem 3.17 page 29
tel
+
+
+node coloring_oracle<<const an:int; const pn:int>> (Enab, Acti: bool^an^pn)
+returns (res:bool);
+let
+ res = lemma_3_14<<an,pn>>(Enab,Acti) and theorem_3_17<<an,pn>>(Enab,Acti);
+tel
diff --git a/test/coloring/oracle.lus b/test/coloring/oracle.lus
deleted file mode 100644
index c0d6bc7f35acb000154ec5f2b3377dad1d4dcf7e..0000000000000000000000000000000000000000
--- a/test/coloring/oracle.lus
+++ /dev/null
@@ -1,30 +0,0 @@
-
-node silence(Enab_p1_conflict,
- Enab_p2_conflict,
- Enab_p3_conflict,
- Enab_p4_conflict,
- Enab_p5_conflict,
- Enab_p6_conflict,
- Enab_p7_conflict:bool;
- p1_conflict,
- p2_conflict,
- p3_conflict,
- p4_conflict,
- p5_conflict,
- p6_conflict,
- p7_conflict:bool
-)
-returns(ok:bool);
-var
- cpt:int;
-let
- cpt = 0 -> pre cpt + 1;
- ok= (cpt < 7) or -- lemma 3.14
- nor(Enab_p1_conflict,
- Enab_p2_conflict,
- Enab_p3_conflict,
- Enab_p4_conflict,
- Enab_p5_conflict,
- Enab_p6_conflict,
- Enab_p7_conflict);
-tel
diff --git a/test/coloring/oracle_lemma3_14.lus b/test/coloring/oracle_lemma3_14.lus
deleted file mode 100644
index 30ed692cf113c473b0c078be428f46c4638f5cda..0000000000000000000000000000000000000000
--- a/test/coloring/oracle_lemma3_14.lus
+++ /dev/null
@@ -1,19 +0,0 @@
-
-include "coloring_oracle.lus"
-
-const n=7;
-const m=1;
-const degree=0;
-const diameter=0;
-
-
-node oracle(p1_conflict,p2_conflict,p3_conflict,p4_conflict,p5_conflict,p6_conflict,p7_conflict,Enab_p1_conflict,Enab_p2_conflict,Enab_p3_conflict,Enab_p4_conflict,Enab_p5_conflict,Enab_p6_conflict,Enab_p7_conflict:bool) returns (ok:bool);
-var
- Acti:bool^1^7;
- Enab:bool^1^7;
-let
- Acti = [[p1_conflict],[p2_conflict],[p3_conflict],[p4_conflict],[p5_conflict],[p6_conflict],[p7_conflict]];
-
- Enab = [[Enab_p1_conflict],[Enab_p2_conflict],[Enab_p3_conflict],[Enab_p4_conflict],[Enab_p5_conflict],[Enab_p6_conflict],[Enab_p7_conflict]];
- ok = lemma_3_14<<m,n>>(Enab,Acti); -- from Lemma 3.14 page 29
-tel
diff --git a/test/coloring/oracle_theorem3_17.lus b/test/coloring/oracle_theorem3_17.lus
deleted file mode 100644
index dcd87e703658dd7243da808b52e0c4e09ff3195a..0000000000000000000000000000000000000000
--- a/test/coloring/oracle_theorem3_17.lus
+++ /dev/null
@@ -1,19 +0,0 @@
-
-include "coloring_oracle.lus"
-
-const n=7;
-const m=1;
-const degree=0;
-const diameter=0;
-
-
-node oracle(p1_conflict,p2_conflict,p3_conflict,p4_conflict,p5_conflict,p6_conflict,p7_conflict,Enab_p1_conflict,Enab_p2_conflict,Enab_p3_conflict,Enab_p4_conflict,Enab_p5_conflict,Enab_p6_conflict,Enab_p7_conflict:bool) returns (ok:bool);
-var
- Acti:bool^1^7;
- Enab:bool^1^7;
-let
- Acti = [[p1_conflict],[p2_conflict],[p3_conflict],[p4_conflict],[p5_conflict],[p6_conflict],[p7_conflict]];
-
- Enab = [[Enab_p1_conflict],[Enab_p2_conflict],[Enab_p3_conflict],[Enab_p4_conflict],[Enab_p5_conflict],[Enab_p6_conflict],[Enab_p7_conflict]];
- ok = theorem_3_17<<m,n>>(Enab,Acti); -- from theorem 3.17
-tel
diff --git a/test/coloring/ring_oracle.lus b/test/coloring/ring_oracle.lus
new file mode 100644
index 0000000000000000000000000000000000000000..687acb0ca71f394f1b4b3cd1c484cebddd63ec36
--- /dev/null
+++ b/test/coloring/ring_oracle.lus
@@ -0,0 +1,35 @@
+-- Automatically generated by /home/jahier/sasa/_build/default/src/sasaMain.exe version "2.10.0" ("a331f5b")
+-- on crevetete the 8/7/2019 at 16:59:24
+--../../_build/install/default/bin/sasa -seed 42 -l 100 -glos ring.dot
+
+include "coloring_oracle.lus"
+const an=1; -- actions number
+const pn=7; -- processes number
+const degree=2;
+const min_degree=2;
+const mean_degree=2.000000;
+const diameter=3;
+const card=7;
+const links_number=7;
+const is_cyclic=true;
+const is_connected=true;
+const is_a_tree=false;
+const adjency=[
+ [f,t,f,f,f,f,t],
+ [t,f,t,f,f,f,f],
+ [f,t,f,t,f,f,f],
+ [f,f,t,f,t,f,f],
+ [f,f,f,t,f,t,f],
+ [f,f,f,f,t,f,t],
+ [t,f,f,f,f,t,f]];
+
+node oracle(p1_conflict,p2_conflict,p3_conflict,p4_conflict,p5_conflict,p6_conflict,p7_conflict,Enab_p1_conflict,Enab_p2_conflict,Enab_p3_conflict,Enab_p4_conflict,Enab_p5_conflict,Enab_p6_conflict,Enab_p7_conflict:bool) returns (ok:bool);
+var
+ Acti:bool^1^7;
+ Enab:bool^1^7;
+let
+ Acti = [[p1_conflict],[p2_conflict],[p3_conflict],[p4_conflict],[p5_conflict],[p6_conflict],[p7_conflict]];
+ Enab = [[Enab_p1_conflict],[Enab_p2_conflict],[Enab_p3_conflict],[Enab_p4_conflict],[Enab_p5_conflict],[Enab_p6_conflict],[Enab_p7_conflict]];
+
+ ok = coloring_oracle<<an,pn>>(Enab,Acti);
+tel
diff --git a/test/dijkstra-ring/Makefile b/test/dijkstra-ring/Makefile
index a1995f4ec1be147e269fe36a221e3a7b392aefad..64222dff6ae00e5c651f7866ddbe7fae56f10152 100644
--- a/test/dijkstra-ring/Makefile
+++ b/test/dijkstra-ring/Makefile
@@ -1,4 +1,4 @@
-# Time-stamp: <modified the 07/06/2019 (at 10:05) by Erwan Jahier>
+# Time-stamp: <modified the 08/07/2019 (at 17:17) by Erwan Jahier>
test: cmxs lurette1
@@ -20,23 +20,13 @@ rdbg: cmxs ring.lut
-sut-nd "lutin ring.lut -n distributed"\
-lurette1:cmxs ring.lut
+lurette1:cmxs ring.lut ring_oracle.lus
lurette \
-env "$(sasa) ring.dot -custd " \
-sut "lutin ring.lut -n distributed" \
-
-lemma6.28:cmxs ring.lut
- lurette \
- -env "$(sasa) ring.dot -custd " \
- -sut "lutin ring.lut -n distributed" \
- -oracle "lv6 oracle_lemma6_28.lus -n oracle "
-
-theorem6.29:cmxs ring.lut
- lurette \
- -env "$(sasa) ring.dot -custd " \
- -sut "lutin ring.lut -n distributed" \
- -oracle "lv6 oracle_theorem6_29.lus -n oracle "
-
+ -oracle "lv6 ring_oracle.lus -n oracle"
-include ../Makefile.inc
+lclean: clean
+ rm -f ring_oracle.lus
diff --git a/test/dijkstra-ring/oracle_lemma6_28.lus b/test/dijkstra-ring/oracle_lemma6_28.lus
deleted file mode 100644
index 1a3645da446ea742c27bce57aa41fb48993b8827..0000000000000000000000000000000000000000
--- a/test/dijkstra-ring/oracle_lemma6_28.lus
+++ /dev/null
@@ -1,20 +0,0 @@
-
-include "dijkstra_ring.lus"
-
-const n=8;
-const m=1;
-const degree=0;
-const diameter=0;
-
-
-node oracle(p1_a,p2_a,p3_a,p4_a,p5_a,p6_a,p7_a,p8_a,Enab_p1_a,Enab_p2_a,Enab_p3_a,Enab_p4_a,Enab_p5_a,Enab_p6_a,Enab_p7_a,Enab_p8_a:bool) returns (ok:bool);
-var
- Acti:bool^1^8;
- Enab:bool^1^8;
-let
- Acti = [[p1_a],[p2_a],[p3_a],[p4_a],[p5_a],[p6_a],[p7_a],[p8_a]];
-
- Enab = [[Enab_p1_a],[Enab_p2_a],[Enab_p3_a],[Enab_p4_a],[Enab_p5_a],[Enab_p6_a],[Enab_p7_a],[Enab_p8_a]];
-
- ok = lemma_6_28<<m,n>>(Enab,Acti) ; -- Lemma 6.28
-tel
diff --git a/test/dijkstra-ring/oracle_theorem6_29.lus b/test/dijkstra-ring/oracle_theorem6_29.lus
deleted file mode 100644
index 8d7c8e378f8334f9d9a2f8c04d451a11b6d2bc8e..0000000000000000000000000000000000000000
--- a/test/dijkstra-ring/oracle_theorem6_29.lus
+++ /dev/null
@@ -1,21 +0,0 @@
-
-include "dijkstra_ring.lus"
-
-const n=8;
-const m=1;
-const degree=0;
-const diameter=0;
-const k = 42;
-
-
-node oracle(p1_a,p2_a,p3_a,p4_a,p5_a,p6_a,p7_a,p8_a,Enab_p1_a,Enab_p2_a,Enab_p3_a,Enab_p4_a,Enab_p5_a,Enab_p6_a,Enab_p7_a,Enab_p8_a:bool) returns (ok:bool);
-var
- Acti:bool^1^8;
- Enab:bool^1^8;
-let
- Acti = [[p1_a],[p2_a],[p3_a],[p4_a],[p5_a],[p6_a],[p7_a],[p8_a]];
-
- Enab = [[Enab_p1_a],[Enab_p2_a],[Enab_p3_a],[Enab_p4_a],[Enab_p5_a],[Enab_p6_a],[Enab_p7_a],[Enab_p8_a]];
-
- ok = theorem_6_29<<m,n>>(Enab,Acti) ; -- Theorem 6.29
-tel
diff --git a/test/dijkstra-ring/ring.dot b/test/dijkstra-ring/ring.dot
index 9a3a12ee04f2f9a8ffe25bf7b15c957690d7c9be..8466e481aa26607b534dce4f85bb79471916f51b 100644
--- a/test/dijkstra-ring/ring.dot
+++ b/test/dijkstra-ring/ring.dot
@@ -1,4 +1,5 @@
digraph ring7 {
+ graph [k=3]
p1 [algo="ringroot.ml" init="v=1" ]
p2 [algo="ring.ml" init="v=3" ]
diff --git a/test/lustre/round.lus b/test/lustre/round.lus
index db2606b22011024b7ad588e6de839191186fce38..ed7eebd0cad48aefd499f2a3023340e3f3faeaa0 100644
--- a/test/lustre/round.lus
+++ b/test/lustre/round.lus
@@ -1,4 +1,4 @@
--- -- Time-stamp: <modified the 08/07/2019 (at 15:28) by Erwan Jahier>
+-- -- Time-stamp: <modified the 08/07/2019 (at 17:04) by Erwan Jahier>
--
-- Computing rounds in Lustre
-- The inputs are 2 arrays Enab and Acti, where:
@@ -19,7 +19,7 @@ let
res = boolred<<0,0,pn>>(mask); -- when all are false,
tel
-node mask_init <<const an:int; const pn:int>> (E,A: bool^an^pn) returns (res : bool^pn);
+function mask_init <<const an:int; const pn:int>> (E,A: bool^an^pn) returns (res : bool^pn);
var
enab:bool^pn; -- at least one action is enabled
acti:bool^pn; -- at least one action is active
@@ -34,7 +34,7 @@ let
res = not(a=>b);
tel
-node mask_update<<const an: int; const pn: int>> (E,A: bool^an^pn; pmask:bool^pn)
+function mask_update<<const an: int; const pn: int>> (E,A: bool^an^pn; pmask:bool^pn)
returns (res : bool^pn);
var
acti:bool^pn; -- at least one action is active
diff --git a/test/lustre/utils.lus b/test/lustre/utils.lus
index 19422a13a05802c66a19a09a4b77c25a03519f3a..8032b57df5053f24a84c00203da2b69275b3fb25 100644
--- a/test/lustre/utils.lus
+++ b/test/lustre/utils.lus
@@ -30,26 +30,30 @@ node map_and<<const n:int>> (X,Y:bool^n) returns (Z:bool^n);
let
Z = map<<and,n>>(X,Y) ;
tel
+node map_or<<const n:int>> (X,Y:bool^n) returns (Z:bool^n);
+let
+ Z = map<<or,n>>(X,Y) ;
+tel
-----------------------------------------------------------------------------
node implies_list(A,B:bool^m) returns (res:bool^m);
let
- res = map<<=>,an>>(A,B) ;
+ res = map<<=>,m>>(A,B) ;
tel
-----------------------------------------------------------------------------
-node one_true (tab:bool^an^pn) returns (res:bool);
+node one_true <<const m:int ; const n:int>> (tab:bool^m^n) returns (res:bool);
let
- res = (((red<<count_true_acc<<an>>,pn>>(0,tab)))=1);
+ res = (((red<<count_true_acc<<m>>,n>>(0,tab)))=1);
tel
-----------------------------------------------------------------------------
-node all_true (t:bool^m^n) returns (res:bool);
+node all_true <<const m:int ; const n:int>>(t:bool^m^n) returns (res:bool);
let
res = boolred<<m,m,m>>((red<<map_and<<m>>,n>>(true^m,t))) ;
tel
-node all_false (t:bool^m^n) returns (res:bool);
+node all_false <<const m:int ; const n:int>>(t:bool^m^n) returns (res:bool);
let
res = boolred<<0,0,m>>((red<<map_or<<m>>,n>>(false^m,t))) ;
tel
diff --git a/test/unison/Makefile b/test/unison/Makefile
index a2ff818ae9fbc7b5766b8d949a35ba6a33710e9b..4fee40a63af4e87d35a8368238401510808070c0 100644
--- a/test/unison/Makefile
+++ b/test/unison/Makefile
@@ -1,4 +1,4 @@
-# Time-stamp: <modified the 07/06/2019 (at 17:36) by Erwan Jahier>
+# Time-stamp: <modified the 08/07/2019 (at 17:27) by Erwan Jahier>
test: test1 test2 lurette0
@@ -21,23 +21,11 @@ luciole:
luciole-rif $(sasa) ring.dot -custd -rif -ifi
-lurette0:cmxs ring.lut
+lurette0:cmxs ring.lut ring_oracle.lus
lurette -o lurette.rif \
-env "$(sasa) ring.dot -custd -rif" \
- -sut "lutin ring.lut -n synchronous"
-
-lemma4_10:cmxs ring.lut
- lurette -o lurette.rif \
- -env "$(sasa) ring.dot -custd -rif" \
- -sut "lutin ring.lut -n synchronous" \
- -oracle "lv6 oracle_lemma4_10.lus -n oracle"
-
-theorem4_11:cmxs ring.lut
- lurette -o lurette.rif \
- -env "$(sasa) ring.dot -custd -rif" \
- -sut "lutin ring.lut -n synchronous" \
- -oracle "lv6 oracle_theorem4_11.lus -n oracle"
-
+ -sut "lutin ring.lut -n synchronous" \
+ -oracle "lv6 ring_oracle.lus -n oracle"
lurette: lurette0 s g
@@ -47,3 +35,6 @@ rdbg: unison.cma unison.cmxs ring.lut
-sut-nd "lutin ring.lut -n synchronous"
-include ../Makefile.inc
+
+lclean: clean
+ rm -f ring_oracle.lus
diff --git a/test/unison/oracle_lemma4_10.lus b/test/unison/oracle_lemma4_10.lus
deleted file mode 100644
index 0f309c888573c73f7b367ddb39b4c783f5b21387..0000000000000000000000000000000000000000
--- a/test/unison/oracle_lemma4_10.lus
+++ /dev/null
@@ -1,19 +0,0 @@
-include "unison_oracle.lus"
-
-const n=7;
-const m=1;
-const degree=0;
-const diameter=3;
-
-
-node oracle(p1_g,p2_g,p3_g,p4_g,p5_g,p6_g,p7_g,Enab_p1_g,Enab_p2_g,Enab_p3_g,Enab_p4_g,Enab_p5_g,Enab_p6_g,Enab_p7_g:bool) returns (ok:bool);
-var
- Acti:bool^1^7;
- Enab:bool^1^7;
-let
- Acti = [[p1_g],[p2_g],[p3_g],[p4_g],[p5_g],[p6_g],[p7_g]];
-
- Enab = [[Enab_p1_g],[Enab_p2_g],[Enab_p3_g],[Enab_p4_g],[Enab_p5_g],[Enab_p6_g],[Enab_p7_g]];
-
- ok = lemma_4_10<<m,n>>(Enab,Acti) ; -- from Lemma 4.10 page 40
-tel
diff --git a/test/unison/oracle_theorem4_11.lus b/test/unison/oracle_theorem4_11.lus
deleted file mode 100644
index b957e9aaefd80146b47dd0a65cf3b3a5efccb3ce..0000000000000000000000000000000000000000
--- a/test/unison/oracle_theorem4_11.lus
+++ /dev/null
@@ -1,21 +0,0 @@
-include "unison_oracle.lus"
-
-const n=7;
-const m=1;
-const degree=0;
-const diameter=3;
-const max_clock =10 ;
-const is_connected = true;
-
-
-
-node oracle(p1_g,p2_g,p3_g,p4_g,p5_g,p6_g,p7_g,Enab_p1_g,Enab_p2_g,Enab_p3_g,Enab_p4_g,Enab_p5_g,Enab_p6_g,Enab_p7_g:bool) returns (ok:bool);
-var
- Acti:bool^1^7;
- Enab:bool^1^7;
-let
- Acti = [[p1_g],[p2_g],[p3_g],[p4_g],[p5_g],[p6_g],[p7_g]];
-
- Enab = [[Enab_p1_g],[Enab_p2_g],[Enab_p3_g],[Enab_p4_g],[Enab_p5_g],[Enab_p6_g],[Enab_p7_g]];
- ok = theorem_4_11<<m,n>>(Enab,Acti,is_connected,max_clock); -- from theorem 4.11 page 40
-tel
diff --git a/test/unison/ring.dot b/test/unison/ring.dot
index 188917b7cf5311ebd87093c3ed254db469d2396a..c7c94ca656eb662599e07266d45695b3429b9c26 100644
--- a/test/unison/ring.dot
+++ b/test/unison/ring.dot
@@ -1,5 +1,5 @@
graph ring7 {
- graph [diameter=7]
+ graph [max_clock=10]
p1 [algo="unison.ml"]
p2 [algo="unison.ml" ]
diff --git a/test/unison/round.lus b/test/unison/round.lus
deleted file mode 100644
index 94dfbc6bf42973a7e7027e594bffb55ee7368285..0000000000000000000000000000000000000000
--- a/test/unison/round.lus
+++ /dev/null
@@ -1,132 +0,0 @@
--- -- Time-stamp: <modified the 26/06/2019 (at 15:13) by Erwan Jahier>
---
--- Computing rounds in Lustre
--- The inputs are 2 arrays Enab and Acti, where:
--- - Enab[i][j] is true iff action i of process j is enabled
--- - Acti[i][j] is true iff action i of process j is active
-
--- n holds the number of processes
--- m holds the number of actions per process
-node round<<const m : int; const n: int>> (Enab, Acti: bool^m^n) returns (res:bool);
-var
- mask: bool^n;
- pres: bool;
-let
- pres = true -> pre res;
- mask = merge pres (true -> mask_init<<m, n>> (Enab, Acti) when pres)
- (false -> mask_update<<m, n>>(Enab, Acti, pre mask) when not pres);
-
- res = boolred<<0,0,n>>(mask); -- when all are false,
-tel
-
-node mask_init <<const m:int; const n:int>> (E,A: bool^m^n) returns (res : bool^n);
-var
- enab:bool^n; -- at least one action is enabled
- acti:bool^n; -- at least one action is active
-let
- enab = map<< red<<or, m>>, n >>(false^n, E);
- acti = map<< red<<or, m>>, n >>(false^n, A);
- res = map<<not_implies, n>>(enab,acti);
-tel
-
-function not_implies(a,b:bool) returns (res:bool);
-let
- res = not(a=>b);
-tel
-
-node mask_update<<const m: int; const n: int>> (E,A: bool^m^n; pmask:bool^n) returns (res : bool^n);
-var
- acti:bool^n; -- at least one action is active
-let
- acti = map<< red<<or, m>>, n >>(false^n, A);
- res = map<<not_implies, n>>(pmask,acti);
-tel
-
-
-node test53=round<< 5,3 >>
-node test52=round<< 5,2 >>
-
------------------------------------------------------------------------------
-node count(x:bool) returns(cpt:int);
-let
- cpt = 0 -> if x then pre cpt + 1 else pre cpt;
-tel
------------------------------------------------------------------------------
-
-node silent<<const m: int; const n: int>> (Enab: bool^m^n) returns (ok:bool);
-var
- enab:bool^n; -- at least one action is enabled
-let
- enab = map<< red<<or, m>>, n >>(false^n, Enab);
- ok = not(red<<or, n>>(false, enab));
-tel
-
------------------------------------------------------------------------------
-node after_n(n:int; x:bool) returns (res:bool);
-var cpt:int;
-let
- cpt = 0 -> pre cpt + 1;
- res = cpt <= n or x;
-tel
-
------------------------------------------------------------------------------
------------------------------------------------------------------------------
-node bool_to_int(X:int; Y:bool) returns (Z:int);
-let
- Z = if(Y) then X+1 else X;
-tel
-
------------------------------------------------------------------------------
-node map_and (X,Y:bool^m) returns (Z:bool^m);
-let
- Z = map<<and,m>>(X,Y) ;
-tel
-
------------------------------------------------------------------------------
-node implies_list(A,B:bool^m) returns (res:bool^m);
-let
- res = map<<=>,m>>(A,B) ;
-tel
-
------------------------------------------------------------------------------
-node add_int_true(X:int; Y:bool^m) returns (Z:int);
-let
- Z = red<<bool_to_int,m>>(X,Y);
-tel
-
------------------------------------------------------------------------------
-node one_true (tab:bool^m^n) returns (res:bool);
-let
- res = (((red<<add_int_true,n>>(0,tab)))=1);
-tel
-
------------------------------------------------------------------------------
-node all_true (tab_acti:bool^m^n) returns (res:bool);
-let
- res = boolred<<m,m,m>>((red<<map_and,n>>(true^m,tab_acti))) ;
-tel
-
------------------------------------------------------------------------------
-node compt_move (tab_acti:bool^m^n) returns (nb_act:int);
-let
- nb_act = 0 -> pre(nb_act) + (red<<add_int_true,n>>(0,tab_acti));
-tel
-
------------------------------------------------------------------------------
-node is_distributed(acti,enab:bool^m^n) returns (res:bool);
-let
- res = true -> (((red<<add_int_true,n>>(0,acti))>=1) or silent<<m,n>>(enab)) and pre(res);
-tel
-
------------------------------------------------------------------------------
-node is_central(acti:bool^m^n) returns (res:bool);
-let
- res = true -> (one_true(acti)) and pre(res);
-tel
-
------------------------------------------------------------------------------
-node is_synchronous(enab,acti:bool^m^n) returns (res:bool);
-let
- res = true -> all_true(map<<implies_list,n>>(enab,acti)) and pre(res);
-tel
-
diff --git a/test/unison/unison.ml b/test/unison/unison.ml
index 6916347978bab520da05db445e7b8e12da8e9e94..3c709010fd574acda46be7db5f336a8b7f0fe6c9 100644
--- a/test/unison/unison.ml
+++ b/test/unison/unison.ml
@@ -1,9 +1,9 @@
-(* Time-stamp: <modified the 03/07/2019 (at 10:29) by Erwan Jahier> *)
+(* Time-stamp: <modified the 08/07/2019 (at 17:28) by Erwan Jahier> *)
open Algo
(* let m=10 (* max 2 (1+2*diameter ()) *) *)
-let diameter = int_of_string (get_graph_attribute "diameter")
+let diameter = Algo.diameter ()
let m = max 2 (1+2*diameter)
diff --git a/test/unison/unison_oracle.lus b/test/unison/unison_oracle.lus
index f6b98e291c4a9f9cd95bb6c31cd3ccb958f7c77b..d82c3b5e23d784296f2b48cd3bf21a6768aa92f8 100644
--- a/test/unison/unison_oracle.lus
+++ b/test/unison/unison_oracle.lus
@@ -1,28 +1,37 @@
-include "../lustre/round.lus"
-
+include "../lustre/oracle_utils.lus"
-----------------------------------------------------------------------------
-
-node theorem_4_11<<const m : int; const n: int>> (Enab, Acti: bool^m^n;is_connected:bool;max_clock:int) returns (res:bool);
+node theorem_4_11<<const an:int; const pn:int>> (Enab, Acti: bool^an^pn)
+returns (res:bool);
var
nb_step:int;
All_Acti:bool;
let
nb_step = 1 -> pre(nb_step) + 1 ;
- All_Acti = all_true(Acti);
- res =((max_clock>= (2*diameter-1)) and is_connected) => (nb_step>=(3*diameter-2)) => All_Acti ; -- Theorem 4.11 page 40
+ All_Acti = all_true<<an,pn>>(Acti);
+ res = ((max_clock>= (2*diameter-1)) and is_connected)
+ => (nb_step>=(3*diameter-2)) => All_Acti ; -- Theorem 4.11 page 40
tel
-----------------------------------------------------------------------------
-
-node lemma_4_10<<const m : int; const n: int>> (Enab, Acti: bool^m^n) returns (res:bool);
+node lemma_4_10<<const an: int; const pn:int>> (Enab, Acti: bool^an^pn)
+returns (res:bool);
var
nb_step:int;
All_Acti:bool;
Silent:bool;
let
nb_step = 0 -> pre nb_step + 1 ;
- Silent = silent<<m,n>>(Enab);
- All_Acti = all_true(Acti);
+ Silent = silent<<an,pn>>(Enab);
+ All_Acti = all_true<<an,pn>>(Acti);
res = (nb_step>=((3*diameter)-2)) => All_Acti ; -- from Lemma 4.10 page 40
-tel
\ No newline at end of file
+tel
+
+-----------------------------------------------------------------------------
+node unison_oracle<<const an:int; const pn:int>> (Enab, Acti: bool^an^pn)
+returns (ok:bool);
+let
+
+ ok = lemma_4_10 <<an,pn>> (Enab, Acti) and
+ theorem_4_11<<an,pn>> (Enab, Acti);
+tel