From c3dfe95fff436f353577a4dd8edc4c16e8ea0992 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr>
Date: Fri, 10 Jun 2022 16:41:39 +0200
Subject: [PATCH] fix: the round number in lustre oracles (no incr at the last
step)
---
test/async-unison/Makefile | 4 +-
test/async-unison/async_unison_oracle.lus | 9 ++--
test/async-unison/ring_oracle.lus | 47 -------------------
.../bfs_spanning_tree_oracle.lus | 7 +--
test/coloring/Makefile | 4 +-
test/coloring/coloring_oracle.lus | 2 +-
test/lustre/round.lus | 16 ++++---
test/rsp-tree/rsp_tree_oracle.lus | 2 +-
8 files changed, 24 insertions(+), 67 deletions(-)
delete mode 100644 test/async-unison/ring_oracle.lus
diff --git a/test/async-unison/Makefile b/test/async-unison/Makefile
index c120fd68..8b250e32 100644
--- a/test/async-unison/Makefile
+++ b/test/async-unison/Makefile
@@ -1,4 +1,4 @@
-# Time-stamp: <modified the 30/05/2022 (at 11:05) by Erwan Jahier>
+# Time-stamp: <modified the 10/06/2022 (at 16:08) by Erwan Jahier>
DECO_PATTERN="0-:p.ml"
-include ../Makefile.dot
@@ -25,7 +25,7 @@ rdbg_test: ring.ml
rdbg --sasa -o ring.rif -l 10000 -env "$(sasa) -vl 1 ring.dot -cd" -go --input some_session
clean: genclean
- rm -f ring.ml
+ rm -f ring.ml ring_oracle.lus
##############################################################################
# Other examples of use
diff --git a/test/async-unison/async_unison_oracle.lus b/test/async-unison/async_unison_oracle.lus
index 53341531..37424f3e 100644
--- a/test/async-unison/async_unison_oracle.lus
+++ b/test/async-unison/async_unison_oracle.lus
@@ -21,11 +21,12 @@ let
(i<=j or (adjacency[l/pn][l mod pn] => is_close(State[l/pn], State[l mod pn])));
tel
-node async_unison_oracle (State : int^pn; Enab, Acti: bool^an^pn)
-returns (res, Legitimate:bool; rn:int);
+node async_unison_oracle (Legitimate:bool; Enab, Acti: bool^an^pn; State : int^pn)
+returns (res:bool);
+var
+ rn:int;
let
- rn = round_count(round <<an,pn>>(Enab,Acti));
- Legitimate = is_legitimate <<pn*pn-1>>(State);
+ rn = round_count(round <<an,pn>>(Enab,Acti), silent<<an,pn>>(Enab));
res = redge(Legitimate) => (rn <= diameter*card);
tel
diff --git a/test/async-unison/ring_oracle.lus b/test/async-unison/ring_oracle.lus
deleted file mode 100644
index e750c685..00000000
--- a/test/async-unison/ring_oracle.lus
+++ /dev/null
@@ -1,47 +0,0 @@
--- Automatically generated by /home/jahier/.opam/4.09.0/bin/sasa version "2.15.1" ("f665f01")
--- on crevetete the 13/2/2020 at 23:11:02
---sasa -glos ring.dot
-
-include "async_unison_oracle.lus"
-const an=2; -- actions number
-const pn=7; -- processes number
-const degree=2;
-const min_degree=2;
-const mean_degree=1.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 f=false;
-const t=true;
-const adjacency=[
- [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_c:int;p2_c:int;p3_c:int;p4_c:int;p5_c:int;p6_c:int;p7_c:int;
- Enab_p1_Ip,Enab_p1_Rp,Enab_p2_Ip,Enab_p2_Rp,Enab_p3_Ip,Enab_p3_Rp,Enab_p4_Ip,
- Enab_p4_Rp,Enab_p5_Ip,Enab_p5_Rp,Enab_p6_Ip,Enab_p6_Rp,Enab_p7_Ip,Enab_p7_Rp:bool;
- p1_Ip,p1_Rp,p2_Ip,p2_Rp,p3_Ip,p3_Rp,p4_Ip,p4_Rp,
- p5_Ip,p5_Rp,p6_Ip,p6_Rp,p7_Ip,p7_Rp:bool)
-returns (ok,stable:bool; rn : int);
-var
- Acti:bool^an^pn;
- Enab:bool^an^pn;
- State:int^pn;
-let
- Acti = [[p1_Ip,p1_Rp],[p2_Ip,p2_Rp],[p3_Ip,p3_Rp],[p4_Ip,p4_Rp],
- [p5_Ip,p5_Rp],[p6_Ip,p6_Rp],[p7_Ip,p7_Rp]];
- Enab = [[Enab_p1_Ip,Enab_p1_Rp],[Enab_p2_Ip,Enab_p2_Rp],[Enab_p3_Ip,Enab_p3_Rp],
- [Enab_p4_Ip,Enab_p4_Rp],[Enab_p5_Ip,Enab_p5_Rp],[Enab_p6_Ip,Enab_p6_Rp],
- [Enab_p7_Ip,Enab_p7_Rp]];
- State = [p1_c,p2_c,p3_c,p4_c,p5_c,p6_c,p7_c];
- ok, stable, rn = async_unison_oracle(State,Enab,Acti);
-tel
diff --git a/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus b/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus
index 56e0da5e..6551027a 100644
--- a/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus
+++ b/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus
@@ -2,13 +2,14 @@ include "../lustre/oracle_utils.lus"
node bfs_spanning_tree_oracle<<const an:int; const pn:int>>
(legitimate: bool; Enab, Acti: bool^an^pn; config:int^(2*pn))
-returns (ok:bool; RoundNb:int; mask0, mask: bool^pn);
+returns (ok:bool);
var
CD_disable:bool;
Silent, Round : bool;
+ RoundNb:int;
let
- Round, mask0, mask = round <<an,pn>>(Enab,Acti);
- RoundNb = round_count(Round);
+ Round = round <<an,pn>>(Enab,Acti);
+ RoundNb = round_count(Round, Silent);
Silent = silent<<an,pn>>(Enab);
CD_disable = all_CD_are_false(Enab);
ok = lemma_5_16 (RoundNb, CD_disable) and
diff --git a/test/coloring/Makefile b/test/coloring/Makefile
index 69e01b1c..e849c2bb 100644
--- a/test/coloring/Makefile
+++ b/test/coloring/Makefile
@@ -1,4 +1,4 @@
-# Time-stamp: <modified the 30/05/2022 (at 14:38) by Erwan Jahier>
+# Time-stamp: <modified the 10/06/2022 (at 16:29) by Erwan Jahier>
sasa=$(DIR)/bin/sasa -l 100
@@ -19,7 +19,7 @@ utest:
lurette: ring.cmxs ring_oracle.lus
lurette --sasa -o lurette-ring.rif \
- -sut "sasa ring.dot -rif -lcd " \
+ -sut "sasa ring.dot -rif -lcd " \
-oracle "lv6 ring_oracle.lus -n oracle -exec"
clean: genclean
rm -f ring.lut ring.ml ring_oracle.ml
diff --git a/test/coloring/coloring_oracle.lus b/test/coloring/coloring_oracle.lus
index e164cd66..0fae2f5c 100644
--- a/test/coloring/coloring_oracle.lus
+++ b/test/coloring/coloring_oracle.lus
@@ -24,7 +24,7 @@ var
-- RoundNb:int;
let
Round = round <<an,pn>>(Enab,Acti);
- RoundNb = round_count(Round);
+ RoundNb = round_count(Round, silent<<an,pn>>(Enab));
res = RoundNb <= 1; -- from theorem 3.17 page 29
tel
diff --git a/test/lustre/round.lus b/test/lustre/round.lus
index 6398b656..b97db670 100644
--- a/test/lustre/round.lus
+++ b/test/lustre/round.lus
@@ -1,4 +1,4 @@
--- -- Time-stamp: <modified the 10/06/2022 (at 15:59) by Erwan Jahier>
+-- -- Time-stamp: <modified the 10/06/2022 (at 16:45) by Erwan Jahier>
--
-- Computing rounds in Lustre
-- The inputs are 2 arrays Enab and Acti, where:
@@ -8,27 +8,29 @@
-- n holds the number of processes
-- m holds the number of actions per process
node round<<const an : int; const pn: int>> (Enab, Acti: bool^an^pn)
-returns (res:bool; mask0, mask: bool^pn;);
+returns (res:bool);
var
-- mask[i] is true iff pi should be activated or stop being enabled
-- when forall i mask[i] is false, we have a round.
pmask: bool^pn;
- init_mask, psilent: bool;
+ init_mask, silent: bool;
+ mask0, mask: bool^pn;
let
- psilent = false fby silent<<an,pn>>(Enab);
+ silent = silent<<an,pn>>(Enab);
pmask = (false^pn) fby mask;
init_mask = boolred<<0,0,pn>>(mask0);
mask0 = (false^pn) -> mask_update<<an, pn>>(Enab, pre Acti, pmask);
mask = merge init_mask (true -> mask_init<<an, pn>>(Enab when init_mask))
(false -> mask0 when not init_mask);
- res = true -> not(psilent) and (boolred<<0,0,pn>>(mask0));
+ res = true -> not(silent) and (boolred<<0,0,pn>>(mask0));
tel
-- At the first instant, the round has not begun
-node round_count (r:bool) returns (res:int);
+-- At the very end, no incr should be done (
+node round_count (r,silent:bool) returns (res:int);
var cpt : int;
let
- cpt = (if r then 1 else 0) + 0 fby cpt;
+ cpt = (if r and not silent then 1 else 0) + 0 fby cpt;
res = 0 -> cpt;
tel
diff --git a/test/rsp-tree/rsp_tree_oracle.lus b/test/rsp-tree/rsp_tree_oracle.lus
index 49893bf1..ff4fa81d 100644
--- a/test/rsp-tree/rsp_tree_oracle.lus
+++ b/test/rsp-tree/rsp_tree_oracle.lus
@@ -9,7 +9,7 @@ var
let
Round = round <<an,pn>>(Enab,Acti);
Silent = silent<<an,pn>>(Enab);
- RoundNb = round_count(Round);
+ RoundNb = round_count(Round, Silent);
-- Theorem 3 in the case of connected graphs
res = (not(Silent) and is_connected) => (RoundNb < 3*card+diameter);
--
GitLab