From 6618348fe893be118380fda1111d0de8c9687ca4 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr>
Date: Fri, 5 Jul 2019 15:39:34 +0200
Subject: [PATCH] Test: rewrite sligthly the bfs oracle, and commit the generic
oracle
---
lib/sasacore/genOracle.ml | 10 +++---
test/Makefile.inc | 5 ++-
test/bfs-spanning-tree/Makefile | 11 ++++---
.../bfs_spanning_tree_oracle.lus | 14 +++++++++
.../fig5.1-noinit_oracle.lus | 31 -------------------
5 files changed, 29 insertions(+), 42 deletions(-)
create mode 100644 test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus
delete mode 100644 test/bfs-spanning-tree/fig5.1-noinit_oracle.lus
diff --git a/lib/sasacore/genOracle.ml b/lib/sasacore/genOracle.ml
index f02599a0..72d13556 100644
--- a/lib/sasacore/genOracle.ml
+++ b/lib/sasacore/genOracle.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 05/07/2019 (at 11:30) by Erwan Jahier> *)
+(* Time-stamp: <modified the 05/07/2019 (at 15:25) by Erwan Jahier> *)
open Process
@@ -35,8 +35,8 @@ let (f: 'v Process.t list -> string) =
Str.global_replace (Str.regexp "[-,\\.]") "_" algo
in
Printf.sprintf "%sinclude \"%s_oracle.lus\"
-const n=%d;
-const m=%d;
+const an=%d; -- actions number
+const pn=%d; -- processes number
const degree=%d;
const diameter=%d;
@@ -44,12 +44,12 @@ node oracle(%s) returns (ok:bool);
var
%slet
%s %s
- ok = %s_oracle<<m,n>>(Enab,Acti);
+ ok = %s_oracle<<an,pn>>(Enab,Acti);
tel
"
(Mypervasives.entete "--" SasaVersion.str SasaVersion.sha)
algo
- n m degree diameter
+ m n degree diameter
input_decl
array_decl
array_def_acti
diff --git a/test/Makefile.inc b/test/Makefile.inc
index c04b14bb..bb7781da 100644
--- a/test/Makefile.inc
+++ b/test/Makefile.inc
@@ -1,4 +1,4 @@
-# Time-stamp: <modified the 20/06/2019 (at 17:26) by Erwan Jahier>
+# Time-stamp: <modified the 05/07/2019 (at 15:18) by Erwan Jahier>
DIR=../../_build/install/default
@@ -18,6 +18,9 @@ LIB=-package algo
%.lut: %.dot
$(sasa) -gld $^
+%_oracle.lus: %.dot
+ $(sasa) -glos $^
+
%.rif: cmxs %.dot
$(sasa) $(sasaopt) $*.dot -rif > $*.rif
diff --git a/test/bfs-spanning-tree/Makefile b/test/bfs-spanning-tree/Makefile
index f1cfbb42..2b9bc3ad 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 11:09) by Erwan Jahier>
+# Time-stamp: <modified the 05/07/2019 (at 15:30) by Erwan Jahier>
test: test0 test2 lurette0 lurette1
@@ -26,15 +26,14 @@ gnuplot: fig5.1-noinit.rif
gnuplot2: fig5.2.rif
gnuplot-rif $<
-lurette0:cmxs fig5.1-noinit.lut
+lurette0:cmxs fig5.1-noinit.lut fig5.1-noinit_oracle.lus
lurette -o lurette.rif \
-env "$(sasa) fig5.1-noinit.dot -custd -rif" \
-sut "lutin fig5.1-noinit.lut -n distributed"
-lurette1:cmxs fig5.1.lut
+lurette1:cmxs fig5.1.lut fig5.1_oracle.lus
rdbg -lurette -o lurette.rif \
- -env "$(sasa) fig5.1.dot -custd -rif" \
- -sut "lutin fig5.1.lut -n distributed" \
+ -env "$(sasa) fig5.1.dot -dd -rif" \
-oracle "lv6 fig5.1_oracle.lus -n oracle"
lurette: lurette0
@@ -61,3 +60,5 @@ manual:cmxs fig5.1-noinit.lut
-include ../Makefile.inc
+lclean: clean
+ rm fig*oracle.lus
diff --git a/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus b/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus
new file mode 100644
index 00000000..bfaed4c4
--- /dev/null
+++ b/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus
@@ -0,0 +1,14 @@
+
+include "round.lus"
+
+node bfs_spanning_tree_oracle<<const an:int; const pn:int>> (Enab, Acti: bool^an^pn)
+returns (ok:bool);
+var
+ Round, Silent:bool;
+ RoundNb:int;
+let
+ Silent = silent<<an,pn>>(Enab);
+ Round = round <<an,pn>>(Enab,Acti);
+ RoundNb = count(Round);
+ ok = (RoundNb>=diameter+2) => Silent; -- from theorem 5.18 page 57
+tel
diff --git a/test/bfs-spanning-tree/fig5.1-noinit_oracle.lus b/test/bfs-spanning-tree/fig5.1-noinit_oracle.lus
deleted file mode 100644
index d1a7e835..00000000
--- a/test/bfs-spanning-tree/fig5.1-noinit_oracle.lus
+++ /dev/null
@@ -1,31 +0,0 @@
-
-include "round.lus"
-
-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,Round, Silent:bool; RoundNb:int);
-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]];
-
- Round = round <<m,n>>(Enab,Acti);
- RoundNb = count(Round);
- Silent = silent<<m,n>>(Enab);
- ok = (RoundNb>=diameter+2) => Silent; -- from theorem 5.18 page 57
-tel
--
GitLab