From 52b31d787b42e21b8c9ac74c4d5e4384712c04c5 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr>
Date: Thu, 19 Jan 2023 16:31:25 +0100
Subject: [PATCH] feat: add a fault injection button in the GUI
---
lib/sasa/sasaRun.ml | 108 ++++++++++++++++--------------
lib/sasacore/round.ml | 41 +++++++-----
lib/sasacore/simuState.ml | 28 +++++++-
lib/sasacore/simuState.mli | 16 ++++-
salut/test/Makefile.inc | 8 ++-
src/sasaMain.ml | 20 ++----
test/Makefile.inc | 12 ++--
test/dune2copy | 2 +-
tools/rdbg4sasa/gtkgui.ml | 82 ++++++++++++++++-------
tools/rdbg4sasa/sasa-rdbg-cmds.ml | 16 +++++
10 files changed, 214 insertions(+), 119 deletions(-)
diff --git a/lib/sasa/sasaRun.ml b/lib/sasa/sasaRun.ml
index c57e6504..f7b5c128 100644
--- a/lib/sasa/sasaRun.ml
+++ b/lib/sasa/sasaRun.ml
@@ -1,12 +1,12 @@
open Sasacore
(* open SasArg *)
-
+
let (get_action_value : (string * Data.v) list -> string -> string -> bool) =
fun sl pid a ->
let vn = Printf.sprintf "%s_%s" pid (StringOf.action a) in
match List.assoc_opt vn sl with
| Some (Data.B b) -> b
- | None
+ | None
| Some _ ->
Printf.printf "Error: can not find %s in [%s]\n" vn
(String.concat "," (fst (List.split sl)));
@@ -35,9 +35,9 @@ let (get_sl_out: bool -> 'v Process.t list -> bool list list -> RdbgPlugin.sl) =
fun enab pl ll ->
let str = if enab then "Enab_" else "" in
List.flatten (
- (* assert (List.length pl = List.length ll); *)
+ assert (List.length pl = List.length ll);
List.map2 (fun p enab_l ->
- (* assert (List.length p.actions = List.length enab_l); *)
+ assert (List.length p.actions = List.length enab_l);
List.map2 (fun a enab ->
Printf.sprintf "%s%s_%s" str p.pid (StringOf.action a), Data.B enab)
p.actions enab_l)
@@ -52,12 +52,12 @@ let (compute_potentiel: 'v SimuState.t -> RdbgPlugin.sl) =
if Register.get_potential () = None then []
else
[("potential", Data.F (SimuState.compute_potentiel st))]
-
+
let (compute_legitimate: bool -> 'v SimuState.t -> bool) =
fun silent st ->
silent ||
match Register.get_legitimate () with
- | None -> silent
+ | None -> silent
| Some f ->
let pidl = List.map (fun p -> p.Process.pid) st.network in
f pidl (SimuState.neigbors_of_pid st)
@@ -96,7 +96,7 @@ let (make_do: string array -> 'v SimuState.t -> RdbgPlugin.t) =
| None -> ( (* the first step *)
(* 1: Get enable processes *)
let pnall, enab_ll = Sasacore.SimuState.get_enable_processes st in
- let sasa_nenv = from_sasa_env st in
+ let sasa_nenv = from_sasa_env st in
let pot_sl = compute_potentiel st in
let silent = List.for_all (fun b -> not b) (List.flatten enab_ll) in
let legit = compute_legitimate silent st in
@@ -105,7 +105,7 @@ let (make_do: string array -> 'v SimuState.t -> RdbgPlugin.t) =
("silent", Data.B silent)::("legitimate", Data.B legit)::
("round", Data.B Round.s.is_round)::("round_nb", Data.I Round.s.cpt)::pot_sl
@ sasa_nenv @ (get_sl_out true pl enab_ll)
- )
+ )
| Some (pre_pnall, pre_enab_ll) ->
(* let was_silent = List.for_all (fun b -> not b) (List.flatten pre_enab_ll) in *)
(* if was_silent then failwith "Silent"; *)
@@ -126,10 +126,10 @@ let (make_do: string array -> 'v SimuState.t -> RdbgPlugin.t) =
let legit = compute_legitimate silent nst in
Round.update legit false activate_val enab_ll;
pre_enable_processes_opt := Some(pnall, enab_ll);
- sasa_config := st.config;
+ sasa_config := st.config;
("silent", Data.B silent)::("legitimate", Data.B legit)::
("round", Data.B Round.s.is_round)::("round_nb", Data.I Round.s.cpt)::pot_sl @
- sasa_nenv @ (get_sl_out true pl enab_ll)
+ sasa_nenv @ (get_sl_out true pl enab_ll)
in
let (step_internal_daemon: RdbgPlugin.sl -> RdbgPlugin.sl) =
fun sl_in ->
@@ -143,8 +143,8 @@ let (make_do: string array -> 'v SimuState.t -> RdbgPlugin.t) =
if silent then (
let enab = get_sl_out true pl enab_ll in
let trigger = (* set all trig var to false *)
- List.map (fun (n,v) -> String.sub n 5 ((String.length n) -5),v) enab
- in
+ List.map (fun (n,v) -> String.sub n 5 ((String.length n) -5),v) enab
+ in
("silent", Data.B silent)::("legitimate", Data.B legit)::
("round", Data.B Round.s.is_round)::("round_nb", Data.I Round.s.cpt)::pot_sl@
(from_sasa_env st) @ enab @ trigger
@@ -200,17 +200,15 @@ let (make_do: string array -> 'v SimuState.t -> RdbgPlugin.t) =
flush stderr
in
let exhaustive_search_reset () =
- match !exaustive_search_res with
- | None -> ()
- | Some _ ->
- let log = open_out (st.sasarg.topo ^ ".log") in
- ExhaustSearch.reset ();
- let path = ExhaustSearch.f log (st.sasarg.daemon=ExhaustCentralSearch) st in
- exaustive_search_res := Some path
- in
- let _exhaustive_search_reset () =
- ()
+ match !exaustive_search_res with
+ | None -> ()
+ | Some _ ->
+ let log = open_out (st.sasarg.topo ^ ".log") in
+ ExhaustSearch.reset ();
+ let path = ExhaustSearch.f log (st.sasarg.daemon=ExhaustCentralSearch) st in
+ exaustive_search_res := Some path
in
+ let _exhaustive_search_reset () = () in
let step =
match st.sasarg.daemon with
| DaemonType.Custom -> step_custom
@@ -220,7 +218,7 @@ let (make_do: string array -> 'v SimuState.t -> RdbgPlugin.t) =
in
let ss_table = Hashtbl.create 10 in
let step_dbg sl_in ctx cont =
- let sl_out = step sl_in in
+ let sl_out = step sl_in in
{ ctx with
(* RdbgEvent.nb = 0; *)
(* RdbgEvent.step = 0; (* we are actually in the middle of the first step! *) *)
@@ -242,44 +240,54 @@ let (make_do: string array -> 'v SimuState.t -> RdbgPlugin.t) =
let (mems_in : Data.subst list) = [] in
let (mems_out : Data.subst list) = [] in
let sasa_save_state i =
- let prgs = Random.get_state () in
- (* Printf.eprintf "Save state %i from sasa\n%!" i; *)
- Hashtbl.replace ss_table i
- (prgs, !sasa_config, !pre_enable_processes_opt, Round.get())
+ let prgs = Random.get_state () in
+ (* Printf.eprintf "Save state %i from sasa\n%!" i; *)
+ Hashtbl.replace ss_table i
+ (prgs, !sasa_config, !pre_enable_processes_opt, Round.get())
in
- let sasa_restore_state i =
- match Hashtbl.find_opt ss_table i with
- | Some (prgs, e, pepo, r) ->
- Random.set_state prgs;
- (* Printf.eprintf "Restore state %i from sasa\n%!" i; *)
- sasa_config := e; pre_enable_processes_opt := pepo;
- Round.set r;
- | None ->
- Printf.eprintf "Cannot restore state %i from sasa\n" i;
- flush stderr
+ let sasa_restore_state i =
+ if i = min_int then (* Is it a good idea to use this for fault injection? Not sure. *)
+ (match Register.get_fault () with
+ | None -> Printf.eprintf "Cannot inject faults: no fault function has been provided\n%!";
+ | Some f ->
+ Printf.eprintf "Perform a fault injection in sasa\n%!";
+ pre_enable_processes_opt := None;
+ sasa_config := SimuState.inject_fault_in_conf f st !sasa_config;
+ Round.reinit()
+ )
+ else
+ match Hashtbl.find_opt ss_table i with
+ | Some (prgs, e, pepo, r) ->
+ Random.set_state prgs;
+ (* Printf.eprintf "Restore state %i from sasa\n%!" i; *)
+ sasa_config := e; pre_enable_processes_opt := pepo;
+ Round.set r;
+ | None ->
+ Printf.eprintf "Cannot restore state %i from sasa\n" i;
+ flush stderr
in
- Round.reinit();
+ Round.reinit_mask();
{
id = prog_id;
inputs = vntl_i;
outputs= vntl_o;
reset= (match st.sasarg.daemon with
- | ExhaustCentralSearch | ExhaustSearch -> exhaustive_search_reset
- | _ -> reset
- );
+ | ExhaustCentralSearch | ExhaustSearch -> exhaustive_search_reset
+ | _ -> reset
+ );
kill=(fun _ -> flush stdout; flush stderr);
init_inputs=mems_in;
init_outputs=mems_out;
- step=step;
+ step=step;
step_dbg = step_dbg;
save_state = (match st.sasarg.daemon with
- | ExhaustCentralSearch | ExhaustSearch -> exhaustive_search_save_state
- | _ -> sasa_save_state
- );
+ | ExhaustCentralSearch | ExhaustSearch -> exhaustive_search_save_state
+ | _ -> sasa_save_state
+ );
restore_state = (match st.sasarg.daemon with
- | ExhaustCentralSearch | ExhaustSearch -> exhaustive_search_restore_state
- | _ -> sasa_restore_state
- );
+ | ExhaustCentralSearch | ExhaustSearch -> exhaustive_search_restore_state
+ | _ -> sasa_restore_state
+ );
}
@@ -297,10 +305,10 @@ let (make: string array -> RdbgPlugin.t) =
flush stdout;
exit 2
- | Assert_failure (file, line, col) ->
+ | Assert_failure (file, line, col) ->
prerr_string (
"\nError: oops, sasa internal error\n\tFile \""^ file ^
"\", line " ^ (string_of_int line) ^ ", column " ^
- (string_of_int col) ^ "\n") ;
+ (string_of_int col) ^ "\n") ;
flush stderr;
exit 2
diff --git a/lib/sasacore/round.ml b/lib/sasacore/round.ml
index 8d1a82d3..1c5c7193 100644
--- a/lib/sasacore/round.ml
+++ b/lib/sasacore/round.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 22/06/2022 (at 11:55) by Erwan Jahier> *)
+(* Time-stamp: <modified the 19/01/2023 (at 15:55) by Erwan Jahier> *)
type t = {
mutable first : bool;
@@ -19,6 +19,7 @@ let s:t = {
pre_acti_ll= [];
}
+
let all_false ll = List.for_all (List.for_all (not)) ll
let bool2str b = if b then "t" else "f"
@@ -42,7 +43,7 @@ let (update : bool -> bool -> bool list list -> bool list list -> unit) =
s.cpt <- 0;
s.round_mask <- enab_ll;
s.pre_acti_ll <- curr_acti_ll
- ) else (
+ ) else (
if s.cpt = 0 then (
(* Printf.printf "Round.update: the first round begins\n%!" ; *)
s.cpt <- 1
@@ -53,24 +54,27 @@ let (update : bool -> bool -> bool list list -> bool list list -> unit) =
s.is_round <- false;
)
else
- let new_mask = List.map2 (List.map2 (&&)) s.round_mask enab_ll in (* neutralize *)
- let new_mask = List.map2 (List.map2 (fun m a -> m&¬ a)) new_mask acti_ll in
- s.pre_acti_ll <- curr_acti_ll;
- let empty mask = all_false mask in
- if empty new_mask then
- (
- if not legit then s.cpt <- s.cpt+1;
- s.is_round <- true;
- s.round_mask <- enab_ll
+ try (
+ let new_mask = List.map2 (List.map2 (&&)) s.round_mask enab_ll in (* neutralize *)
+ let new_mask = List.map2 (List.map2 (fun m a -> m&¬ a)) new_mask acti_ll in
+ s.pre_acti_ll <- curr_acti_ll;
+ let empty mask = all_false mask in
+ if empty new_mask then
+ (
+ if not legit then s.cpt <- s.cpt+1;
+ s.is_round <- true;
+ s.round_mask <- enab_ll
+ )
+ else (
+ s.is_round <- false;
+ s.round_mask <- new_mask
)
- else (
- s.is_round <- false;
- s.round_mask <- new_mask
)
+ with _ -> assert false
)
(* ; debug_update "fin" legit *)
-
+
let (get : unit -> t_save) = fun () ->
s.first, s.moves, s.cpt, s.round_mask, s.pre_acti_ll
@@ -81,10 +85,15 @@ let (set : t_save -> unit) = fun (first, moves, cpt, round_mask, pre_acti_ll) ->
s.round_mask <- round_mask;
s.pre_acti_ll <- pre_acti_ll
-let reinit () =
+let reinit () =
s.first <- true;
s.is_round <- false;
s.moves <- 0;
s.cpt <- 0;
s.round_mask <- [];
s.pre_acti_ll <- []
+
+let reinit_mask () =
+ s.is_round <- false;
+ s.round_mask <- [];
+ s.pre_acti_ll <- []
diff --git a/lib/sasacore/simuState.ml b/lib/sasacore/simuState.ml
index 4f843ad7..eaa88394 100644
--- a/lib/sasacore/simuState.ml
+++ b/lib/sasacore/simuState.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 17/01/2023 (at 16:37) by Erwan Jahier> *)
+(* Time-stamp: <modified the 19/01/2023 (at 11:08) by Erwan Jahier> *)
open Register
open Topology
@@ -409,3 +409,29 @@ let (legitimate: 'v t -> bool) = fun st ->
| Some ulf ->
let pidl = List.map (fun p -> p.Process.pid) st.network in
ulf pidl (neigbors_of_pid st)
+
+
+let injected_fault_nb = ref 0
+let get_injected_fault_nb () = !injected_fault_nb
+
+
+
+let (inject_fault_in_conf : (int -> string -> 'v -> 'v) -> 'v t -> 'v Conf.t -> 'v Conf.t) =
+ fun ff st c ->
+
+ let update_nodes e p =
+ let nl = StringMap.find p.Process.pid st.neighbors in
+ let pid = p.Process.pid in
+ let v = Conf.get e pid in
+ let v = ff (List.length nl) pid v in
+ incr injected_fault_nb;
+ Conf.set e pid v
+ in
+ let nc = List.fold_left update_nodes c st.network in
+ nc
+
+let (inject_fault : (int -> string -> 'v -> 'v) -> 'v t -> 'v t) =
+ fun ff st ->
+ let nc = inject_fault_in_conf ff st st.config in
+ let st = { st with config = nc } in
+ update_config nc st
diff --git a/lib/sasacore/simuState.mli b/lib/sasacore/simuState.mli
index 156738d9..1ed8aac3 100644
--- a/lib/sasacore/simuState.mli
+++ b/lib/sasacore/simuState.mli
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 06/04/2022 (at 14:51) by Erwan Jahier> *)
+(* Time-stamp: <modified the 19/01/2023 (at 11:07) by Erwan Jahier> *)
(** The module is used by
- the main sasa simulation loop (in ../../src/sasaMain.ml)
@@ -7,7 +7,7 @@
*)
-
+
(* type 'v t = SasArg.t * 'v layout * 'v Conf.t *)
type 'v t = {
config: 'v Conf.t;
@@ -21,7 +21,7 @@ val make : bool -> string array -> 'v t
type 'v enable_processes =
('v Process.t * 'v Register.neighbor list * Register.action) list list * bool list list
-
+
val get_enable_processes: 'v t -> 'v enable_processes
(** [update_config e c] updates c using e *)
@@ -29,6 +29,16 @@ val update_config: 'v Conf.t -> 'v t -> 'v t
val update_env_with_init : 'v Conf.t -> 'v Process.t list -> 'v Conf.t
+(** inject a fault in a configuration using the registered (user) fault function
+
+nb : inject_fault_in_conf uses only the static part of SimuState.t
+*)
+val inject_fault : (int -> string -> 'v -> 'v) -> 'v t -> 'v t
+
+
+val inject_fault_in_conf : (int -> string -> 'v -> 'v) -> 'v t -> 'v Conf.t -> 'v Conf.t
+val get_injected_fault_nb : unit -> int
+
(** Get pid's state and neighbors *)
val neigbors_of_pid : 'v t -> string -> 'v * ('v Register.neighbor * string) list
diff --git a/salut/test/Makefile.inc b/salut/test/Makefile.inc
index e65fb7f1..b1839174 100644
--- a/salut/test/Makefile.inc
+++ b/salut/test/Makefile.inc
@@ -47,8 +47,12 @@ RUN_KIND2=$(ROOTDIR)/salut/test/run-kind2.sh
make $*.dot $*_const.lus
luciole-rif lv6 $(LIB_LUS) $*.lus $*_const.lus -n $* -exec
-%.rdbg:
- make $*.dot $*_const.lus
+%.rdbg: %.cma
+ make $*_const.lus
+ rdbg -l 10000 -sut-nd "lv6 $(LIB_LUS) $*_const.lus $*.lus -n $* -exec"
+
+%.rdbgui: %.cma
+ make $*_const.lus
rdbgui4sasa -l 10000 -sut-nd "lv6 $(LIB_LUS) $*_const.lus $*.lus -n $* -exec"
##########################################################################################"
diff --git a/src/sasaMain.ml b/src/sasaMain.ml
index e70fbdf1..ea2ee657 100644
--- a/src/sasaMain.ml
+++ b/src/sasaMain.ml
@@ -50,18 +50,6 @@ let (print_step : out_channel -> 'v SimuState.t -> int -> int -> string -> strin
open Sasacore.SimuState
module StringMap = Map.Make(String)
-let injected_fault_nb = ref 0
-let inject_fault ff st =
- let update_nodes e p =
- let nl = StringMap.find p.Process.pid st.neighbors in
- let pid = p.Process.pid in
- let v = Conf.get e pid in
- let v = ff (List.length nl) pid v in
- incr injected_fault_nb;
- Conf.set e pid v
- in
- let e = List.fold_left update_nodes st.config st.network in
- update_config e st
let plur i = if i>1 then "s" else ""
@@ -93,7 +81,7 @@ let (simustep: out_channel -> int -> int -> string -> 'v SimuState.t -> 'v SimuS
(* not (args.rif) && *)
silent
then (
- match if !injected_fault_nb > 0 then None else Register.get_fault () with
+ match if SimuState.get_injected_fault_nb () > 0 then None else Register.get_fault () with
| None ->
Round.update leg true enab_ll enab_ll;
print_step log st n i "t" pot st.sasarg st.config pl (bll2str enab_ll) enab_ll;
@@ -107,12 +95,12 @@ let (simustep: out_channel -> int -> int -> string -> 'v SimuState.t -> 'v SimuS
str Round.s.moves (plur Round.s.moves) (n-i) (plur (n-i))
Round.s.cpt (plur Round.s.cpt);
Printf.fprintf log "%s==> Inject a fault\n%!" str;
- let st = inject_fault ff st in
+ let st = SimuState.inject_fault ff st in
let all, enab_ll = Sasacore.SimuState.get_enable_processes st in
st, all, enab_ll
)
else if leg then (
- match if !injected_fault_nb > 0 then None else Register.get_fault () with
+ match if SimuState.get_injected_fault_nb() > 0 then None else Register.get_fault () with
| None ->
Round.update leg true enab_ll enab_ll;
print_step log st n i "t" pot st.sasarg st.config pl activate_val enab_ll;
@@ -125,7 +113,7 @@ let (simustep: out_channel -> int -> int -> string -> 'v SimuState.t -> 'v SimuS
"\n%sThis algo reached a legitimate configuration after %i move%s, %i step%s, %i round%s.\n"
str Round.s.moves (plur Round.s.moves) (n-i) (plur (n-i)) (Round.s.cpt-1) (plur (Round.s.cpt-1));
Printf.fprintf log "%s==> Inject a fault\n%!" str;
- let st = inject_fault ff st in
+ let st = SimuState.inject_fault ff st in
let all, enab_ll = Sasacore.SimuState.get_enable_processes st in
st, all, enab_ll
)
diff --git a/test/Makefile.inc b/test/Makefile.inc
index 030a0d95..5a47df66 100644
--- a/test/Makefile.inc
+++ b/test/Makefile.inc
@@ -1,4 +1,4 @@
-# Time-stamp: <modified the 18/01/2023 (at 21:20) by Erwan Jahier>
+# Time-stamp: <modified the 19/01/2023 (at 14:18) by Erwan Jahier>
#
# Define some default rules that ought to work most of the time
#
@@ -33,6 +33,10 @@ endif
topology=$* dune build
%.cma: %.dot
topology=$* dune build
+%.cmxa: %.dot
+ topology=$* dune build
+%.a: %.dot
+ topology=$* dune build
genclean:
@@ -95,10 +99,10 @@ endif
############################################################################################
%.rdbg: %.dot
- ledit -h rdbg-history -x rdbg --sasa -sut "sasa $< $(DAEMON)" -l 500
+ ledit -h rdbg-history -x rdbg --sasa -sut "sasa $< $(DAEMON)" -l 10000
%.rdbg-test: %.cma
- rdbg --sasa -sut "sasa $*.dot $(DAEMON)" -go --input some_session -l 500
+ rdbg --sasa -sut "sasa $*.dot $(DAEMON)" -go --input some_session -l 10000
%.rdbgui: %.cma
- rdbgui4sasa -sut "sasa $*.dot $(DAEMON)"
+ rdbgui4sasa -sut "sasa $*.dot $(DAEMON)" -l 10000
diff --git a/test/dune2copy b/test/dune2copy
index 62240466..70215208 100644
--- a/test/dune2copy
+++ b/test/dune2copy
@@ -3,7 +3,7 @@
(library
(name user_algo_files) ;; a fake name because "%{env:topology=ring4}" is rejected
(libraries algo)
- (wrapped false) ; so that user_algo_files is not used in the .cm*
+; (wrapped false) ; so that user_algo_files is not used in the .cm*
(library_flags -linkall)
)
diff --git a/tools/rdbg4sasa/gtkgui.ml b/tools/rdbg4sasa/gtkgui.ml
index 12acb22e..41750b2d 100644
--- a/tools/rdbg4sasa/gtkgui.ml
+++ b/tools/rdbg4sasa/gtkgui.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 16/01/2023 (at 21:36) by Erwan Jahier> *)
+(* Time-stamp: <modified the 19/01/2023 (at 16:30) by Erwan Jahier> *)
#thread
#require "lablgtk3"
@@ -242,9 +242,7 @@ let start () =
ckpt_list := [!e];
!e.save_state !e.nb
-let restart p _ =
- Seed.replay_seed := true;
- let seed = Seed.get dotfile in
+let start_with_seed p seed =
Seed.set seed;
p (Printf.sprintf "Restarting using the seed %d" seed);
!e.RdbgEvent.reset(); (* should be done after the see reset! *)
@@ -253,6 +251,52 @@ let restart p _ =
start ();
d()
+let restart p _ =
+ Seed.replay_seed := true;
+ let seed = Seed.get dotfile in
+ (* change_sasa_seed seed; *)
+ start_with_seed p seed
+
+
+let restart_new_seed p _ =
+ Seed.replay_seed := false;
+ Seed.reset();
+ let seed = Seed.get "restart_new_seed" in
+ change_sasa_seed seed;
+ p (Printf.sprintf "Restarting using the seed %d" seed);
+ start_with_seed p seed
+
+let _restart_new_seed p _ =
+ Seed.reset();
+ let seed = Seed.get "restart_new_seed" in
+ change_sasa_seed seed;
+ Seed.set (seed);
+ !e.RdbgEvent.reset();
+ p (Printf.sprintf "Restarting using the seed %d" seed);
+
+ e:=RdbgStdLib.run ~call_hooks:true ();
+ Round.reinit();
+ redos := [1];
+ ckpt_list := [!e];
+
+ if args.salut_mode then
+ (* in this mode, the hook plays first to provide fake values to sasa
+ but the hook does not need input at this first step
+ *)
+ e:=goto_hook_exit !e;
+ e:=goto_hook_call !e;
+ d()
+
+let inject p _ =
+ let seed = Seed.get dotfile in
+ Seed.set seed;
+ p (Printf.sprintf "A fault is injected.\nThe seed is set to %d\n" seed);
+ Round.reinit_mask();
+ !e.restore_state min_int;
+ start ();
+ d()
+
+
let counter_map = Hashtbl.create 0
let update_daemongui_tbl e =
@@ -869,31 +913,17 @@ let main () =
oracle_button#misc#hide(); (* indeed, in the defaut mode (manual central), it should be hided *)
oracle_button_ref := Some oracle_button
);
- let _ = make_button `REFRESH "Restar_t" "Restart from the beginning"
+ if not args.salut_mode then (
+ let _ =
+ make_button `ADD "Inject _Fault" "Inject a fault (the Algo.fault_function should be set)"
+ (button_cb true true (inject p))
+ in
+ ());
+ let _ = make_button `GOTO_FIRST "Restar_t" "Restart from the beginning"
(button_cb true true (restart p))
in
let _ = make_button `REFRESH "_New Seed" "Restart from the beginning using a New Seed"
- (button_cb true true
- (fun ()->
- Seed.reset(); Seed.replay_seed := false;
- let seed = Seed.get dotfile in
- change_sasa_seed seed;
- Seed.set (seed);
- !e.RdbgEvent.reset();
- p (Printf.sprintf "Restarting using the seed %d" seed);
-
- e:=RdbgStdLib.run ~call_hooks:true ();
- Round.reinit();
- redos := [1];
- ckpt_list := [!e];
-
- if args.salut_mode then
- (* in this mode, the hook plays first to provide fake values to sasa
- but the hook does not need input at this first step
- *)
- e:=goto_hook_exit !e;
- e:=goto_hook_call !e;
- d()))
+ (button_cb true true (restart_new_seed p))
in
let graph () =
let graph_button = button ~use_mnemonic:true ~packing:bbox#add () in
diff --git a/tools/rdbg4sasa/sasa-rdbg-cmds.ml b/tools/rdbg4sasa/sasa-rdbg-cmds.ml
index a69192e2..8bc28af8 100644
--- a/tools/rdbg4sasa/sasa-rdbg-cmds.ml
+++ b/tools/rdbg4sasa/sasa-rdbg-cmds.ml
@@ -189,6 +189,21 @@ let r () =
(* if !ckpt_list = [] then *)
ckpt_list := [!e];;
+(**********************************************************************)
+(* Fault injection *)
+
+let inject_a_fault () =
+ let seed = Seed.get dotfile in
+ Seed.set seed;
+ Printf.printf "Restarting using the seed %d\n" seed;
+ Round.reinit_mask();
+ !e.restore_state min_int;
+ redos := [1];
+ ckpt_list := [!e];;
+
+
+let iaf = inject_a_fault
+
(**********************************************************************)
(* Move forward until silence *)
@@ -314,6 +329,7 @@ let _ = add_doc_entry
"viol" "unit -> unit" "Move forward until the oracle is violated"
"sasa" "sasa-rdbg-cmds.ml"
+
(**********************************************************************)
(* Potential *)
--
GitLab