diff --git a/tools/rdbg4sasa/gtkgui.ml b/tools/rdbg4sasa/gtkgui.ml
index df2cccfb6084bc921d7ecd9c38628778cae416f1..28ab05ee13d1c2f4a6415d36acbf3f6047b71b6a 100644
--- a/tools/rdbg4sasa/gtkgui.ml
+++ b/tools/rdbg4sasa/gtkgui.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 27/05/2021 (at 10:38) by Erwan Jahier> *)
+(* Time-stamp: <modified the 27/05/2021 (at 17:23) by Erwan Jahier> *)
#thread
#require "lablgtk3"
@@ -20,10 +20,10 @@ let rdbg_nodes_info e: (string * string * bool) list =
let split_var (str, value) =
let v = match value with B v -> v | _ -> assert false in
let p, label =
- match String.split_on_char '_' str with
- | [] | [_] | [_;_] -> assert false
- | [_; x; y] -> x, y
- | [_; x; y; z] -> x^y,z
+ match args.salut_mode, String.split_on_char '_' str with
+ | _, [] | _, [_] | _, [_;_] -> assert false (* should not occur (naming conv) *)
+ | false, _::x::y -> x, String.concat "_" y
+ | true, _::x::y::z -> x^y, String.concat "_" z
| _ -> assert false
in
p, label,v
@@ -71,7 +71,6 @@ let refresh () =
(** Met en place le hook *)
let daemongui_activate = Hashtbl.create 1
-
let (fake_val_of_type : Data.t -> Data.v) = function
| Bool -> B false
| Int -> I (Random.int 10)
@@ -96,6 +95,7 @@ let create_tags (buffer:GText.buffer) =
()
let tags_created = ref false
+let oracle_button_ref = ref None
let write color b str =
if not !tags_created then (create_tags b; tags_created := true);
@@ -125,9 +125,11 @@ let display_event b =
(* *)
let goto_hook_call () =
- e := next_cond !e (fun e -> e.name = "mv_hook" && e.kind = Call)
+ if custom_mode then
+ e := next_cond !e (fun e -> e.name = "mv_hook" && e.kind = Call)
let goto_hook_exit () =
+ if custom_mode then
e := next_cond !e (fun e -> e.name = "mv_hook" && e.kind = Exit)
let init_rdbg_hook () =
@@ -156,9 +158,9 @@ let init_rdbg_hook () =
| None -> false
| Some x -> x
in
- let activate = match enabled with
+ let activate = match enabled with (* activate the Enabled actions! *)
| B true -> B to_activate
- | _ -> B false
+ | B false -> B false
in
(str, activate)
) sl
@@ -178,16 +180,16 @@ let init_rdbg_hook () =
let set_tooltip b = b#misc#set_tooltip_text
-let custom_daemon p gtext vbox step_button round_button =
+let custom_daemon p gtext vbox step_button round_button legitimate_button =
(* création du rdbg_mv_hook et de tout ce qu'il faut autour *)
init_rdbg_hook ();
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 ()
+ ~label:"Distributed" ~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_dd#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
@@ -214,19 +216,17 @@ let custom_daemon p gtext vbox step_button round_button =
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.iter
- (fun n status -> Hashtbl.replace daemongui_activate n (n = node && status))
- daemongui_activate;
- )
- | Manual ->
- let txt = Printf.sprintf "Manual step: \n\n%s" (str_of_sasa_event false !e) in
+ 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.replace daemongui_activate node activate
+ Hashtbl.filter_map_inplace (fun n status -> Some (n = node)) daemongui_activate;
+ )
+ | Manual ->
+ let txt = Printf.sprintf "Manual step: \n\n%s" (str_of_sasa_event false !e) in
+ blue gtext#buffer txt;
+ Hashtbl.replace daemongui_activate node activate
);
in
@@ -241,9 +241,9 @@ let custom_daemon p gtext vbox 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
@@ -272,9 +272,9 @@ let custom_daemon p gtext vbox 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 ()
@@ -296,12 +296,12 @@ let custom_daemon p gtext vbox 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;
- goto_hook_exit ();
- goto_hook_call ();
- display_event gtext;
- refresh ();
- false));
+ update_rdbg_hook name true;
+ goto_hook_exit ();
+ goto_hook_call ();
+ display_event gtext;
+ refresh ();
+ false));
Hashtbl.add pushbox_map name pushbox
)
nodes_enabled;
@@ -309,8 +309,8 @@ let custom_daemon p gtext vbox 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
@@ -352,25 +352,30 @@ let custom_daemon p gtext vbox step_button round_button =
let update_checkbox node enabled =
match !daemon_kind with
| Manual ->
- show step_button; show checkbox_grid;
- hide round_button; hide pushbox_grid; hide counter_grid;
- let checkbox = Hashtbl.find checkbox_map node 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 legitimate_button;
+ (match !oracle_button_ref with Some b -> hide b | None -> ());
+ hide round_button; hide pushbox_grid; hide counter_grid;
+ let checkbox = Hashtbl.find checkbox_map node in
+ if enabled then
+ show checkbox
+ else (
+ checkbox#set_active false; (* on decoche *)
+ hide checkbox
+ );
+ checkbox#set_sensitive enabled
| ManualCentral ->
- 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
+ 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;
+ 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 ->
- show step_button; show round_button; show counter_grid;
- hide checkbox_grid; hide pushbox_grid;
+ (match !oracle_button_ref with Some b -> show b | None -> ());
+ show step_button; show round_button; show counter_grid; show legitimate_button;
+ hide checkbox_grid; hide pushbox_grid;
in
let update_all_checkboxes () =
let nodes_enabled = rdbg_nodes_enabled !e in
@@ -418,10 +423,10 @@ let custom_daemon p gtext vbox step_button round_button =
| [] -> 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
+ 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
@@ -432,53 +437,53 @@ let custom_daemon p gtext vbox step_button round_button =
(* 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 ();
- d ()
- )
+ 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 ();
+ d ()
+ )
| Synchronous -> (
- Hashtbl.clear daemongui_activate;
- List.iter (fun n -> Hashtbl.replace daemongui_activate n true) nodes;
- goto_hook_exit ();
- goto_hook_call ();
- d ()
- )
+ Hashtbl.clear daemongui_activate;
+ List.iter (fun n -> Hashtbl.replace daemongui_activate n true) nodes;
+ goto_hook_exit ();
+ goto_hook_call ();
+ d ()
+ )
| 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 ();
- d ()
- )
+ 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 ();
+ d ()
+ )
| 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 ();
- d ()
- )
- | ManualCentral -> () (* SNO; the step is done in pushbox callbacks *)
- | Manual ->
+ 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 ();
d ()
+ )
+ | ManualCentral -> () (* SNO; the step is done in pushbox callbacks *)
+ | Manual ->
+ goto_hook_exit ();
+ goto_hook_call ();
+ d ()
in
step
@@ -557,11 +562,26 @@ let main () =
let round_button =
button ~use_mnemonic:true ~stock:`MEDIA_FORWARD ~packing:bbox#add ~label:"round" ()
in
+ let legitimate () =
+ 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;
+ (* change_label legitimate_button "Silen_t"; *)
+ ignore (legitimate_button#connect#clicked ~callback:
+ (button_cb true (fun () -> legitimate(); goto_hook_call ())));
+ legitimate_button#misc#hide(); (* indeed, in the defaut mode (manual central),
+ it should be hided *)
+ legitimate_button
+ in
+ let legitimate_button = legitimate () in
+
let ze_step =
if custom_mode then
- custom_daemon p text_out w step_button round_button
+ custom_daemon p text_out w step_button round_button legitimate_button
else
- s
+ s (* cf sasa-rdbg-cmds.ml *)
in
let step () =
ze_step();
@@ -581,23 +601,14 @@ let main () =
~callback:(
button_cb true (fun () ->
next_round_gui !roundnb;
- if !e.name <> "mv_hook" && !e.kind <> Call then goto_hook_call ())));
+ if custom_mode && !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 true (fun () -> pr();pr(); goto_hook_call ())));
- let legitimate () =
- 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;
- (* change_label legitimate_button "Silen_t"; *)
- ignore (legitimate_button#connect#clicked ~callback:
- (button_cb true (fun () -> legitimate(); goto_hook_call ())))
- in
- legitimate ();
let graph () =
let graph_button = button ~use_mnemonic:true ~packing:bbox#add () in
@@ -617,11 +628,14 @@ let main () =
butt
in
if args.oracles <> [] then (
- ignore (make_button `OK "_Oracle" "Move FORWARD until an oracle is violated"
+ let oracle_button = 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
- (fun () -> let str = viol_string () in goto_hook_call (); d();str)))
+ (fun () -> let str = viol_string () in goto_hook_call (); d();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 `UNDO "_Undo" "Undo the last move" (button_cb true (fun ()->u();d())) in
let _ = make_button `REFRESH "Restar_t" "Restart from the beginning"
diff --git a/tools/rdbg4sasa/sasa-rdbg-cmds.ml b/tools/rdbg4sasa/sasa-rdbg-cmds.ml
index 3ff960364de9727b911c5c79ed921e08fb3e781b..5143bc6fa63c444a405a0d8ea1ad0bcf617965e6 100644
--- a/tools/rdbg4sasa/sasa-rdbg-cmds.ml
+++ b/tools/rdbg4sasa/sasa-rdbg-cmds.ml
@@ -193,7 +193,7 @@ let str_of_sasa_event short e =
Printf.sprintf "%s_%s=%s" pid n (Data.val_to_string string_of_float v)
in
let pot = match List.assoc_opt "potential" e.data with
- | Some F f -> Printf.sprintf "potential = %.1f\n" f
+ | Some F f -> Printf.sprintf " => potential %.1f" f
| _ -> ""
in
let leg = match List.assoc_opt "legitimate" e.data with
@@ -209,12 +209,12 @@ let str_of_sasa_event short e =
(if e.step <> e.nb then (":" ^ (string_of_int e.nb)) else "")
(String.concat " " (List.map to_string_var vars))
else
- Printf.sprintf "Round %i - Step %i%s\n%s%s\n%s%s%s" !roundnb e.step
- (if e.step <> e.nb then (" - Event " ^ (string_of_int e.nb)) else "")
+ Printf.sprintf "Round %i - Step %i%s%s\n%s%s\n%s%s" !roundnb e.step
+ (if e.step <> e.nb then (" - Event " ^ (string_of_int e.nb)) else "") pot
(RdbgStdLib.string_of_event e)
(if vars = [] then "" else
("Active node states: "^(String.concat " " (List.map to_string_var vars))))
- pot leg silent
+ leg silent
)
let print_sasa_event short e =