From 353b46cf68bf7f96d8a8753526e908e63da21e52 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr>
Date: Thu, 27 May 2021 10:41:30 +0200
Subject: [PATCH] Update: more work on rdbgui4sasa
---
tools/rdbg4sasa/dot4sasa.ml | 2 +-
tools/rdbg4sasa/gtkgui.ml | 159 ++++++++++++++++++++----------------
2 files changed, 88 insertions(+), 73 deletions(-)
diff --git a/tools/rdbg4sasa/dot4sasa.ml b/tools/rdbg4sasa/dot4sasa.ml
index f8d40393..5d827d18 100644
--- a/tools/rdbg4sasa/dot4sasa.ml
+++ b/tools/rdbg4sasa/dot4sasa.ml
@@ -197,7 +197,7 @@ subgraph undir {\n\t edge [dir=none]\n%s} " trans_dir_str trans_undir_str
| _ -> ""
in
Printf.fprintf oc
- "digraph %s {\nlabel=\"%s \nRound %d Step %d%s\"\nnode [shape=record];\n%s\n%s\n}\n"
+ "digraph %s {\nlabel=\"%s \nRound %d / Step %d\n%s\"\nnode [shape=record];\n%s\n%s\n}\n"
"g" f rn e.step pot
nodes_decl trans_str;
flush oc;
diff --git a/tools/rdbg4sasa/gtkgui.ml b/tools/rdbg4sasa/gtkgui.ml
index 34c5ca5e..df2cccfb 100644
--- a/tools/rdbg4sasa/gtkgui.ml
+++ b/tools/rdbg4sasa/gtkgui.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 26/05/2021 (at 10:37) by Erwan Jahier> *)
+(* Time-stamp: <modified the 27/05/2021 (at 10:38) by Erwan Jahier> *)
#thread
#require "lablgtk3"
@@ -54,7 +54,12 @@ let rdbg_nodes_enabled e =
in
last::res
-
+(* The interesting event to start in not the first event *)
+let set_first_check_point e =
+ e.save_state e.nb;
+ RdbgStdLib.ckpt_list := [e]
+
+
type daemon_kind = Distributed | Synchronous | Central | LocCentral | ManualCentral | Manual
let daemon_kind = ref ManualCentral
@@ -110,15 +115,17 @@ let green = write "green_foreground"
let blue_add = write_add "blue_foreground"
let black_add = write_add "black_foreground"
let red_add = write_add "red_foreground"
-(**********************************************************************************)
-(* *)
-let goto_hook_call b =
- e := next_cond !e (fun e -> e.name = "mv_hook" && e.kind = Call);
+let display_event b =
blue_add b#buffer "----------------------------------------";
blue_add b#buffer "----------------------------------------\n";
blue_add b#buffer (str_of_sasa_event false !e)
+(**********************************************************************************)
+
+(* *)
+let goto_hook_call () =
+ e := next_cond !e (fun e -> e.name = "mv_hook" && e.kind = Call)
let goto_hook_exit () =
e := next_cond !e (fun e -> e.name = "mv_hook" && e.kind = Exit)
@@ -196,11 +203,11 @@ let custom_daemon p gtext vbox step_button round_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 gtext;
- d()
- );
+ if args.salut_mode then goto_hook_exit ();
+ goto_hook_call ();
+ blue_add gtext#buffer (str_of_sasa_event false !e);
+ set_first_check_point !e;
+ d();
let nodes_enabled = rdbg_nodes_enabled !e in
(** Met à jour le hook pour node quand le bouton ou une checkbox correspondant est activé *)
@@ -291,7 +298,8 @@ let custom_daemon p gtext vbox step_button round_button =
~callback: (fun _ ->
update_rdbg_hook name true;
goto_hook_exit ();
- goto_hook_call gtext;
+ goto_hook_call ();
+ display_event gtext;
refresh ();
false));
Hashtbl.add pushbox_map name pushbox
@@ -429,14 +437,14 @@ let custom_daemon p gtext vbox step_button round_button =
Hashtbl.clear daemongui_activate;
List.iter (fun n -> Hashtbl.replace daemongui_activate n true) to_activate;
goto_hook_exit ();
- goto_hook_call gtext;
+ goto_hook_call ();
d ()
)
| Synchronous -> (
Hashtbl.clear daemongui_activate;
List.iter (fun n -> Hashtbl.replace daemongui_activate n true) nodes;
goto_hook_exit ();
- goto_hook_call gtext;
+ goto_hook_call ();
d ()
)
| Central -> (
@@ -447,7 +455,7 @@ let custom_daemon p gtext vbox step_button round_button =
Printf.printf "Activating %s\n" n;
Hashtbl.replace daemongui_activate n true) to_activate;
goto_hook_exit ();
- goto_hook_call gtext;
+ goto_hook_call ();
d ()
)
| LocCentral -> (
@@ -463,13 +471,13 @@ let custom_daemon p gtext vbox step_button round_button =
Hashtbl.clear daemongui_activate;
List.iter (fun n -> Hashtbl.replace daemongui_activate n true) to_activate;
goto_hook_exit ();
- goto_hook_call gtext;
+ goto_hook_call ();
d ()
)
| ManualCentral -> () (* SNO; the step is done in pushbox callbacks *)
| Manual ->
goto_hook_exit ();
- goto_hook_call gtext;
+ goto_hook_call ();
d ()
in
step
@@ -493,20 +501,20 @@ 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 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 *)
@@ -519,25 +527,28 @@ let main () =
button#set_image icon;
refresh ()
in
- let button_cb cmd () =
+ let button_cb display_event_flag cmd () =
blue text_out#buffer "From ";
let txt = Printf.sprintf "\n%s%!" (str_of_sasa_event false !e) in
(* text_out#buffer#set_text txt; *)
blue_add text_out#buffer txt;
cmd ();
+ if display_event_flag then display_event text_out;
refresh ()
in
let button_cb_string cmd () =
let txt = Printf.sprintf "\n%s" (cmd ()) in
(* text_out#buffer#set_text txt; *)
- blue_add text_out#buffer txt;
+ blue text_out#buffer txt;
+ let txt = Printf.sprintf "\n%s%!" (str_of_sasa_event false !e) in
+ red_add text_out#buffer txt;
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";
- ignore (back_step_button#connect#clicked ~callback:(button_cb bd));
+ ignore (back_step_button#connect#clicked ~callback:(button_cb true bd));
let step_button = button ~use_mnemonic:true ~packing:bbox#add ~stock:`GO_FORWARD () in
let back_round_button =
@@ -563,17 +574,18 @@ let main () =
set_tooltip step_button "Move FORWARD to the next STEP";
change_label step_button "_Step";
- ignore (step_button#connect#clicked ~callback:(button_cb step));
+ ignore (step_button#connect#clicked ~callback:(button_cb true step));
set_tooltip round_button "Move FORWARD to the next ROUND";
change_label round_button "_Round";
ignore (round_button#connect#clicked
- ~callback:(button_cb (fun () ->
- next_round_gui !roundnb;
- if !e.name <> "mv_hook" && !e.kind <> Call then goto_hook_call text_out)));
+ ~callback:(
+ button_cb true (fun () ->
+ next_round_gui !roundnb;
+ if !e.name <> "mv_hook" && !e.kind <> Call then goto_hook_call ())));
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 (fun () -> pr();pr(); goto_hook_call text_out)));
+ ~callback:(button_cb true (fun () -> pr();pr(); goto_hook_call ())));
let legitimate () =
let legitimate_button = button ~use_mnemonic:true ~packing:bbox#add () in
@@ -582,8 +594,8 @@ let main () =
let image = GMisc.image ~file:(libui_prefix^"/chut_small.svg") () in
legitimate_button#set_image image#coerce;
(* change_label legitimate_button "Silen_t"; *)
- ignore (legitimate_button#connect#clicked ~callback:(button_cb legitimate))
-
+ ignore (legitimate_button#connect#clicked ~callback:
+ (button_cb true (fun () -> legitimate(); goto_hook_call ())))
in
legitimate ();
@@ -592,7 +604,7 @@ let main () =
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 graph_view));
+ ignore (graph_button#connect#clicked ~callback:(button_cb false graph_view));
in
graph ();
@@ -608,59 +620,62 @@ let main () =
ignore (make_button `OK "_Oracle" "Move FORWARD until an oracle is violated"
(* let image = GMisc.image ~file:"../rdbg-utils/oracle_small.jpg" () in *)
(* viol_button#set_image image#coerce; *)
- (button_cb_string viol_string))
+ (button_cb_string
+ (fun () -> let str = viol_string () in goto_hook_call (); d();str)))
);
- let _ = make_button `UNDO "_Undo" "Undo the last move" (button_cb (fun ()->u();d())) in
+ let _ = make_button `UNDO "_Undo" "Undo the last move" (button_cb true (fun ()->u();d())) in
let _ = make_button `REFRESH "Restar_t" "Restart from the beginning"
- (button_cb
- (fun ()->
- let seed = Seed.get dotfile in
- Seed.set seed;
- p (Printf.sprintf "Restarting using the seed %d" seed);
- r();
- if args.salut_mode then
- (* in this mode, the hook plays first to provide fake values to sasa
+ (button_cb true
+ (fun ()->
+ let seed = Seed.get dotfile in
+ Seed.set seed;
+ p (Printf.sprintf "Restarting using the seed %d" seed);
+ r();
+ 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
- *)
- goto_hook_exit ();
- goto_hook_call text_out;
- d()))
+ *)
+ goto_hook_exit ();
+ goto_hook_call ();
+ set_first_check_point !e;
+ d()))
in
let _ = make_button `REFRESH "_New Seed" "Restart from the beginning using a New Seed"
- (button_cb
- (fun ()->
- Seed.reset();
- Seed.replay_seed := false;
- let seed = Seed.get dotfile in
- Seed.set (seed);
- p (Printf.sprintf "Restarting using the seed %d" seed);
- r();
- if args.salut_mode then
- (* in this mode, the hook plays first to provide fake values to sasa
+ (button_cb true
+ (fun ()->
+ Seed.reset();
+ Seed.replay_seed := false;
+ let seed = Seed.get dotfile in
+ Seed.set (seed);
+ p (Printf.sprintf "Restarting using the seed %d" seed);
+ r();
+ 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
- *)
- goto_hook_exit ();
- goto_hook_call text_out;
- d()))
+ *)
+ goto_hook_exit ();
+ goto_hook_call ();
+ set_first_check_point !e;
+ d()))
in
let _ = make_button `MEDIA_PLAY "_Sim2chro" "Launch sim2chro on the generated data (so far)"
- (button_cb sim2chro)
+ (button_cb false sim2chro)
in
let _ = make_button `MEDIA_PLAY "_Gnuplot" "Launch gnuplot-rif on the generated data (so far)"
- (button_cb gnuplot)
+ (button_cb 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;
@@ -680,7 +695,7 @@ let main () =
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
@@ -693,14 +708,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
@@ -746,9 +761,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);
--
GitLab