diff --git a/lib/sasacore/simuState.ml b/lib/sasacore/simuState.ml
index 801290eeb5449b8ea67f119570ad518f9428ff14..a62f42ca6b88bb0c1e38865af00e87a2d618c3e1 100644
--- a/lib/sasacore/simuState.ml
+++ b/lib/sasacore/simuState.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 16/06/2022 (at 23:26) by Erwan Jahier> *)
+(* Time-stamp: <modified the 22/06/2022 (at 22:49) by Erwan Jahier> *)
open Register
open Topology
@@ -54,9 +54,9 @@ let (neigbors_of_pid : 'v t -> pid -> 's * ('s neighbor * pid) list) =
match StringMap.find_opt pid st.neighbors with
| Some x -> x
| None ->
- failwith (
- Printf.sprintf "no %s found in %s" pid
- (String.concat "," (List.map (fun p -> p.Process.pid) st.network)))
+ Printf.eprintf "no %s found in %s\n%!" pid
+ (String.concat "," (List.map (fun p -> p.Process.pid) st.network));
+ exit 2
in
Conf.get st.config pid, List.map (fun n -> n, n.Register.pid) nl
diff --git a/src/sasaMain.ml b/src/sasaMain.ml
index 0fee1b8466f6123bcb9cfbd1c579ee807ff38141..1edce3abfe989dc6628262a04ad46ac95936b4fd 100644
--- a/src/sasaMain.ml
+++ b/src/sasaMain.ml
@@ -75,7 +75,9 @@ let (simustep: out_channel -> int -> int -> string -> 'v SimuState.t -> 'v SimuS
if verb then Printf.fprintf log "==> SasaSimuState.simustep :1: Get enable processes\n%!";
let all, enab_ll = Sasacore.SimuState.get_enable_processes st in
if verb then Printf.fprintf log "==> SasaSimuState.simustep: Get the potential\n%!";
- let pot = try string_of_float (SimuState.compute_potentiel st) with _ -> "" in
+ let pot = if Register.get_potential () = None then "" else
+ string_of_float (SimuState.compute_potentiel st)
+in
let pl = st.network in
if verb then Printf.fprintf log "==> SasaSimuState.simustep: is it legitimate?\n%!";
let silent = List.for_all (fun b -> not b) (List.flatten enab_ll) in
diff --git a/test/Makefile.inc b/test/Makefile.inc
index 6efb3bd6f914dc87927208d7830a5264213338cb..3c3c06a2c09bad7d493e455f5cf1f8c2cbe60d07 100644
--- a/test/Makefile.inc
+++ b/test/Makefile.inc
@@ -1,4 +1,4 @@
-# Time-stamp: <modified the 26/05/2022 (at 10:07) by Erwan Jahier>
+# Time-stamp: <modified the 22/06/2022 (at 21:33) by Erwan Jahier>
#
# Define some default rules that ought to work most of the time
#
@@ -49,7 +49,7 @@ OCAMLC=ocamlfind ocamlc -bin-annot
$(sasa) $(sasaopt) $*.dot > $*.rif
%.pdf:
- osage -Tpdf $*.dot -o $*.pdf
+ dot -Tpdf $*.dot -o $*.pdf
xpdf $*.pdf
%.ocd: %.ml
diff --git a/test/async-unison/async_unison_oracle.lus b/test/async-unison/async_unison_oracle.lus
index 37424f3ea539d473076286643920f9f9ba30bf04..bb5a8b837d1975752759a2bc84fe725145b178dd 100644
--- a/test/async-unison/async_unison_oracle.lus
+++ b/test/async-unison/async_unison_oracle.lus
@@ -21,13 +21,10 @@ let
(i<=j or (adjacency[l/pn][l mod pn] => is_close(State[l/pn], State[l mod pn])));
tel
-node async_unison_oracle (Legitimate:bool; Enab, Acti: bool^an^pn; State : int^pn)
+node async_unison_oracle (Legitimate:bool; Enab, Acti: bool^an^pn; State : int^pn; round:bool; round_nb:int)
returns (res:bool);
-var
- rn:int;
let
- rn = round_count(round <<an,pn>>(Enab,Acti), silent<<an,pn>>(Enab));
- res = redge(Legitimate) => (rn <= diameter*card);
+ res = redge(Legitimate) => (round_nb <= diameter*card);
tel
node redge(x:bool) returns (res:bool);
diff --git a/test/bfs-spanning-tree/Makefile b/test/bfs-spanning-tree/Makefile
index bb37c8e451e354182610fd666e0189b8d45087c2..90dfaf5f66ad62749b1cc4421c03035e3757ad30 100644
--- a/test/bfs-spanning-tree/Makefile
+++ b/test/bfs-spanning-tree/Makefile
@@ -1,4 +1,4 @@
-# Time-stamp: <modified the 11/06/2022 (at 16:13) by Erwan Jahier>
+# Time-stamp: <modified the 22/06/2022 (at 10:17) by Erwan Jahier>
DECO_PATTERN="0:root.ml 1-:p.ml"
-include ../Makefile.dot
@@ -23,11 +23,11 @@ test2: fig51.cmxs
lurette0: fig51_noinit.cmxs fig51_noinit.lut fig51_noinit_oracle.lus
lurette --sasa -o lurette.rif \
- -env "sasa fig51_noinit.dot -dd -rif" \
+ -env "sasa fig51_noinit.dot -dd -rif -seed 42" \
-oracle "lv6 fig51_noinit_oracle.lus -n oracle"
test_rdbg: fig51_noinit.ml fig51_noinit.lut
- ledit rdbg --sasa -sut "sasa fig51_noinit.dot -dd " -go --input some_session
+ ledit rdbg --sasa -sut "sasa fig51_noinit.dot " -go --input some_session
clean: genclean
rm -f fig*oracle.lus fig5*.ml
diff --git a/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus b/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus
index 6551027a408973f0e4cedf2d370925268476b965..26b225726b802864fa1f4492b8a5005107d7ab34 100644
--- a/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus
+++ b/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus
@@ -1,19 +1,16 @@
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))
+ (legitimate: bool; Enab, Acti: bool^an^pn; config:int^(2*pn);round:bool; round_nb:int)
returns (ok:bool);
var
CD_disable:bool;
- Silent, Round : bool;
- RoundNb:int;
+ Silent : bool;
let
- 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
- theorem_5_18 (Silent, RoundNb);
+ ok = lemma_5_16 (round_nb, CD_disable) and
+ theorem_5_18 (Silent, round_nb);
tel
-----------------------------------------------------------------------------
diff --git a/test/coloring/Makefile b/test/coloring/Makefile
index e849c2bb47e501ce02a7120ad7e5590478d64fb6..b0b0d7d9d5136f78dfe716ffddbbebcc2f47061e 100644
--- a/test/coloring/Makefile
+++ b/test/coloring/Makefile
@@ -1,4 +1,4 @@
-# Time-stamp: <modified the 10/06/2022 (at 16:29) by Erwan Jahier>
+# Time-stamp: <modified the 22/06/2022 (at 10:56) 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 -seed 42" \
-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 0fae2f5cd9e795d05eabbef4c3ce00981abb49e2..668b2f0d069043f78dac88a02e4b27e96cad09cf 100644
--- a/test/coloring/coloring_oracle.lus
+++ b/test/coloring/coloring_oracle.lus
@@ -4,49 +4,32 @@ include "../lustre/oracle_utils.lus"
-----------------------------------------------------------------------------
-- Lemma 3.14 The execution e terminates after at most n-1 moves
-- (under a Locally Central demon).
-node lemma_3_14<<const an:int; const pn: int>> (Enab, Acti: bool^an^pn) returns (res:bool);
-var
- MoveNb:int;
- Silent:bool;
+node lemma_3_14<<const an:int; const pn: int>> (legitimate: bool; Enab, Acti: bool^an^pn) returns (res:bool;MoveNb:int);
+--var
+-- MoveNb:int;
let
MoveNb = move_count(Acti);
- Silent = silent<<an,pn>>(Enab);
- res = Silent => (MoveNb) <= pn-1;
+ res = legitimate => (MoveNb) <= pn-1;
tel
-----------------------------------------------------------------------------
-- Theorem 3.17 The stabilization time of Color is at most one round
-- (under a Locally Central demon).
-node theorem_3_17<<const an:int; const pn:int>> (Enab, Acti: bool^an^pn)
-returns (res:bool; RoundNb:int);
-var
- Round:bool;
--- RoundNb:int;
+function theorem_3_17<<const an:int; const pn:int>> (Enab, Acti: bool^an^pn; round_nb:int)
+returns (res:bool);
let
- Round = round <<an,pn>>(Enab,Acti);
- RoundNb = round_count(Round, silent<<an,pn>>(Enab));
- res = RoundNb <= 1; -- from theorem 3.17 page 29
+ res = round_nb <= 1; -- from theorem 3.17 page 29
tel
-node coloring_oracle0<<const an:int; const pn:int>> (Enab, Acti: bool^an^pn)
-returns (res:bool; RoundNb:int);
+node coloring_oracle<<const an:int; const pn:int>> (legitimate: bool; potential:real; Enab, Acti: bool^an^pn;
+ config:int^pn; round:bool; round_nb:int)
+returns (res:bool; move_nb:int);
var res0:bool;
let
- res0, RoundNb = theorem_3_17<<an,pn>>(Enab,Acti);
- res = res0 and lemma_3_14<<an,pn>>(Enab,Acti);
-tel
-
-
--- Hide the second output of coloring_oracle0
--- Indeed, the automatically generated oracles (out of the dot files) suppose
--- that this node has only one output.
-node coloring_oracle<<const an:int; const pn:int>> (Enab, Acti: bool^an^pn)
-returns (res:bool);
-var RoundNb:int;
-let
- res, RoundNb = coloring_oracle0<<an,pn>>(Enab,Acti);
+ res0, move_nb = lemma_3_14<<an,pn>>(legitimate, Enab,Acti);
+ res = theorem_3_17<<an,pn>>(Enab,Acti, round_nb)
+ and res0
+ ;
tel
-
-
node test=coloring_oracle<< 5,2 >>
diff --git a/test/coloring/ring_oracle.lus b/test/coloring/ring_oracle.lus
index 0d22238e6499db280c4369c45951b16815083b27..7a256c5d6d913f0ef535648e9d34d1e8bb366f3c 100644
--- a/test/coloring/ring_oracle.lus
+++ b/test/coloring/ring_oracle.lus
@@ -1,11 +1,11 @@
--- 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
+-- Automatically generated by /home/jahier/.opam/4.13.1/bin/sasa version "v4.6.0" ("169b4f7")
+-- on crevetete the 22/6/2022 at 10:52:23
+--sasa -glos ring.dot
include "coloring_oracle.lus"
const an=1; -- actions number
const pn=7; -- processes number
-const degree=2;
+const max_degree=2;
const min_degree=2;
const mean_degree=2.000000;
const diameter=3;
@@ -14,7 +14,9 @@ const links_number=7;
const is_cyclic=true;
const is_connected=true;
const is_a_tree=false;
-const adjency=[
+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],
@@ -23,15 +25,19 @@ const adjency=[
[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; r:int);
+node oracle(legitimate:bool;potential:real;
+ p1_c:int;p2_c:int;p3_c:int;p4_c:int;p5_c:int;p6_c:int;p7_c:int;
+ 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;round:bool; round_nb:int)
+returns (ok:bool; move_nb:int);
var
- Acti:bool^1^7;
- Enab:bool^1^7;
+ Acti:bool^an^pn;
+ Enab:bool^an^pn;
+ Config:p1_c^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]];
+ Config = [p1_c,p2_c,p3_c,p4_c,p5_c,p6_c,p7_c];
- ok, r = coloring_oracle0<<an,pn>>(Enab,Acti);
+ ok,move_nb = coloring_oracle(legitimate,potential, Enab, Acti, Config, round, round_nb);
tel
-
-
diff --git a/test/dijkstra-ring/dijkstra_ring_oracle.lus b/test/dijkstra-ring/dijkstra_ring_oracle.lus
index c63d1279b96ed62ed960351c101ee6fdcdf60bc9..4b570f77090f23b31bb521509523aa0a3e0e4f16 100644
--- a/test/dijkstra-ring/dijkstra_ring_oracle.lus
+++ b/test/dijkstra-ring/dijkstra_ring_oracle.lus
@@ -33,7 +33,8 @@ tel
node dijkstra_ring_oracle_cov<<const an:int; const pn:int>>
-(legitimate:bool; Enab, Acti: bool^an^pn) returns (ok:bool; WortCaseReached : bool);
+(legitimate:bool; Enab, Acti: bool^an^pn;round:bool; round_nb:int)
+returns (ok:bool; WortCaseReached : bool);
var
WortCase : int;
MoveNb:int;
diff --git a/test/dijkstra-ring/ring_oracle.lus b/test/dijkstra-ring/ring_oracle.lus
index 38a80fc2cc3efcaf7bdb9287f59bccfb813558f0..e5876c4b202e00d3d08f4e51899dc8d290ef37d9 100644
--- a/test/dijkstra-ring/ring_oracle.lus
+++ b/test/dijkstra-ring/ring_oracle.lus
@@ -30,7 +30,7 @@ const k=3;
node oracle(legitimate:bool;
root_c:int;p2_c:int;p3_c:int;p4_c:int;p5_c:int;p6_c:int;p7_c:int;p8_c:int;
Enab_root_T,Enab_p2_T,Enab_p3_T,Enab_p4_T,Enab_p5_T,Enab_p6_T,Enab_p7_T,Enab_p8_T:bool;
- root_T,p2_T,p3_T,p4_T,p5_T,p6_T,p7_T,p8_T:bool)
+ root_T,p2_T,p3_T,p4_T,p5_T,p6_T,p7_T,p8_T:bool;round:bool; round_nb:int)
returns (ok, WCReached:bool);
var
Acti:bool^an^pn;
@@ -39,5 +39,5 @@ let
Acti = [[root_T],[p2_T],[p3_T],[p4_T],[p5_T],[p6_T],[p7_T],[p8_T]];
Enab = [[Enab_root_T],[Enab_p2_T],[Enab_p3_T],[Enab_p4_T],[Enab_p5_T],[Enab_p6_T],[Enab_p7_T],[Enab_p8_T]];
- ok, WCReached = dijkstra_ring_oracle_cov(legitimate, Enab, Acti);
+ ok, WCReached = dijkstra_ring_oracle_cov(legitimate, Enab, Acti, round, round_nb);
tel
diff --git a/test/lustre/oracle_utils.lus b/test/lustre/oracle_utils.lus
index 3c15bb85d527d252087c4b55d643e9a1bd54d516..e8ef92faa226a6f713a192bc3f290d795160e981 100644
--- a/test/lustre/oracle_utils.lus
+++ b/test/lustre/oracle_utils.lus
@@ -5,13 +5,13 @@ include "demon.lus"
-----------------------------------------------------------------------------
-- An algo is silent when no action is enable
-function _silent<<const an: int; const pn: int>> (Enab: bool^an^pn) returns (ok:bool);
+function silent<<const an: int; const pn: int>> (Enab: bool^an^pn) returns (ok:bool);
let
ok = all_false<<an, pn>>(Enab);
tel
-----------------------------------------------------------------------------
-node _move_count (tab_acti:bool^an^pn) returns (nb_act:int);
+node move_count (tab_acti:bool^an^pn) returns (nb_act:int);
let
nb_act = (0 -> pre(nb_act)) + (red<<count_true_acc<<an>>,pn>>(0,tab_acti));
tel
diff --git a/test/rsp-tree/rsp_tree_oracle.lus b/test/rsp-tree/rsp_tree_oracle.lus
index ff4fa81d8c103354cc18a3fec018bd987c56b46f..0911a5104abecd891c679188566bc73511cf9ed5 100644
--- a/test/rsp-tree/rsp_tree_oracle.lus
+++ b/test/rsp-tree/rsp_tree_oracle.lus
@@ -2,16 +2,14 @@ include "../lustre/oracle_utils.lus"
type string;
-node rsp_tree_oracle(legit:bool; Enab, Acti:bool^an^pn; config: int ^(3*pn)) returns (res:bool);
+node rsp_tree_oracle(legit:bool; Enab, Acti:bool^an^pn; config: int ^(3*pn); round:bool; round_nb:int)
+returns (res:bool);
var
- Silent,Round:bool;
- RoundNb:int;
+ Silent:bool;
let
- Round = round <<an,pn>>(Enab,Acti);
Silent = silent<<an,pn>>(Enab);
- RoundNb = round_count(Round, Silent);
-- Theorem 3 in the case of connected graphs
- res = (not(Silent) and is_connected) => (RoundNb < 3*card+diameter);
+ res = (not(Silent) and is_connected) => (round_nb < 3*card+diameter);
tel
-- end of some_node
diff --git a/test/st-KK06-algo1/st_KK06_algo1_oracle.lus b/test/st-KK06-algo1/st_KK06_algo1_oracle.lus
index 53d844d4a56f78df0b1df241cd9e02ccd9721a16..e01c9aecca055ee41d9ff4e53132e541ec6bfdf0 100644
--- a/test/st-KK06-algo1/st_KK06_algo1_oracle.lus
+++ b/test/st-KK06-algo1/st_KK06_algo1_oracle.lus
@@ -2,7 +2,7 @@
include "../lustre/utils.lus"
node st_KK06_algo1_oracle<<const an:int; const pn:int>>
-(legitimate:bool; Enab,Acti:bool^an^pn; Config: int^pn) returns (ok:bool);
+(legitimate:bool; Enab,Acti:bool^an^pn; Config: int^pn;round:bool; round_nb:int) returns (ok:bool);
var
moves : int;
let
diff --git a/test/st-KK06-algo2/st_KK06_algo2_oracle.lus b/test/st-KK06-algo2/st_KK06_algo2_oracle.lus
index d77ada0ca0e1e6b83e33001d487554cb8dee5c6b..afc3d1a64354a87d530d2425f03b99cbb3d56b83 100644
--- a/test/st-KK06-algo2/st_KK06_algo2_oracle.lus
+++ b/test/st-KK06-algo2/st_KK06_algo2_oracle.lus
@@ -3,7 +3,7 @@ include "../lustre/utils.lus"
const bigN = 2*card;
-node st_KK06_algo2_oracle<<const an:int; const pn:int>>(leg:bool; Enab,Acti:bool^an^pn; Config: int^pn)
+node st_KK06_algo2_oracle<<const an:int; const pn:int>>(leg:bool; Enab,Acti:bool^an^pn; Config: int^pn;round:bool; round_nb:int)
returns (ok:bool);
var
moves : int;
diff --git a/test/unison/unison_oracle.lus b/test/unison/unison_oracle.lus
index 861e74561564a56900abede055fdeabca8a5d66a..c7a09189f909630dda8a6fd65d05acd1bbc2b731 100644
--- a/test/unison/unison_oracle.lus
+++ b/test/unison/unison_oracle.lus
@@ -26,7 +26,8 @@ let
tel
-----------------------------------------------------------------------------
-node unison_oracle<<const an:int; const pn:int>> (legit:bool; Enab, Acti: bool^an^pn; Config:int^pn)
+node unison_oracle<<const an:int; const pn:int>> (legit:bool; Enab, Acti: bool^an^pn; Config:int^pn;
+ round:bool; round_nb:int)
returns (ok:bool);
let
diff --git a/tools/rdbg4sasa/gtkgui.ml b/tools/rdbg4sasa/gtkgui.ml
index ce400704c5c692dc807cc76d9986ee386d84fe44..32cb0bce7dfe8c69cdc8f03e54b970c43306c8e3 100644
--- a/tools/rdbg4sasa/gtkgui.ml
+++ b/tools/rdbg4sasa/gtkgui.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 21/06/2022 (at 17:50) by Erwan Jahier> *)
+(* Time-stamp: <modified the 22/06/2022 (at 23:27) by Erwan Jahier> *)
#thread
#require "lablgtk3"
@@ -742,7 +742,6 @@ let main () =
let step () =
if not (is_silent ~dflt:false !e) || (not args.salut_mode && !e.kind <> Ltop) then (
- Printf.printf "a_gui_step is called \n%!";
e := a_gui_step !e;
d()
)