From 6eead8db001eaca22ecc473784d53cffe4808822 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr>
Date: Wed, 8 Jun 2022 11:23:28 +0200
Subject: [PATCH] fix: round numbers were wrong and inconsistant (in sasa,
rdbg, and oracles)
---
src/sasaMain.ml | 8 +++--
.../bfs_spanning_tree_oracle.lus | 11 ++++---
test/bfs-spanning-tree/fig51_noinit.rif.exp | 2 +-
test/dfs-list/4.13.1/g.rif.exp | 4 +--
test/dfs/4.13.1/g.rif.exp | 4 +--
test/lustre/round.lus | 17 +++++-----
test/rsp-tree/4.13.1/ba100.rif.exp | 4 +--
test/rsp-tree/4.13.1/er30.rif.exp | 4 +--
test/rsp-tree/4.13.1/grid4.rif.exp | 4 +--
test/rsp-tree/4.13.1/udg100.rif.exp | 4 +--
test/toy-example-a5sf/te.rif.exp | 6 ++--
tools/rdbg4sasa/sasa-rdbg-cmds.ml | 32 +++++++++++++------
12 files changed, 59 insertions(+), 41 deletions(-)
diff --git a/src/sasaMain.ml b/src/sasaMain.ml
index 14b3841d..291c6020 100644
--- a/src/sasaMain.ml
+++ b/src/sasaMain.ml
@@ -52,7 +52,11 @@ let (update_round : bool list list -> bool list list -> unit) =
if !round_mask = [] then round_mask := enab_ll;
round_mask := List.map2 (List.map2 (&&)) !round_mask enab_ll;
round_mask := List.map2 (List.map2 (fun m a -> m && not a)) !round_mask acti_ll;
- if List.for_all (List.for_all (not)) !round_mask then (
+ if
+ not(List.for_all (List.for_all (not)) enab_ll) && (* silent conf: the round number
+ has already been incremented *)
+ List.for_all (List.for_all (not)) !round_mask
+ then (
round_mask := enab_ll;
incr rounds
);
@@ -97,7 +101,7 @@ let (simustep: out_channel -> int -> int -> string -> 'v SimuState.t -> 'v SimuS
match Register.get_fault () with
| None ->
print_step log st n i "t" pot st.sasarg st.config pl activate_val enab_ll;
- incr rounds;
+ update_round enab_ll enab_ll;
raise (Silent (n-i))
| Some ff ->
print_step log st n i "t" pot st.sasarg st.config pl activate_val enab_ll;
diff --git a/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus b/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus
index ca3d4dd1..df72597c 100644
--- a/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus
+++ b/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus
@@ -3,10 +3,12 @@ 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);
+var
+ oracle_round:int;
+ th_5_18:bool;
let
-
- ok = lemma_5_16 <<an,pn>> (Enab, Acti) and
- theorem_5_18<<an,pn>> (Enab, Acti);
+ th_5_18, oracle_round = theorem_5_18<<an,pn>> (Enab, Acti);
+ ok = lemma_5_16 <<an,pn>> (Enab, Acti) and th_5_18;
tel
-----------------------------------------------------------------------------
@@ -38,10 +40,9 @@ tel
-----------------------------------------------------------------------------
node theorem_5_18<<const an : int; const pn: int>> (Enab, Acti: bool^an^pn)
-returns (res:bool);
+returns (res:bool;RoundNb:int);
var
Round:bool;
- RoundNb:int;
Silent:bool;
let
Round = round <<an,pn>>(Enab,Acti);
diff --git a/test/bfs-spanning-tree/fig51_noinit.rif.exp b/test/bfs-spanning-tree/fig51_noinit.rif.exp
index f854413a..6346e717 100644
--- a/test/bfs-spanning-tree/fig51_noinit.rif.exp
+++ b/test/bfs-spanning-tree/fig51_noinit.rif.exp
@@ -8,7 +8,7 @@
0 -1 1 1 2 0 3 0 4 1 3 0 2 2 1 1 f f f f f f f f f f f t f f f f f f f f f f f f f f f t f f f f f
0 -1 1 1 2 0 3 0 4 1 3 1 2 2 1 1 f f f f f f f f f f f f f f f f f f f f f f f f f f f t f f f f t
-#This algo is silent after 22 moves, 5 steps, 6 rounds.
+#This algo is silent after 22 moves, 5 steps, 5 rounds.
q
#quit
diff --git a/test/dfs-list/4.13.1/g.rif.exp b/test/dfs-list/4.13.1/g.rif.exp
index 666fe73d..23e204a2 100644
--- a/test/dfs-list/4.13.1/g.rif.exp
+++ b/test/dfs-list/4.13.1/g.rif.exp
@@ -1,5 +1,5 @@
# Automatically generated by /home/jahier/.opam/4.13.1/bin/sasa version "v4.5.9" ("c9bee55")
-# on crevetete the 30/5/2022 at 14:27:33
+# on crevetete the 8/6/2022 at 11:19:12
#sasa g.dot -seed 42
#seed 42
@@ -88,6 +88,6 @@
#step 26
#outs -1 0 0 -1 -1 -1 -1 -1 -1 -1 0 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -10 -1 0 2 -1 -1 -1 -1 -1 -1 -1 0 -1 0 2 2 -1 -1 -1 -1 -1 -1 1 -1 2 -1 -1 -1 -1 -1 -1 -1 -1 0 -1 2 1 -1 -1 -1 -1 -1 -1 -1 0 -1 2 1 1 -1 -1 -1 -1 -1 -1 0 -1 2 1 1 1 -1 -1 -1 -1 -1 0 -1 2 1 1 1 1 -1 -1 -1 -1 1 f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f t t
-This algo is silent after 63 moves, 26 steps, 17 rounds.
+This algo is silent after 63 moves, 26 steps, 16 rounds.
#quit
diff --git a/test/dfs/4.13.1/g.rif.exp b/test/dfs/4.13.1/g.rif.exp
index aafa2336..37568c7a 100644
--- a/test/dfs/4.13.1/g.rif.exp
+++ b/test/dfs/4.13.1/g.rif.exp
@@ -1,5 +1,5 @@
# Automatically generated by /home/jahier/.opam/4.13.1/bin/sasa version "v4.5.9" ("c9bee55")
-# on crevetete the 30/5/2022 at 14:21:27
+# on crevetete the 8/6/2022 at 11:18:53
#sasa g.dot -seed 42
#seed 42
@@ -88,6 +88,6 @@
#step 26
#outs -1 0 0 -1 -1 -1 -1 -1 -1 -1 0 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -10 -1 0 2 -1 -1 -1 -1 -1 -1 -1 0 -1 0 2 2 -1 -1 -1 -1 -1 -1 1 -1 2 -1 -1 -1 -1 -1 -1 -1 -1 0 -1 2 1 -1 -1 -1 -1 -1 -1 -1 0 -1 2 1 1 -1 -1 -1 -1 -1 -1 0 -1 2 1 1 1 -1 -1 -1 -1 -1 0 -1 2 1 1 1 1 -1 -1 -1 -1 1 f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f t t
-This algo is silent after 63 moves, 26 steps, 17 rounds.
+This algo is silent after 63 moves, 26 steps, 16 rounds.
#quit
diff --git a/test/lustre/round.lus b/test/lustre/round.lus
index 770a813e..36102203 100644
--- a/test/lustre/round.lus
+++ b/test/lustre/round.lus
@@ -1,4 +1,4 @@
--- -- Time-stamp: <modified the 08/10/2019 (at 21:36) by Erwan Jahier>
+-- -- Time-stamp: <modified the 08/06/2022 (at 11:09) by Erwan Jahier>
--
-- Computing rounds in Lustre
-- The inputs are 2 arrays Enab and Acti, where:
@@ -11,14 +11,15 @@ node round<<const an : int; const pn: int>> (Enab, Acti: bool^an^pn) returns (re
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.
- mask: bool^pn;
- pres: bool;
- psilent: bool;
+ mask0, mask: bool^pn;
+ init_mask, psilent: bool;
let
- pres = true -> pre res;
- mask = merge pres (true -> mask_init<<an, pn>> (Enab, Acti) when pres)
- (false -> mask_update<<an, pn>>(Enab, Acti, pre mask) when not pres);
- res = not(psilent) and boolred<<0,0,pn>>(mask) ; -- when all are false,
+ init_mask = true -> boolred<<0,0,pn>>(pre mask);
+ mask0 = merge init_mask (true -> mask_init<<an, pn>> (Enab, Acti) when init_mask)
+ (false -> mask_update<<an, pn>>(Enab, Acti, pre mask) when not init_mask);
+ mask = merge res (true -> mask_init<<an, pn>> (Enab, Acti) when res)
+ (false -> mask0 when not res);
+ res = not(psilent) and boolred<<0,0,pn>>(mask0) ; -- when all are false,
psilent = false fby silent<<an,pn>>(Enab);
tel
diff --git a/test/rsp-tree/4.13.1/ba100.rif.exp b/test/rsp-tree/4.13.1/ba100.rif.exp
index ed84a839..c2d7d6ce 100644
--- a/test/rsp-tree/4.13.1/ba100.rif.exp
+++ b/test/rsp-tree/4.13.1/ba100.rif.exp
@@ -1,5 +1,5 @@
# Automatically generated by /home/jahier/.opam/4.13.1/bin/sasa version "v4.5.9" ("c9bee55")
-# on crevetete the 30/5/2022 at 14:31:29
+# on crevetete the 8/6/2022 at 11:20:27
#sasa ba100.dot -seed 42
#seed 42
@@ -91,6 +91,6 @@
#step 27
#outs 1 -1 0 1 0 2 1 0 1 1 0 1 1 2 2 1 0 1 1 0 1 1 0 1 1 0 2 1 0 2 1 2 2 1 8 2 1 0 2 1 0 1 1 0 1 1 0 1 1 0 1 1 1 2 1 0 1 1 2 2 1 0 3 1 5 2 1 1 2 1 0 1 1 0 1 1 0 1 1 1 2 1 2 3 1 2 2 1 0 2 1 0 1 1 2 3 1 4 2 1 0 2 1 0 1 1 0 2 1 2 2 1 3 2 1 2 2 1 0 3 1 1 2 1 1 3 1 0 1 1 1 2 1 0 2 1 0 2 1 0 1 1 0 1 1 0 2 1 0 1 1 0 2 1 0 1 1 0 1 1 0 1 1 0 2 1 0 2 1 0 2 1 1 2 1 1 3 1 0 2 1 0 2 1 0 1 1 0 1 1 1 2 1 1 2 1 0 3 1 0 1 1 0 1 1 0 1 1 0 2 1 1 3 1 1 2 1 0 1 1 0 1 1 1 2 1 0 3 1 0 3 1 1 2 1 1 3 1 1 3 1 1 2 1 1 2 1 0 1 1 0 2 1 0 2 1 1 2 1 1 3 1 2 3 1 0 2 1 0 1 1 0 2 1 0 2 1 0 1 1 0 2 1 1 2 1 1 2 1 1 2 1 0 2 1 0 3 1 1 2 f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f t f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f t
-This algo is silent after 304 moves, 27 steps, 11 rounds.
+This algo is silent after 304 moves, 27 steps, 10 rounds.
#quit
diff --git a/test/rsp-tree/4.13.1/er30.rif.exp b/test/rsp-tree/4.13.1/er30.rif.exp
index 795cdb1d..8485e08c 100644
--- a/test/rsp-tree/4.13.1/er30.rif.exp
+++ b/test/rsp-tree/4.13.1/er30.rif.exp
@@ -1,5 +1,5 @@
# Automatically generated by /home/jahier/.opam/4.13.1/bin/sasa version "v4.5.9" ("c9bee55")
-# on crevetete the 30/5/2022 at 14:31:28
+# on crevetete the 8/6/2022 at 11:20:27
#sasa er30.dot -seed 42
#seed 42
@@ -109,6 +109,6 @@
#step 33
#outs 1 -1 0 1 1 2 1 2 2 1 0 4 1 1 4 1 0 3 1 0 3 1 1 4 1 0 1 1 1 3 1 0 3 1 2 3 1 3 3 1 2 4 1 1 2 1 1 4 1 1 4 1 0 3 1 0 3 1 0 3 1 0 3 1 0 3 1 0 3 1 0 3 1 0 2 1 2 3 1 3 3 1 0 5 1 1 4 1 0 5 f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f t f f f f f f f f f t
-This algo is silent after 158 moves, 33 steps, 12 rounds.
+This algo is silent after 158 moves, 33 steps, 11 rounds.
#quit
diff --git a/test/rsp-tree/4.13.1/grid4.rif.exp b/test/rsp-tree/4.13.1/grid4.rif.exp
index 7a59ed2d..08b2c8fe 100644
--- a/test/rsp-tree/4.13.1/grid4.rif.exp
+++ b/test/rsp-tree/4.13.1/grid4.rif.exp
@@ -1,5 +1,5 @@
# Automatically generated by /home/jahier/.opam/4.13.1/bin/sasa version "v4.5.9" ("c9bee55")
-# on crevetete the 30/5/2022 at 14:31:28
+# on crevetete the 8/6/2022 at 11:20:27
#sasa grid4.dot -seed 42
#seed 42
@@ -148,6 +148,6 @@
#step 46
#outs 1 -1 0 1 0 1 1 0 2 1 0 3 1 0 1 1 1 2 1 1 3 1 1 4 1 0 2 1 1 3 1 1 4 1 0 5 1 0 3 1 1 4 1 1 5 1 1 6 f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f t f f f f f f f f f f f f f f f f f f f f f f f f f f f f f t
-This algo is silent after 101 moves, 46 steps, 27 rounds.
+This algo is silent after 101 moves, 46 steps, 26 rounds.
#quit
diff --git a/test/rsp-tree/4.13.1/udg100.rif.exp b/test/rsp-tree/4.13.1/udg100.rif.exp
index c1e553cc..60407ccc 100644
--- a/test/rsp-tree/4.13.1/udg100.rif.exp
+++ b/test/rsp-tree/4.13.1/udg100.rif.exp
@@ -1,5 +1,5 @@
# Automatically generated by /home/jahier/.opam/4.13.1/bin/sasa version "v4.5.9" ("c9bee55")
-# on crevetete the 30/5/2022 at 14:31:29
+# on crevetete the 8/6/2022 at 11:20:27
#sasa udg100.dot -seed 42
#seed 42
@@ -109,6 +109,6 @@
#step 33
#outs 1 -1 0 1 0 1 1 5 3 1 5 3 1 17 2 1 12 3 1 0 1 1 20 4 1 0 1 1 21 2 1 0 1 1 0 1 1 0 1 1 21 2 1 5 3 1 0 1 1 12 3 1 16 3 1 17 4 1 19 2 1 18 3 1 21 4 1 20 2 1 22 3 1 25 2 1 8 3 1 0 1 1 12 3 1 16 4 1 9 3 1 20 3 1 16 2 1 5 3 1 15 4 1 7 4 1 13 4 1 17 4 1 8 3 1 12 3 1 20 2 1 22 2 1 19 4 1 14 4 1 21 2 1 18 4 1 14 4 1 19 3 1 20 2 1 0 1 1 15 4 1 24 2 1 17 3 1 12 3 1 0 1 1 0 1 1 12 2 1 21 4 1 12 3 1 17 3 1 18 4 1 16 4 1 21 2 1 0 1 1 21 4 1 19 4 1 11 2 1 15 2 1 0 1 1 19 3 1 0 1 1 9 2 1 0 1 1 14 2 1 7 3 1 0 1 1 3 2 1 15 2 1 18 2 1 14 5 1 20 2 1 0 1 1 0 1 1 0 1 1 17 2 1 0 1 1 12 3 1 0 1 1 0 1 1 18 2 1 0 1 1 7 3 1 9 3 1 9 3 1 14 4 1 19 2 1 20 4 1 15 4 1 0 1 1 0 1 1 15 3 f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f t f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f t
-This algo is silent after 499 moves, 33 steps, 12 rounds.
+This algo is silent after 499 moves, 33 steps, 11 rounds.
#quit
diff --git a/test/toy-example-a5sf/te.rif.exp b/test/toy-example-a5sf/te.rif.exp
index 5be68f37..f754098e 100644
--- a/test/toy-example-a5sf/te.rif.exp
+++ b/test/toy-example-a5sf/te.rif.exp
@@ -1,5 +1,5 @@
-# Automatically generated by /home/jahier/.opam/4.13.1/bin/sasa version "v4.5.7" ("38972d1")
-# on crevetete the 16/2/2022 at 18:56:31
+# Automatically generated by /home/jahier/.opam/4.13.1/bin/sasa version "v4.5.9" ("c9bee55")
+# on crevetete the 8/6/2022 at 11:20:45
#sasa te.dot -seed 42
#seed 42
@@ -79,6 +79,6 @@
#step 23
#outs 1 7 7 1 6 7 1 5 7 1 4 7 1 3 7 1 2 7 1 1 7 f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f t t 0.
-This algo is silent after 43 moves, 23 steps, 15 rounds.
+This algo is silent after 43 moves, 23 steps, 14 rounds.
#quit
diff --git a/tools/rdbg4sasa/sasa-rdbg-cmds.ml b/tools/rdbg4sasa/sasa-rdbg-cmds.ml
index 79ef085e..22d9dedc 100644
--- a/tools/rdbg4sasa/sasa-rdbg-cmds.ml
+++ b/tools/rdbg4sasa/sasa-rdbg-cmds.ml
@@ -30,16 +30,18 @@ module IntMap = Map.Make(Int)
type round_st = {
cpt: int;
mask : string list; (* nodes we look the activation of *) (* XXX use an array! *)
- tbl : (int * bool * string list) IntMap.t
- (* maps event nb to round, round nb, and mask *)
+ tbl : (int * bool * string list * bool) IntMap.t;
+ (* maps event nb to round, round nb, and mask *)
+ silent:bool
}
let verbose = ref false
let round_st_init = {
- cpt = 1;
+ cpt = 0;
mask = [];
- tbl = IntMap.empty
+ tbl = IntMap.empty;
+ silent = false
}
let round_st_ref = ref round_st_init
@@ -47,11 +49,12 @@ let round_st_ref = ref round_st_init
let set_round_st_cpt n = round_st_ref := { !round_st_ref with cpt = n }
let set_round_st_mask m = round_st_ref := { !round_st_ref with mask = m }
let set_round_st_tbl t = round_st_ref := { !round_st_ref with tbl = t }
+let set_round_st_silent t = round_st_ref := { !round_st_ref with silent = t }
let round_reset i =
round_st_ref := round_st_init;
if !verbose then Printf.printf "\nInit round_st at event %d\n%!" i;
- set_round_st_tbl (IntMap.add i (1,true, []) !round_st_ref.tbl)
+ set_round_st_tbl (IntMap.add i (1, true, [], false) !round_st_ref.tbl)
let clean_round_st_tbl i =
set_round_st_tbl (IntMap.filter (fun k _v -> k <= i) !round_st_ref.tbl)
@@ -79,14 +82,22 @@ let enabled pl = (* returns the enabled processes *)
let (round : RdbgEvent.t -> bool) =
fun e ->
match IntMap.find_opt e.nb !round_st_ref.tbl with
- | Some (croundnb, round, cmask) ->
+ | Some (croundnb, round, cmask, csilent) ->
(* Printf.printf "round tabulated at e.nb %d: croundnb=%d round = %b\n%!" *)
(* e.nb croundnb round; *)
set_round_st_cpt croundnb;
set_round_st_mask cmask;
+ set_round_st_silent csilent;
round
| None ->
- if !round_st_ref.mask = [] && (e.data=[] || is_silent e) then false else
+ if is_silent e && not !round_st_ref.silent then (
+ (* when the conf becomes silent, we necessarily have a round *)
+ set_round_st_silent true;
+ set_round_st_cpt (!round_st_ref.cpt + 1);
+ true
+ )
+ else
+ if !round_st_ref.mask = [] && (e.data=[] || !round_st_ref.silent) then false else
let round =
if not
( (* we check if a round occurs when activated processes are available *)
@@ -105,7 +116,7 @@ let (round : RdbgEvent.t -> bool) =
set_round_st_mask (enabled pl);
let rm_me = get_removable pl in
if !verbose then (
- Printf.printf "\nMask (event %d): %s\n" e.nb
+ Printf.printf "\nMask (event %d): %s\n%!" e.nb
(String.concat "," !round_st_ref.mask);
Printf.printf "To remove from mask: %s\n%!" (String.concat "," rm_me)
);
@@ -137,7 +148,7 @@ let (round : RdbgEvent.t -> bool) =
Printf.printf "IntMap.add e.nb=%d round_nb=%d round= %b mask=%s\n%!"
e.nb !round_st_ref.cpt round (String.concat "," !round_st_ref.mask);
set_round_st_tbl
- (IntMap.add e.nb (!round_st_ref.cpt, round, !round_st_ref.mask)
+ (IntMap.add e.nb (!round_st_ref.cpt, round, !round_st_ref.mask, false)
!round_st_ref.tbl);
(* Printf.printf "round computed at e.nb %d: croundnb=%d round = %b\n%!"
e.nb !roundnb round; *)
@@ -149,10 +160,11 @@ let restore_round_nb i =
| None ->
(* Printf.printf "restore_round_nb: At event %d, nothing to restore\n%!" e.nb ; *)
()
- | Some (n,_, m) ->
+ | Some (n,_, m, s ) ->
(* Printf.printf "restore_round_nb: At event %d, restore the rn %d\n%!" e.nb n; *)
set_round_st_cpt n;
set_round_st_mask m;
+ set_round_st_silent s;
()
let sasa_next e =
--
GitLab