From f3f315124d5c0832a120b151426020d4f21a4a78 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr>
Date: Thu, 3 Jun 2021 14:08:19 +0200
Subject: [PATCH] Update: some progress to get time-travel working with
rdbgui4sasa
---
tools/rdbg4sasa/gtkgui.ml | 215 ++++++++++++++++++------------
tools/rdbg4sasa/sasa-rdbg-cmds.ml | 90 +++++++------
2 files changed, 176 insertions(+), 129 deletions(-)
diff --git a/tools/rdbg4sasa/gtkgui.ml b/tools/rdbg4sasa/gtkgui.ml
index 966af367..90fe497d 100644
--- a/tools/rdbg4sasa/gtkgui.ml
+++ b/tools/rdbg4sasa/gtkgui.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 31/05/2021 (at 11:56) by Erwan Jahier> *)
+(* Time-stamp: <modified the 03/06/2021 (at 12:02) by Erwan Jahier> *)
#thread
#require "lablgtk3"
@@ -117,14 +117,23 @@ let display_event b =
(**********************************************************************************)
(* *)
-let goto_hook_call () =
- if custom_mode then (
- e := next_cond !e (fun e -> e.name = "mv_hook" && e.kind = Call)
- )
+let goto_hook_call e =
+ if custom_mode then
+ next_cond e (fun e -> e.name = "mv_hook" && e.kind = Call)
+ else
+ e
+
+let goto_hook_exit e =
+ if custom_mode then
+ next_cond e (fun e -> e.name = "mv_hook" && e.kind = Exit)
+ else
+ e
-let goto_hook_exit () =
+let goto_top e =
if custom_mode then
- e := next_cond !e (fun e -> e.name = "mv_hook" && e.kind = Exit)
+ next_cond e (fun e -> e.kind = Ltop)
+ else
+ e
let init_rdbg_hook () =
let guidaemon sl =
@@ -175,7 +184,7 @@ let init_rdbg_hook () =
let set_tooltip b = b#misc#set_tooltip_text
-let custom_daemon p gtext vbox step_button round_button legitimate_button =
+let custom_daemon p gtext vbox step_button back_step_button round_button legitimate_button =
(* création du rdbg_mv_hook et de tout ce qu'il faut autour *)
init_rdbg_hook ();
@@ -200,8 +209,8 @@ let custom_daemon p gtext vbox step_button round_button legitimate_button =
(* Necessary for salut (to perform a fake step that let sasa provide
the first set of enables) *)
- if args.salut_mode then goto_hook_exit ();
- goto_hook_call ();
+ if args.salut_mode then e := goto_hook_exit !e;
+ e := goto_hook_call !e;
blue_add gtext#buffer (str_of_sasa_event false !e);
d();
let nodes_enabled = rdbg_nodes_enabled !e in
@@ -222,7 +231,6 @@ let custom_daemon p gtext vbox step_button round_button legitimate_button =
blue gtext#buffer txt;
Hashtbl.replace daemongui_activate node activate
);
-
in
(* 1 case par noeud : activer/pas activer *)
@@ -291,8 +299,8 @@ let custom_daemon p gtext vbox step_button round_button legitimate_button =
ignore(pushbox#event#connect#button_press
~callback: (fun _ ->
update_rdbg_hook name true;
- goto_hook_exit ();
- goto_hook_call ();
+ e := goto_hook_exit !e;
+ e := goto_hook_call !e;
display_event gtext;
store !e.nb;
refresh ();
@@ -348,6 +356,7 @@ let custom_daemon p gtext vbox step_button round_button legitimate_button =
match !daemon_kind with
| Manual ->
show step_button; show checkbox_grid;
+ hide back_step_button;
hide legitimate_button;
(match !oracle_button_ref with Some b -> hide b | None -> ());
hide round_button; hide pushbox_grid; hide counter_grid;
@@ -362,14 +371,17 @@ let custom_daemon p gtext vbox step_button round_button legitimate_button =
| ManualCentral ->
hide legitimate_button;
(match !oracle_button_ref with Some b -> hide b | None -> ());
- hide step_button; hide round_button; hide checkbox_grid; hide counter_grid;
+ (* hide back_step_button; *)
+ hide step_button;
+ hide round_button; hide checkbox_grid; hide counter_grid;
show pushbox_grid;
let pushbox = Hashtbl.find pushbox_map node in
if enabled then show pushbox else hide pushbox;
pushbox#set_sensitive enabled
| Distributed | Synchronous | Central | LocCentral ->
(match !oracle_button_ref with Some b -> show b | None -> ());
- show step_button; show round_button; show counter_grid; show legitimate_button;
+ show back_step_button; show step_button; show round_button;
+ show counter_grid; show legitimate_button;
hide checkbox_grid; hide pushbox_grid;
in
let update_all_checkboxes () =
@@ -425,63 +437,57 @@ let custom_daemon p gtext vbox step_button round_button legitimate_button =
in
aux 0 [] nl
in
- let step () =
- let nodes_enabled = rdbg_nodes_enabled !e in
+ let set_daemongui_tbl e =
+ (* In automatic modes:
+ - looks who is enabled,
+ - chooses whom to activate, and
+ - sets the the tbl shared with the hook function
+
+ Should therefore be used at events where the enabled process info is available
+ *)
+ let nodes_enabled = rdbg_nodes_enabled e in
let nodes = List.filter (fun (_,b) -> b) nodes_enabled in
let nodes = get_higher_prioriry nodes in
- (* p ("==> gtkgui: CALL =" ^ (string_of_event !e)); *)
+ (* p ("==> gtkgui: CALL =" ^ (string_of_event e)); *)
(match !daemon_kind with
- | Distributed -> (
- let nodes = List.map (fun x -> [x]) nodes in
- let to_activate = Daemon.distributed nodes in
- Hashtbl.clear daemongui_activate;
- List.iter (fun n -> Hashtbl.replace daemongui_activate n true) to_activate;
- goto_hook_exit ();
- goto_hook_call ();
- )
- | Synchronous -> (
- Hashtbl.clear daemongui_activate;
- List.iter (fun n -> Hashtbl.replace daemongui_activate n true) nodes;
- goto_hook_exit ();
- goto_hook_call ();
- )
- | Central -> (
- let nodes = List.map (fun x -> [x]) nodes in
- let to_activate = Daemon.central nodes in
- Hashtbl.clear daemongui_activate;
- List.iter (fun n ->
- Printf.printf "Activating %s\n" n;
- Hashtbl.replace daemongui_activate n true) to_activate;
- goto_hook_exit ();
- goto_hook_call ();
- )
- | LocCentral -> (
- let get_neigbors x =
- let succ = snd (List.split (topology.succ x)) in
- let pred = topology.pred x in
- let res = List.fold_left (fun acc x -> if List.mem x acc then acc else x::acc) succ pred in
- (* p (Printf.sprintf "voisins(%s)=%s\n" x (String.concat "," res)); *)
- res
- in
- let nodes = List.map (fun x -> [x, get_neigbors x]) nodes in
- let to_activate = Daemon.locally_central nodes in
- Hashtbl.clear daemongui_activate;
- List.iter (fun n -> Hashtbl.replace daemongui_activate n true) to_activate;
- goto_hook_exit ();
- goto_hook_call ();
+ | Distributed -> (
+ let nodes = List.map (fun x -> [x]) nodes in
+ let to_activate = Daemon.distributed nodes in
+ Hashtbl.clear daemongui_activate;
+ List.iter (fun n -> Hashtbl.replace daemongui_activate n true) to_activate
+ )
+ | Synchronous -> (
+ Hashtbl.clear daemongui_activate;
+ List.iter (fun n -> Hashtbl.replace daemongui_activate n true) nodes
+ )
+ | Central -> (
+ let nodes = List.map (fun x -> [x]) nodes in
+ let to_activate = Daemon.central nodes in
+ Hashtbl.clear daemongui_activate;
+ List.iter (fun n ->
+ Printf.printf "Activating %s\n" n;
+ Hashtbl.replace daemongui_activate n true) to_activate
+ )
+ | LocCentral -> (
+ let get_neigbors x =
+ let succ = snd (List.split (topology.succ x)) in
+ let pred = topology.pred x in
+ let res = List.fold_left
+ (fun acc x -> if List.mem x acc then acc else x::acc) succ pred
+ in
+ (* p (Printf.sprintf "voisins(%s)=%s\n" x (String.concat "," res)); *)
+ res
+ in
+ let nodes = List.map (fun x -> [x, get_neigbors x]) nodes in
+ let to_activate = Daemon.locally_central nodes in
+ Hashtbl.clear daemongui_activate;
+ List.iter (fun n -> Hashtbl.replace daemongui_activate n true) to_activate
+ )
+ | ManualCentral -> () (* SNO; the step is done in pushbox callbacks *)
+ | Manual -> ()
)
- | ManualCentral -> () (* SNO; the step is done in pushbox callbacks *)
- | Manual ->
- goto_hook_exit ();
- goto_hook_call ();
- store !e.nb;
- );
- if not args.salut_mode && is_silent !e then
- (* go to Ltop so that the round number can be updated *)
- e := next_cond !e (fun e -> e.kind = Ltop);
- d ()
in
- step
+ set_daemongui_tbl
let prefix =
try
@@ -550,7 +556,6 @@ let main () =
let back_step_button = button ~use_mnemonic:true ~stock:`GO_BACK ~packing:bbox#add () in
set_tooltip back_step_button "Move BACKWARD to the previous STEP";
change_label back_step_button "Ste_p";
- ignore (back_step_button#connect#clicked ~callback:(button_cb true true bd));
let step_button = button ~use_mnemonic:true ~packing:bbox#add ~stock:`GO_FORWARD () in
let back_round_button =
@@ -564,19 +569,55 @@ let main () =
"Move FORWARD until a legitimate configuration is reached (silence by default)";
let image = GMisc.image ~file:(libui_prefix^"/chut_small.svg") () in
legitimate_button#set_image image#coerce;
-
- let ze_step =
+
+ let set_daemongui_tbl =
if custom_mode then
- custom_daemon p text_out w step_button round_button legitimate_button
+ custom_daemon p text_out w step_button back_step_button round_button legitimate_button
else
- s (* cf sasa-rdbg-cmds.ml *)
- in
- let step () =
- ze_step();
- d()
+ (fun _ -> ())
+ in
+ let a_gui_step e =
+ (* set the daemongui_tbl and step to the next event where the user
+ is asked to choose whom to activate *)
+ if custom_mode then (
+ set_daemongui_tbl e;
+ let e = goto_hook_exit e in
+ let e = goto_hook_call e in
+ if not args.salut_mode && is_silent e then
+ (* go to Ltop so that the round number can be updated *)
+ next_cond e (fun e -> e.kind = Ltop)
+ else
+ e
+ )
+ else
+ let e = sasa_step e in
+ store e.nb;
+ print_event e;
+ e
+ in
+ let back_step_gui () =
+ let lnext e =
+ if args.salut_mode then
+ let e = goto_top e in
+ set_daemongui_tbl e;
+ e
+ else
+ let e = goto_hook_call e in
+ set_daemongui_tbl e;
+ e
+ in
+ let ne = rev_cond_gen !e (fun ne -> ne.step = !e.step-1) lnext in
+ if ne.kind <> !e.kind || ne.name <> !e.name then
+ e:=next_cond ne (fun ne -> ne.kind = !e.kind || ne.name = !e.name)
+ else
+ e:=ne
in
+ ignore (back_step_button#connect#clicked
+ ~callback:(button_cb true false back_step_gui));
+
+ let step () = if not (is_silent !e) then (e := a_gui_step !e; d()) in
let rec legitimate_gui () =
- ze_step();
+ if is_silent !e then () else e := a_gui_step !e;
if is_legitimate !e || is_silent !e then () else (legitimate_gui ());
in
(* change_label legitimate_button "Silen_t"; *)
@@ -588,7 +629,7 @@ let main () =
if custom_mode then legitimate_button#misc#hide();
(* indeed, in the defaut mode (manual central), it should be hided *)
let rec next_round_gui rn =
- ze_step();
+ if is_silent !e then () else e:=a_gui_step !e;
if rn < !roundnb || is_silent !e then () else (next_round_gui rn);
in
@@ -602,8 +643,10 @@ let main () =
button_cb true true (fun () ->
if custom_mode then (
next_round_gui !roundnb;
- if custom_mode && !e.name <> "mv_hook" && !e.kind <> Call then
- goto_hook_call ()
+ if custom_mode && !e.name <> "mv_hook" && !e.kind <> Call
+ && not (is_silent !e)
+ then
+ e:= goto_hook_call !e
)
else
nr ()
@@ -612,7 +655,7 @@ let main () =
set_tooltip back_round_button "Move BACKWARD to the previous ROUND";
change_label back_round_button "Roun_d";
ignore (back_round_button#connect#clicked
- ~callback:(button_cb true true (fun () -> pr();pr(); goto_hook_call ())));
+ ~callback:(button_cb true true (fun () -> pr();pr(); e:=goto_hook_call !e)));
let graph () =
@@ -636,7 +679,7 @@ let main () =
let oracle_button =
make_button `OK "_Oracle" "Move FORWARD until an oracle is violated"
(button_cb_string
- (fun () -> let str = viol_string () in goto_hook_call (); d(); store !e.nb; str))
+ (fun () -> let str = viol_string () in e:=goto_hook_call !e; d(); store !e.nb; str))
in
oracle_button#misc#hide(); (* indeed, in the defaut mode (manual central), it should be hided *)
oracle_button_ref := Some oracle_button
@@ -653,8 +696,8 @@ let main () =
(* in this mode, the hook plays first to provide fake values to sasa
but the hook does not need input at this first step
*)
- goto_hook_exit ();
- goto_hook_call ();
+ e:=goto_hook_exit !e;
+ e:=goto_hook_call !e;
d()))
in
let _ = make_button `REFRESH "_New Seed" "Restart from the beginning using a New Seed"
@@ -670,8 +713,8 @@ let main () =
(* in this mode, the hook plays first to provide fake values to sasa
but the hook does not need input at this first step
*)
- goto_hook_exit ();
- goto_hook_call ();
+ e:=goto_hook_exit !e;
+ e:=goto_hook_call !e;
d()))
in
let _ = make_button `MEDIA_PLAY "_Sim2chro" "Launch sim2chro on the generated data (so far)"
diff --git a/tools/rdbg4sasa/sasa-rdbg-cmds.ml b/tools/rdbg4sasa/sasa-rdbg-cmds.ml
index d7859a2b..627fb956 100644
--- a/tools/rdbg4sasa/sasa-rdbg-cmds.ml
+++ b/tools/rdbg4sasa/sasa-rdbg-cmds.ml
@@ -8,13 +8,24 @@ open RdbgMain
open Sasacore.Topology;;
#use "dot4sasa.ml";;
+
+
+let is_silent e =
+ match List.assoc_opt "silent" e.data with
+ | Some B b -> b
+ | _ -> failwith "The silent value is not available in this event"
+
+let is_legitimate e =
+ match List.assoc_opt "legitimate" e.data with
+ | Some B b -> b
+ | _ -> failwith ("legitimate not available at this event: "^(string_of_event e))
+
(**********************************************************************)
(** Computing rounds *)
-
let roundnb = ref (-666)
let mask = ref [] (* nodes we look the activation of *) (* XXX use an array! *)
-let roundtbl = Hashtbl.create 10;;
+let roundtbl = Hashtbl.create 10;; (* maps event nb to round + round nb *)
(* let _ = Hashtbl.add roundtbl 1 (1,true);; *)
let verbose = ref false
@@ -47,12 +58,14 @@ let enabled pl = (* returns the enabled processes *)
(* called at each event via the time-travel hook *)
let (round : RdbgEvent.t -> bool) = fun e ->
match Hashtbl.find_opt roundtbl e.nb with
- | Some (croundnb, round) ->
+ | Some (croundnb, round, cmask) ->
(* Printf.printf "round tabulated at e.nb %d: croundnb=%d round = %b\n%!" *)
(* e.nb croundnb round; *)
roundnb := croundnb;
+ mask := cmask;
round
| None ->
+ if !mask = [] && is_silent e then false else
let round =
( (* we check if a round occurs when activated processes are available *)
if args.salut_mode then
@@ -91,7 +104,7 @@ let (round : RdbgEvent.t -> bool) = fun e ->
res
in
if round then incr roundnb;
- Hashtbl.add roundtbl e.nb (!roundnb, round);
+ Hashtbl.add roundtbl e.nb (!roundnb, round, !mask);
(* Printf.printf "round computed at e.nb %d: croundnb=%d round = %b\n%!"
e.nb !roundnb round; *)
round
@@ -99,7 +112,7 @@ let (round : RdbgEvent.t -> bool) = fun e ->
let update_round_nb e =
match Hashtbl.find_opt roundtbl e.nb with
| None -> ()
- | Some (n,_) -> roundnb := n
+ | Some (n,_, m) -> roundnb := n; mask := m
(* go to next round *)
let next_round e =
@@ -108,8 +121,8 @@ let next_round e =
(**********************************************************************)
(* redefine (more meaningful) step and back-step for sasa *)
-let sasa_step e = next_cond e (fun ne -> ne.kind = e.kind)
-let sasa_bstep e = rev_cond e (fun ne -> ne.kind = e.kind)
+let sasa_step e = next_cond e (fun ne -> ne.kind = e.kind && ne.name = e.name)
+let sasa_bstep e = rev_cond e (fun ne -> ne.kind = e.kind && ne.name = e.name)
let s () = e:=sasa_step !e ; emacs_udate !e; store !e.nb;pe()
let b () = e:=sasa_bstep !e ; emacs_udate !e; store !e.nb;pe()
@@ -168,6 +181,33 @@ let r () =
(* if the first event is not a round, add it as a check_point *)
if !ckpt_list = [] then ckpt_list := [!e];;
+(**********************************************************************)
+(* Move forward until silence *)
+
+let goto_silence e = next_cond e is_silent
+let silence () = e:=goto_silence !e; !dot_view ();;
+
+let _ = add_doc_entry
+ "silence" "unit -> unit" "Move forward until is_silent returns true"
+ "sasa" "sasa-rdbg-cmds.ml";
+ add_doc_entry
+ "is_silent" "RdbgEvent.t -> bool"
+ "does the event correspond to a silent configuration? (i.e., no enable node)"
+ "sasa" "sasa-rdbg-cmds.ml";;
+
+
+let goto_legitimate e = next_cond e is_legitimate
+let legitimate () = e:=goto_legitimate !e; !dot_view ();;
+let _ =
+ add_doc_entry
+ "legitimate" "unit -> unit"
+ " Move forward until a legitimate configuration is reached (uses 'silence' by default)"
+ "sasa" "sasa-rdbg-cmds.ml";
+ add_doc_entry
+ "is_legitimate" "RdbgEvent.t -> bool"
+ "does the event correspond to a legitimate configuration?"
+ "sasa" "sasa-rdbg-cmds.ml";;
+
(**********************************************************************)
(* print_event tuning *)
@@ -279,42 +319,6 @@ let _ = add_doc_entry
"sasa" "sasa-rdbg-cmds.ml"
-(**********************************************************************)
-(* Move forward until silence *)
-
-let is_silent e =
- match List.assoc_opt "silent" e.data with
- | Some B b -> b
- | _ -> failwith "The silent value is not available in this event"
-
-let goto_silence e = next_cond e is_silent
-let silence () = e:=goto_silence !e; !dot_view ();;
-
-let _ = add_doc_entry
- "silence" "unit -> unit" "Move forward until is_silent returns true"
- "sasa" "sasa-rdbg-cmds.ml";
- add_doc_entry
- "is_silent" "RdbgEvent.t -> bool"
- "does the event correspond to a silent configuration? (i.e., no enable node)"
- "sasa" "sasa-rdbg-cmds.ml";;
-
-let is_legitimate e =
- match List.assoc_opt "legitimate" e.data with
- | Some B b -> b
- | _ -> failwith ("legitimate not available at this event: "^(string_of_event e))
-
-let goto_legitimate e = next_cond e is_legitimate
-let legitimate () = e:=goto_legitimate !e; !dot_view ();;
-let _ =
- add_doc_entry
- "legitimate" "unit -> unit"
- " Move forward until a legitimate configuration is reached (uses 'silence' by default)"
- "sasa" "sasa-rdbg-cmds.ml";
- add_doc_entry
- "is_legitimate" "RdbgEvent.t -> bool"
- "does the event correspond to a legitimate configuration?"
- "sasa" "sasa-rdbg-cmds.ml";;
-
(**********************************************************************)
(* Perform the checkpointing at rounds! *)
--
GitLab