From 00fd74dbfcb51409553d170e1bb29939c414a07c Mon Sep 17 00:00:00 2001
From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr>
Date: Sun, 8 Jan 2023 16:50:53 +0100
Subject: [PATCH] fix: various fixes and improvements in rdbgui4sasa
---
test/dijkstra-ring/my-rdbg-tuning.ml | 5 -
tools/rdbg4sasa/gtkgui.ml | 702 +++++++++++++++------------
tools/rdbg4sasa/sasa-rdbg-cmds.ml | 29 +-
3 files changed, 412 insertions(+), 324 deletions(-)
delete mode 100644 test/dijkstra-ring/my-rdbg-tuning.ml
diff --git a/test/dijkstra-ring/my-rdbg-tuning.ml b/test/dijkstra-ring/my-rdbg-tuning.ml
deleted file mode 100644
index 2839202f..00000000
--- a/test/dijkstra-ring/my-rdbg-tuning.ml
+++ /dev/null
@@ -1,5 +0,0 @@
- (* *)
-#use "rdbg-cmds.ml";;
-#use "sasa-rdbg-cmds.ml";;
-
-
diff --git a/tools/rdbg4sasa/gtkgui.ml b/tools/rdbg4sasa/gtkgui.ml
index 8cffd03a..d5079d04 100644
--- a/tools/rdbg4sasa/gtkgui.ml
+++ b/tools/rdbg4sasa/gtkgui.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 04/01/2023 (at 11:56) by Erwan Jahier> *)
+(* Time-stamp: <modified the 08/01/2023 (at 16:29) by Erwan Jahier> *)
#thread
#require "lablgtk3"
@@ -52,10 +52,48 @@ let rdbg_nodes_enabled e =
in
last::res
+(**********************************************************************************)
type daemon_kind =
Distributed | Synchronous | Central | LocCentral | ManualCentral | Manual
let daemon_kind = ref ManualCentral
+type daemon_mode = Internal (* sasa with internal daemon *) | GuiAuto | GuiManual
+(* Possible way of using rdbgui4sasa w.r.t. daemon modes:
+|-------+----------+---------+-----------|
+| | Internal | GuiAuto | GuiManual |
+|-------+----------+---------+-----------|
+| sasa | yes | yes | yes |
+| salut | | yes | yes |
+|-------+----------+---------+-----------|
+*)
+
+let daemon_mode () =
+ if not custom_mode then Internal else
+ match !daemon_kind with
+ | Distributed | Synchronous | Central | LocCentral -> GuiAuto
+ | ManualCentral | Manual -> GuiManual
+
+let gui_mode = custom_mode (* a better name? *)
+
+let check_point_event e =
+ (* Depending on the way rdbgui4sasa is used, some kinds of events
+ make more sense as checkpoint candidate. Moreover, it is better to have only
+ one checkpoint per step.
+ *)
+ match daemon_mode () with
+ | Internal -> e.kind = Ltop
+ (* | GuiAuto -> e.kind = Ltop *)
+ | GuiAuto -> e.kind = Call && e.name = "mv_hook"
+ | GuiManual -> e.kind = Call && e.name = "mv_hook"
+
+let _ = check_ref := fun e -> e.nb = 1 || (check_point_event e) && round e;;
+
+(* modify the one in rdbg-cmd.ml to inhibit it when the undo is
+ impossible: in manual modes, it would require to store all the
+ user manual inputs to replay the simulation from the last
+ checkpoint (because of the PRGs) *)
+let store i = if daemon_mode() = GuiManual then () else store i
+
let refresh_fun_tbl = Hashtbl.create 1
let _ = Hashtbl.add refresh_fun_tbl "update dot" d
let refresh () =
@@ -118,28 +156,23 @@ let display_event b =
blue_add b#buffer "----------------------------------------\n";
blue_add b#buffer (str_of_sasa_event false !e)
-(**********************************************************************************)
-let custom_mode_ref = ref custom_mode
(* *)
-let goto_hook_call e =
- if !custom_mode_ref then
+
+let goto_hook_call e =
+ if gui_mode then
next_cond e (fun e -> e.name = "mv_hook" && e.kind = Call)
else
e
let goto_hook_exit e =
- if !custom_mode_ref then
+ if gui_mode then
next_cond e (fun e -> e.name = "mv_hook" && e.kind = Exit)
else
e
-let goto_top e =
- if !custom_mode_ref then
- next_cond e (fun e -> e.kind = Ltop)
- else
- e
+let goto_top e = next_cond e (fun e -> e.kind = Ltop)
let init_rdbg_hook () =
let guidaemon sl =
@@ -190,18 +223,18 @@ let init_rdbg_hook () =
in
match !rdbg_mv_hook with
| None -> rdbg_mv_hook := Some guidaemon
- | _ -> () (* custom_mode_ref := false *)
+ | _ -> ()
let set_tooltip b = b#misc#set_tooltip_text
let start () =
- if !custom_mode_ref then init_rdbg_hook ();
+ if gui_mode then init_rdbg_hook ();
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:=next_cond_gen !e (fun e -> e.name="mv_hook" && e.kind=Exit) (fun e -> e.next());
- if !custom_mode_ref then
- e:=next_cond_gen !e (fun e -> e.name="mv_hook" && e.kind=Call) (fun e -> e.next())
+ if gui_mode then
+ e:=next_cond_gen !e check_point_event (fun e -> e.next())
else
(* internal daemon mode *)
e:=next_cond_gen !e (fun e -> e.kind=Ltop) (fun e -> e.next());
@@ -210,29 +243,100 @@ let start () =
!e.save_state !e.nb
let restart p _ =
- !e.RdbgEvent.reset();
Seed.replay_seed := true;
let seed = Seed.get dotfile in
Seed.set seed;
p (Printf.sprintf "Restarting using the seed %d" seed);
+ !e.RdbgEvent.reset(); (* should be done after the see reset! *)
Round.reinit();
e:=RdbgStdLib.run ~call_hooks:true ();
start ();
d()
+let counter_map = Hashtbl.create 0
-let custom_daemon p gtext vbox step_button back_step_button round_button
- legitimate_button undo_button =
-
+let update_daemongui_tbl e =
+ (* In rdbgui automatic modes (ie, not in Manual nor CentralManual
+ nor internal sasa daemons):
+ - looks who is enabled,
+ - chooses whom to activate, and
+ - sets the tbl shared with the hook function
+
+ Should therefore be used at events where the enabled process info is available
+
+ nb: do side-effects via PRGs via Daemons
+ *)
+ assert (gui_mode);
+ let rec get_higher_priority nl =
+ let prio n =
+ let counter = try Hashtbl.find counter_map n with Not_found -> assert false in
+ counter#get
+ in
+ let rec aux p acc = function
+ | [] -> acc
+ | (n, false)::t -> aux p acc t
+ | (n, true)::t ->
+ let pn = prio n in
+ if p > pn then aux p acc t else
+ if p = pn then aux p (n::acc) t else
+ aux pn [n] t
+ in
+ aux 0 [] nl
+ in
+ let nodes_enabled = rdbg_nodes_enabled e in
+ let nodes = List.filter (fun (_,b) -> b) nodes_enabled in
+ let nodes = get_higher_priority nodes in
+ (* 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 (* PRGs inside! *)
+ 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 pred = snd (List.split (topology.pred x)) in
+ let succ = topology.succ 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 -> ()
+ )
+
+(* redraws the gui buttons a each move, to show only buttons related to enabled nodes *)
+let draw_manual_daemons_buttons p gtext vbox step_button back_step_button round_button
+ legitimate_button undo_button =
let daemon_box = GPack.hbox ~packing:vbox#add () ~homogeneous:true ~height:15 in
- let dk_dd = GButton.radio_button ~active:(!daemon_kind=Distributed)
- ~label:"Distributed" ~packing:daemon_box#add ()
+ let dk_cd = GButton.radio_button ~active:(!daemon_kind=Central)
+ ~label:"Central" ~packing:daemon_box#add ()
in
let make_but act lbl = GButton.radio_button ~active:act ~label:lbl
- ~group:dk_dd#group ~packing:daemon_box#add ()
+ ~group:dk_cd#group ~packing:daemon_box#add ()
in
- let dk_cd = make_but (!daemon_kind=Central) "Central" in
let dk_lcd = make_but (!daemon_kind=LocCentral) "Locally Central" in
+ let dk_dd = make_but (!daemon_kind=Distributed) "Distributed" in
let dk_sd = make_but (!daemon_kind=Synchronous) "Synchronous" in
let dk_manual = make_but (!daemon_kind=Manual) "Manual" in
let dk_manual_central = make_but (!daemon_kind=ManualCentral) "Manual Central" in
@@ -246,25 +350,25 @@ let custom_daemon p gtext vbox step_button back_step_button round_button
blue_add gtext#buffer (str_of_sasa_event false !e);
d();
let nodes_enabled = rdbg_nodes_enabled !e in
-
+ let nodes = fst (List.split nodes_enabled) in
let update_rdbg_hook node activate =
(match !daemon_kind with
| Distributed | Synchronous | Central | LocCentral ->
- assert false (* SNO *)
+ assert false (* SNO *)
| ManualCentral -> (
- let txt = Printf.sprintf "ManualCentral step: %s\n\n%s"
- node (str_of_sasa_event false !e) in
- (* gtext#buffer#set_text txt; *)
- blue gtext#buffer txt;
- Hashtbl.filter_map_inplace (fun n _prev_status -> Some (n = node)) daemongui_activate;
- )
+ let txt = Printf.sprintf "ManualCentral step: %s\n\n%s"
+ node (str_of_sasa_event false !e) in
+ (* gtext#buffer#set_text txt; *)
+ blue gtext#buffer txt;
+ List.iter (fun n -> Hashtbl.add daemongui_activate n (n = node)) nodes;
+ (* Hashtbl.filter_map_inplace (fun n _prev_status -> Some (n = node)) daemongui_activate; *)
+ )
| Manual ->
let txt = Printf.sprintf "Set %s to %b\n" node activate in
- blue_add gtext#buffer txt;
- Hashtbl.replace daemongui_activate node activate
+ blue_add gtext#buffer txt;
+ Hashtbl.replace daemongui_activate node activate
);
in
-
(* 1 case par noeud : activer/pas activer *)
(* NB : lablgtk3 ne propose pas le FlowBox (pourtant dispo dans GTK >= 3.12) *)
let n = List.length nodes_enabled in
@@ -275,13 +379,12 @@ let custom_daemon p gtext vbox step_button back_step_button round_button
let i = ref 0 in
let checkbox_grid = GPack.vbox ~packing:vbox#add () in
let checkbox_scrolled_grid = GBin.scrolled_window ~border_width:10 ~hpolicy:`AUTOMATIC
- ~vpolicy:`AUTOMATIC
- ~height:300
- ~shadow_type:`OUT ~packing:checkbox_grid#add ()
+ ~vpolicy:`AUTOMATIC
+ ~height:300
+ ~shadow_type:`OUT ~packing:checkbox_grid#add ()
in
let checkbox_scrolled_grid_box = GPack.vbox ~packing:checkbox_scrolled_grid#add () in
let checkbox_line = GPack.hbox ~packing:checkbox_scrolled_grid_box#add () in
-
let checkbox_line_ref = ref checkbox_line in
let checkbox_map = Hashtbl.create n in
List.iter (fun (name, enabled) ->
@@ -306,9 +409,9 @@ let custom_daemon p gtext vbox step_button back_step_button round_button
(* Des boutons pour le mode Manuel Central *)
let pushbox_grid = GPack.vbox ~packing:vbox#add () ~homogeneous:true in
let pushbox_scrolled_grid = GBin.scrolled_window ~border_width:10 ~hpolicy:`AUTOMATIC
- ~vpolicy:`AUTOMATIC
- ~height:300
- ~shadow_type:`OUT ~packing:pushbox_grid#add ()
+ ~vpolicy:`AUTOMATIC
+ ~height:300
+ ~shadow_type:`OUT ~packing:pushbox_grid#add ()
in
let pushbox_scrolled_grid_box =
GPack.vbox ~homogeneous:true ~packing:pushbox_scrolled_grid#add ()
@@ -330,13 +433,13 @@ let custom_daemon p gtext vbox step_button back_step_button round_button
(* Quand on appuie, met à jour le rdbg_mv_hook *)
ignore(pushbox#event#connect#button_press
~callback: (fun _ ->
- update_rdbg_hook name true;
- e := goto_hook_exit !e;
- e := goto_hook_call !e;
- display_event gtext;
- store !e.nb;
- refresh ();
- false));
+ update_rdbg_hook name true;
+ e := goto_hook_exit !e;
+ e := goto_hook_call !e;
+ display_event gtext;
+ store !e.nb;
+ refresh ();
+ false));
Hashtbl.add pushbox_map name pushbox
)
nodes_enabled;
@@ -344,13 +447,12 @@ let custom_daemon p gtext vbox step_button back_step_button round_button
(* Des compteurs pour les modes automatiques *)
let counter_grid = GPack.vbox ~packing:vbox#add () in
let counter_scrolled_grid = GBin.scrolled_window ~border_width:10 ~hpolicy:`AUTOMATIC
- ~vpolicy:`AUTOMATIC ~height:400
- ~shadow_type:`OUT ~packing:counter_grid#add ()
+ ~vpolicy:`AUTOMATIC ~height:400
+ ~shadow_type:`OUT ~packing:counter_grid#add ()
in
let counter_scrolled_grid_box = GPack.vbox ~packing:counter_scrolled_grid#add () in
let counter_line = GPack.hbox ~packing:counter_scrolled_grid_box#add () in
let counter_line_ref = ref counter_line in
- let counter_map = Hashtbl.create n in
i := 0;
List.iter (fun (name, enabled) ->
incr i;
@@ -385,48 +487,43 @@ let custom_daemon p gtext vbox step_button back_step_button round_button
Hashtbl.add counter_map name counter
)
nodes_enabled;
-
let hide b = b#misc#hide() in
let show b = b#misc#show() in
let update_checkbox node enabled =
match !daemon_kind with
| Manual ->
- show step_button; show checkbox_grid;
- hide back_step_button;
- hide legitimate_button;
- hide undo_button;
- (match !oracle_button_ref with Some b -> hide b | None -> ());
- hide round_button; hide pushbox_grid; hide counter_grid;
- let checkbox = try Hashtbl.find checkbox_map node with Not_found -> assert false in
- if enabled then
- show checkbox
- else (
- checkbox#set_active false; (* on decoche *)
- hide checkbox
- );
- checkbox#set_sensitive enabled
+ show step_button; show checkbox_grid;
+ hide back_step_button;
+ hide legitimate_button;
+ hide undo_button;
+ (match !oracle_button_ref with Some b -> hide b | None -> ());
+ hide round_button; hide pushbox_grid; hide counter_grid;
+ let checkbox = try Hashtbl.find checkbox_map node with Not_found -> assert false in
+ if enabled then
+ show checkbox
+ else (
+ checkbox#set_active false; (* on decoche *)
+ hide checkbox
+ );
+ checkbox#set_sensitive enabled
| ManualCentral ->
- hide undo_button;
- hide legitimate_button;
- (match !oracle_button_ref with Some b -> hide b | None -> ());
- hide back_step_button; (* requires to store all the inputs from the last ckpt! *)
- hide step_button;
- hide round_button; hide checkbox_grid; hide counter_grid;
- show pushbox_grid;
- let pushbox = try Hashtbl.find pushbox_map node with Not_found -> assert false in
- if enabled then show pushbox else hide pushbox;
- pushbox#set_sensitive enabled
-
+ hide undo_button;
+ hide legitimate_button;
+ (match !oracle_button_ref with Some b -> hide b | None -> ());
+ hide back_step_button; (* requires to store all the inputs from the last ckpt! *)
+ hide step_button;
+ hide round_button; hide checkbox_grid; hide counter_grid;
+ show pushbox_grid;
+ let pushbox = try Hashtbl.find pushbox_map node with Not_found -> assert false in
+ if enabled then show pushbox else hide pushbox;
+ pushbox#set_sensitive enabled
+
| Synchronous | Distributed | Central | LocCentral ->
- if !daemon_kind = Synchronous then (
- show undo_button; hide counter_grid
- ) else (
- hide undo_button; show counter_grid
- );
- (match !oracle_button_ref with Some b -> show b | None -> ());
- show back_step_button; show step_button; show round_button;
- if not args.salut_mode then show legitimate_button; (* for the time being *)
- hide checkbox_grid; hide pushbox_grid;
+ show undo_button; show counter_grid;
+ (match !oracle_button_ref with Some b -> show b | None -> ());
+ show back_step_button; show step_button; show round_button;
+ if not args.salut_mode then show legitimate_button; (* for the time being *)
+ hide checkbox_grid; hide pushbox_grid;
in
let update_all_checkboxes () =
(* only display the buttons of enabled nodes (for the manual daemon) *)
@@ -434,7 +531,6 @@ let custom_daemon p gtext vbox step_button back_step_button round_button
List.iter (fun (name, enabled) -> update_checkbox name enabled) nodes_enabled
in
Hashtbl.add refresh_fun_tbl "" update_all_checkboxes;
-
let set_dd_mode () =
black gtext#buffer"==> Switch to a distributed daemon\n";
daemon_kind := Distributed; refresh () in
@@ -461,74 +557,9 @@ let custom_daemon p gtext vbox step_button back_step_button round_button
ignore(dk_manual_central#connect#clicked ~callback:set_manual_central_mode);
(* Affichage d'informations *)
(* gtext#buffer#set_text !gtext_content; *)
-
- let rec get_higher_priority nl =
- let prio n =
- let counter = try Hashtbl.find counter_map n with Not_found -> assert false in
- counter#get
- in
- let rec aux p acc = function
- | [] -> acc
- | (n, false)::t -> aux p acc t
- | (n, true)::t ->
- let pn = prio n in
- if p > pn then aux p acc t else
- if p = pn then aux p (n::acc) t else
- aux pn [n] t
- in
- aux 0 [] nl
- 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_priority nodes in
- (* 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
- )
- | 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 pred = snd (List.split (topology.pred x)) in
- let succ = topology.succ 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 -> ()
- )
- in
- set_daemongui_tbl
+ (* update_daemongui_tbl *)
+ ()
+(* End of draw_manual_daemons_buttons *)
let prefix =
try
@@ -549,26 +580,28 @@ let main () =
let _locale = GtkMain.Main.init () in
let _thread = GtkThread.start () in
let window = GWindow.window
- (* ~width:320 ~height:240 *)
- ~title:"A rdbg GUI for sasa"
- ~show:true ()
+ (* ~width:320 ~height:240 *)
+ ~title:"A rdbg GUI for sasa"
+ ~show:true ()
in
let w = GPack.vbox ~packing:window#add () ~homogeneous:false in
- let box = GPack.vbox ~packing: w#add () in
+ let box0 = GPack.vbox ~packing: w#add () in
+ let box = GPack.vbox ~packing: box0#add () in
let gbox = GPack.hbox ~packing: box#add () in
let gbox2 = GPack.hbox ~packing: box#add () in
let sw2 = GBin.scrolled_window ~border_width:10 ~shadow_type:`OUT ~height:250
- ~packing:box#add ()
+ ~packing:box#add ()
in
set_tooltip sw2 "This window displays commands outputs";
let text_out = GText.view ~wrap_mode:`CHAR ~height:250 ~editable:false
- ~packing: sw2#add () ~cursor_visible:true
+ ~packing: sw2#add () ~cursor_visible:true
in
let p str = black text_out#buffer str in
(* It should be better to rely on the gtk event handler *)
restart p ();
+ let bbox0 = GPack.hbox ~packing: box0#add () in
let bbox = GPack.hbox ~packing: box#add () in
let change_label button str =
@@ -596,23 +629,13 @@ let main () =
refresh ()
in
- 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";
-
- let step_button = button ~use_mnemonic:true ~packing:bbox#add ~stock:`GO_FORWARD () in
- let back_round_button =
- button ~packing:bbox#add ~stock:`MEDIA_PREVIOUS ~use_mnemonic:true ~label:"back round" ()
- in
- let round_button =
- button ~use_mnemonic:true ~stock:`MEDIA_FORWARD ~packing:bbox#add ~label:"round" ()
+ let make_button0 stock lbl msg cmd =
+ let butt = button ~use_mnemonic:true ~stock:stock ~packing:bbox0#add ~label:lbl () in
+ set_tooltip butt msg;
+ change_label butt lbl;
+ ignore (butt#connect#clicked ~callback:cmd);
+ butt
in
- let legitimate_button = button ~use_mnemonic:true ~packing:bbox#add () in
- set_tooltip legitimate_button
- "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 make_button stock lbl msg cmd =
let butt = button ~use_mnemonic:true ~stock:stock ~packing:bbox#add ~label:lbl () in
set_tooltip butt msg;
@@ -620,226 +643,285 @@ let main () =
ignore (butt#connect#clicked ~callback:cmd);
butt
in
- let undo_button = make_button `UNDO "_Undo" "Undo the last move"
- (button_cb true false (fun ()->u();d()))
+ (* Going backward requires special care here to remain
+ deterministic, because of all the PRGs! It concerns back_step,
+ back_round, and undo. *)
+ let goto_gui i =
+ if not gui_mode then ( u(); d() )
+ else
+ let lnext e =
+ if args.salut_mode then (
+ update_daemongui_tbl e;
+ let e = goto_hook_call e in
+ e
+ )
+ else (
+ update_daemongui_tbl e;
+ if e.kind = Ltop then e.restore_state e.nb;
+ let e = goto_hook_call e in
+ e
+ )
+ in
+ let ne =
+ if i < !e.nb then
+ rev_cond_gen !e (fun ne -> ne.nb = i) lnext (fun _ -> ())
+ else if i > !e.nb then
+ next_cond_gen !e (fun ne -> ne.nb = i) lnext
+ else
+ !e
+ in
+ e:=ne;
+ ignore (round !e);
+ d()
+ in
+ let undo_gui () =
+ let i =
+ match !redos with
+ | _::i::t -> redos := i::t; i
+ | i::[] -> i
+ | [] -> 1
+ in
+ goto_gui i
+ in
+ let back_round_button =
+ button ~packing:bbox0#add ~stock:`MEDIA_PREVIOUS ~use_mnemonic:true
+ ~label:"back round" ()
+ in
+ let back_step_button = button ~use_mnemonic:true ~stock:`GO_BACK ~packing:bbox0#add () in
+ set_tooltip back_step_button "Move BACKWARD to the previous STEP";
+ change_label back_step_button "Ste_p";
+
+ let undo_button = make_button0 `UNDO "_Undo" "Undo the last move"
+ (button_cb true false undo_gui)
+ in
+ let step_button = button ~use_mnemonic:true ~packing:bbox0#add ~stock:`GO_FORWARD () in
+ let round_button =
+ button ~use_mnemonic:true ~stock:`MEDIA_FORWARD ~packing:bbox0#add ~label:"round" ()
+ in
+ let legitimate_button =
+ button ~use_mnemonic:true ~stock:`GOTO_LAST ~packing:bbox0#add ()
in
+ set_tooltip legitimate_button
+ "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 set_daemongui_tbl =
- if !custom_mode_ref then
- custom_daemon p text_out w step_button back_step_button round_button
- legitimate_button undo_button
+ if gui_mode then draw_manual_daemons_buttons p text_out w step_button
+ back_step_button round_button legitimate_button undo_button;
+ let update_daemongui_tbl_and_redraw =
+ if gui_mode then update_daemongui_tbl
else
(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_ref then (
- set_daemongui_tbl e;
+ if gui_mode then (
+ update_daemongui_tbl_and_redraw e;
let e = goto_hook_exit e in
let e = goto_hook_call e in
e
)
- else
+ else (* internal daemon mode *)
let e = sasa_step e in
store e.nb;
print_event e;
e
in
- let rec next_round_gui_loop rn =
- if is_silent ~dflt:false !e then (
- if not args.salut_mode && !e.kind <> Ltop then
- (* go to Ltop so that the round number can be updated *)
- e := next_cond !e (fun e -> e.kind = Ltop);
+ let postambule () = (* necessary to get the round nb rigth! *)
+ if not args.salut_mode && not (check_point_event !e) then
+ e := next_cond !e check_point_event
+ in
+ let next_step_gui () =
+ if not (is_silent ~dflt:false !e)
+ (* ??? || (not args.salut_mode && !e.kind <> Ltop) *)
+ then (
+ e := a_gui_step !e;
+ d()
)
- else e:=a_gui_step !e;
- if (get_round !e) || is_silent ~dflt:false !e then () else (next_round_gui_loop rn);
in
let next_round_gui () =
- if !custom_mode_ref then (
+ if gui_mode then (
+ let rec next_round_gui_loop rn =
+ if is_silent ~dflt:false !e then (postambule ())
+ else e := a_gui_step !e;
+ if (get_round !e) || is_silent ~dflt:false !e then () else (
+ next_round_gui_loop rn
+ );
+ in
next_round_gui_loop (get_round_nb !e);
if
- !custom_mode_ref && args.salut_mode && !e.name<>"mv_hook"
+ args.salut_mode && !e.name<>"mv_hook"
&& !e.kind<>Call && not (is_silent ~dflt:false !e)
then
e:= goto_hook_call !e
)
else ( (* internal daemon mode *)
- e := next_round !e
- );
- store !e.nb
+ e := next_cond_gen !e
+ (fun e -> e.kind = Ltop && (round e || is_legitimate e))
+ sasa_next
+ )
in
let back_step_gui () =
- if not !custom_mode_ref then (
+ if not gui_mode then ( (* internal daemon mode *)
e := back_step !e;
pe()
)
- else (
+ else (
if args.salut_mode then
let lnext e =
- set_daemongui_tbl e;
+ update_daemongui_tbl e; (* necessary to get the PRGs rigth during backward moves *)
let e = goto_hook_call e in
e
in
let ne =
rev_cond_gen !e
(fun ne ->
- if ne.step = !e.step-1 && ne.kind = !e.kind then true else (
- Printf.printf "%d: ne.step=%d (!e.step-1)=%d\n%!" ne.nb ne.step (!e.step-1);
- false
- )
+ if ne.step = !e.step-1 && ne.kind = !e.kind then true else (
+ Printf.printf "%d: ne.step=%d (!e.step-1)=%d\n%!" ne.nb ne.step (!e.step-1);
+ false
+ )
)
lnext (fun _ -> ())
in
e:=ne
else (* custom sasa mode *)
let lnext e =
- set_daemongui_tbl e;
+ update_daemongui_tbl e;
if e.kind = Ltop then
- (* Necessary for reproductibility because set_daemongui_tbl
- calls Random.int (via Daemon) which changes the PRGS! *)
+ (* Necessary for reproductibility because update_daemongui_tbl
+ calls Random.int (via Daemon) which changes the PRGS! *)
e.restore_state e.nb;
let e = goto_hook_call e in
e
in
let ne = rev_cond_gen !e
- (fun ne -> ne.step = !e.step-1 && ne.name = "mv_hook" && ne.kind=Call)
- lnext (fun _ -> ())
+ (fun ne -> ne.step = !e.step-1 && check_point_event ne)
+ lnext (fun _ -> ())
in
e:=ne
- );
- store !e.nb
+ )
in
let back_round_gui () =
- if not !custom_mode_ref then (
+ if not gui_mode then ( (* internal daemon mode *)
e:=goto_last_ckpt !e.nb
)
- else (
- let ne1 = goto_last_ckpt !e.nb in
- let ne2 = goto_last_ckpt ne1.nb in
- if ne1.nb = !e.nb then
- (* already at the first event. Do nothing *)
- ()
- else if ne1.nb = ne2.nb then (
- (* Still in the first round. Go at the beginning *)
- e:=ne1
- )
- else (
- (* From round n>1, go to round n-1 *)
- e:=ne2;
- if !e.kind <> Call && not args.salut_mode then
- (* only the first event is already a call*)
- e:=goto_hook_call !e
- )
- );
- store !e.nb;
+ else
+ (
+ let ne1 = goto_last_ckpt !e.nb in
+ let ne2 = if round !e then ne1 else goto_last_ckpt ne1.nb in
+ if ne1.nb = !e.nb then
+ (* already at the first event. Do nothing *)
+ ()
+ else if ne1.nb = ne2.nb then (
+ (* Still in the first round. Go at the beginning *)
+ e:=ne1
+ )
+ else (
+ (* From round n>1, go to round n-1 *)
+ e:=ne2;
+ if !e.kind <> Call && not args.salut_mode then
+ (* only the first event is already a call*)
+ e:=goto_hook_call !e
+ (* else if args.salut_mode then e:=??? *)
+ )
+ );
refresh ()
in
ignore (back_step_button#connect#clicked
- ~callback:(button_cb true false back_step_gui));
+ ~callback:(button_cb true true back_step_gui));
- let step () =
- if not (is_silent ~dflt:false !e) || (not args.salut_mode && !e.kind <> Ltop) then (
- e := a_gui_step !e;
- d()
- )
- in
let rec legitimate_gui () =
- if is_silent ~dflt:false !e then () else e := a_gui_step !e;
- if is_legitimate !e || is_silent ~dflt:false !e then (
- if not args.salut_mode && !e.kind <> Ltop then
- e := next_cond !e (fun e -> e.kind = Ltop);
+ if gui_mode then (
+ if is_silent ~dflt:false !e then () else e := a_gui_step !e;
+ if is_legitimate !e || is_silent ~dflt:false !e then (
+ postambule (); d()
+ )
+ else legitimate_gui ();
)
- else (legitimate_gui ());
+ else (* internal daemon mode *)
+ e:= next_cond !e (fun le -> is_legitimate le && le.kind=Ltop)
in
- (* change_label legitimate_button "Silen_t"; *)
+ change_label legitimate_button "_Legit";
ignore (legitimate_button#connect#clicked ~callback:
- (button_cb true true (fun () ->
- if !custom_mode_ref then legitimate_gui() else
- e:= next_cond !e (fun le -> is_legitimate le && le.kind=Ltop))
- )
- );
- if !custom_mode_ref then legitimate_button#misc#hide();
- (* indeed, in the defaut mode (manual central), it should be hided *)
+ (button_cb true true legitimate_gui)
+ );
+ if daemon_mode()=GuiManual then legitimate_button#misc#hide();
set_tooltip step_button "Move FORWARD to the next STEP";
change_label step_button "_Step";
- ignore (step_button#connect#clicked ~callback:(button_cb true true step));
+ ignore (step_button#connect#clicked ~callback:(button_cb true true next_step_gui));
set_tooltip round_button "Move FORWARD to the next ROUND";
change_label round_button "_Round";
- ignore (round_button#connect#clicked ~callback:(button_cb true true next_round_gui)
- );
+ ignore (round_button#connect#clicked ~callback:(button_cb true true next_round_gui));
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 back_round_gui));
-
- let graph () =
- let graph_button = button ~use_mnemonic:true ~packing:bbox#add () in
- set_tooltip graph_button "Visualize the Topology states: Green=Enabled ; Gold=Active";
- let image = GMisc.image ~file:(libui_prefix^"/graph_small.png") () in
- graph_button#set_image image#coerce;
- ignore (graph_button#connect#clicked ~callback:(button_cb false false graph_view));
-
- in
- graph ();
-
if args.oracles <> [] then (
let oracle_button =
make_button `OK "_Oracle" "Move FORWARD until an oracle is violated"
(button_cb_string
(fun () -> let str = viol_string () in
- e:=goto_hook_call !e; d(); store !e.nb; str))
+ 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
);
let _ = make_button `REFRESH "Restar_t" "Restart from the beginning"
- (button_cb true true (restart p))
+ (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 ()->
- !e.RdbgEvent.reset();
- Seed.reset(); Seed.replay_seed := false;
- let seed = Seed.get dotfile in
- change_sasa_seed seed;
- Seed.set (seed);
- 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
+ (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()))
+ *)
+ 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)"
- (button_cb false false sim2chro)
+ let graph () =
+ let graph_button = button ~use_mnemonic:true ~packing:bbox#add () in
+ set_tooltip graph_button "Visualize the Topology states: Green=Enabled ; Gold=Active";
+ let image = GMisc.image ~file:(libui_prefix^"/graph_small.png") () in
+ graph_button#set_image image#coerce;
+ ignore (graph_button#connect#clicked ~callback:(button_cb false false graph_view));
+
+ in
+ graph ();
+ let _ = make_button `MEDIA_PLAY "Sim2_chro" "Launch sim2chro on the generated data (so far)"
+ (button_cb false false sim2chro)
in
let _ = make_button `MEDIA_PLAY "_Gnuplot" "Launch gnuplot-rif on the generated data (so far)"
- (button_cb false false gnuplot)
+ (button_cb false false gnuplot)
in
let _ = make_button `INFO "_Info" "Get information about the current session"
- (button_cb_string info_string)
+ (button_cb_string info_string)
in
let _ = make_button `QUIT "_Quit" "Quit RDBGUI" (fun() -> p "bye"; Stdlib.exit 0) in
let sw1 = GBin.scrolled_window ~border_width:10 ~shadow_type:`IN ~height:130 ~width:50
- ~packing:w#add ()
+ ~packing:w#add ()
in
sw1#misc#set_tooltip_text "This window displays the rdbg.log file";
let text_in = GText.view ~wrap_mode:`CHAR ~height:250 ~editable:true ~width:50
- ~packing: sw1#add () ~cursor_visible:true
+ ~packing: sw1#add () ~cursor_visible:true
in
let rdbg_log = open_in "rdbg.log" in
create_tags text_in#buffer;
@@ -855,11 +937,11 @@ let main () =
read_rdbglog ()
in
let _ = Thread.create read_rdbglog () in
-
+
let dot_button = radio_button ~packing:gbox#add ~label:"dot" () in
let make_but active lbl = radio_button ~packing:gbox#add
- ~active:active ~group:dot_button#group ~label:lbl ()
+ ~active:active ~group:dot_button#group ~label:lbl ()
in
let fd_button = make_but false "fdp" in
let sf_button = make_but false "sfdp" in
@@ -872,14 +954,14 @@ let main () =
let connect button str cmd =
ignore (button#connect#clicked
~callback:(fun () -> p ((button#misc#tooltip_text)^"\n"^(help_string str));
- dot_view := cmd; !dot_view()))
+ dot_view := cmd; !dot_view()))
in
let have_parent () = (* is there a parent field in the state ? *)
List.exists (fun (v,_) -> Str.string_match (Str.regexp ".*_par.*") v 0) !e.data
in
if have_parent () then (
let make_but lbl = GButton.radio_button ~packing:gbox2#add
- ~group:dot_button#group ~label:lbl ()
+ ~group:dot_button#group ~label:lbl ()
in
let par_dot_button = make_but "dot*" in
let par_fd_button = make_but "fdp*" in
@@ -906,14 +988,14 @@ let main () =
connect par_pa_button "pa_par" pa_par;
connect par_os_button "os_par" os_par;
);
- set_tooltip dot_button "Use the dot engine to display the graph";
- set_tooltip fd_button "Use the fdp engine to display the graph";
- set_tooltip sf_button "Use the sfdp engine to display the graph";
- set_tooltip ne_button "Use the neato engine to display the graph";
- set_tooltip tw_button "Use the twopi engine to display the graph";
- set_tooltip ci_button "Use the circo engine to display the graph";
- set_tooltip pa_button "Use the patchwork engine to display the graph";
- set_tooltip os_button "Use the osage engine to display the graph";
+ set_tooltip dot_button "Use the dot engine to display the graph (cf https://graphviz.org/docs/layouts/)";
+ set_tooltip fd_button "Use the fdp engine to display the graph (cf https://graphviz.org/docs/layouts/)";
+ set_tooltip sf_button "Use the sfdp engine to display the graph (cf https://graphviz.org/docs/layouts/)";
+ set_tooltip ne_button "Use the neato engine to display the graph (cf https://graphviz.org/docs/layouts/)";
+ set_tooltip tw_button "Use the twopi engine to display the graph (cf https://graphviz.org/docs/layouts/)";
+ set_tooltip ci_button "Use the circo engine to display the graph (cf https://graphviz.org/docs/layouts/)";
+ set_tooltip pa_button "Use the patchwork engine to display the graph (cf https://graphviz.org/docs/layouts/)";
+ set_tooltip os_button "Use the osage engine to display the graph (cf https://graphviz.org/docs/layouts/)";
connect dot_button "d" dot;
connect fd_button "fd" fd;
@@ -925,9 +1007,9 @@ let main () =
connect os_button "os" os;
ignore (window#connect#destroy ~callback: (
- fun () ->
- quit (); (* quit rdbg, this will stop the readloop below *)
- Main.quit () (* terminate gtk *)
+ fun () ->
+ quit (); (* quit rdbg, this will stop the readloop below *)
+ Main.quit () (* terminate gtk *)
));
Seed.replay_seed := true;
ignore(Seed.get dotfile);
diff --git a/tools/rdbg4sasa/sasa-rdbg-cmds.ml b/tools/rdbg4sasa/sasa-rdbg-cmds.ml
index 1f356ba5..334523af 100644
--- a/tools/rdbg4sasa/sasa-rdbg-cmds.ml
+++ b/tools/rdbg4sasa/sasa-rdbg-cmds.ml
@@ -50,7 +50,14 @@ let enabled pl = (* returns the enabled processes *)
(* called at each event via the time-travel hook *)
let (round : RdbgEvent.t -> bool) =
fun e ->
- if e.kind=Exit && e.name = "sasa" then get_round e else false
+ let get_it =
+ if args.salut_mode then
+ e.kind=Call && e.name = "mv_hook"
+ else
+ true
+ (* e.kind=Exit && e.name = "sasa" *)
+ in
+ if get_it then get_round e else false
(**********************************************************************)
let d_par () = dot true (get_round_nb !e) p dotfile !e;;
@@ -145,12 +152,15 @@ It is the case for sasa and lutin at least.
let (string_to_string_list : string -> string list) =
fun str ->
- Str.split (Str.regexp "[ \t]+") str
+ Str.split (Str.regexp "[ \t]+") str
let (change_ocaml_plugin_seed: int -> RdbgPlugin.t -> RdbgPlugin.t) =
- fun seed rdbgplugin ->
- let new_sasa_call = Printf.sprintf "%s --seed %d" rdbgplugin.id seed in
- Sasa.SasaRun.make(Array.of_list (string_to_string_list new_sasa_call))
+ fun seed rdbgplugin ->
+ if args.salut_mode then ((* nothing to do here *) rdbgplugin) else
+ let new_sasa_call = Printf.sprintf "%s --seed %d" rdbgplugin.id seed in
+ Printf.printf "%s\n%!" new_sasa_call;
+ Sasa.SasaRun.make (Array.of_list (string_to_string_list new_sasa_call))
+
let (change_plugin_seed : int -> RdbgArg.reactive_program -> RdbgArg.reactive_program) =
fun seed plugin ->
@@ -318,11 +328,12 @@ let _ = add_doc_entry
"potential" "unit -> float option" "returns the current potential if available"
"sasa" "sasa-rdbg-cmds.ml"
-
-
(**********************************************************************)
-(* Perform the checkpointing at rounds! *)
-let _ = check_ref := fun e -> e.nb = 1 || round e;;
+(* overide the default checkpointing at rounds
+
+nb : this is overridden in gtkgui.ml
+*)
+let _ = check_ref := fun e -> e.nb = 1 || (e.kind=Exit && e.name="sasa" && round e);;
(**********************************************************************)
let _ =
--
GitLab