From 72e6c5960938af0a38a99b444bae1c679b284917 Mon Sep 17 00:00:00 2001 From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr> Date: Wed, 26 May 2021 10:52:41 +0200 Subject: [PATCH] Update: some rdbgui4sasa enhancements --- tools/rdbg4sasa/dot4sasa.ml | 8 +- tools/rdbg4sasa/gtkgui.ml | 197 ++++++++++++++++++++---------- tools/rdbg4sasa/sasa-rdbg-cmds.ml | 33 +++-- 3 files changed, 160 insertions(+), 78 deletions(-) diff --git a/tools/rdbg4sasa/dot4sasa.ml b/tools/rdbg4sasa/dot4sasa.ml index 148d29e2..f8d40393 100644 --- a/tools/rdbg4sasa/dot4sasa.ml +++ b/tools/rdbg4sasa/dot4sasa.ml @@ -191,10 +191,14 @@ let to_pdf engine par_var only_parent rn g f e = else Printf.sprintf "subgraph dir {\n\t%s} subgraph undir {\n\t edge [dir=none]\n%s} " trans_dir_str trans_undir_str + in + let pot = match List.assoc_opt "potential" e.data with + | Some F f -> Printf.sprintf " potential=%.1f" f + | _ -> "" in Printf.fprintf oc - "digraph %s {\nlabel=\"%s \nRound %d Step %d\"\nnode [shape=record];\n%s\n%s\n}\n" - "g" f rn e.step + "digraph %s {\nlabel=\"%s \nRound %d Step %d%s\"\nnode [shape=record];\n%s\n%s\n}\n" + "g" f rn e.step pot nodes_decl trans_str; flush oc; close_out oc; diff --git a/tools/rdbg4sasa/gtkgui.ml b/tools/rdbg4sasa/gtkgui.ml index b15413b1..34c5ca5e 100644 --- a/tools/rdbg4sasa/gtkgui.ml +++ b/tools/rdbg4sasa/gtkgui.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 22/05/2021 (at 21:21) by Erwan Jahier> *) +(* Time-stamp: <modified the 26/05/2021 (at 10:37) by Erwan Jahier> *) #thread #require "lablgtk3" @@ -79,9 +79,46 @@ let (fake_val_of_type : Data.t -> Data.v) = function | Alias _ -> assert false | String _ -> assert false + +(**********************************************************************************) +(* Write with colors *) +let create_tags (buffer:GText.buffer) = + buffer#create_tag ~name:"blue_foreground" [`FAMILY "monospace"; `FOREGROUND "blue"]; + buffer#create_tag ~name:"black_foreground" [`FAMILY "monospace"; `FOREGROUND "black"]; + buffer#create_tag ~name:"red_foreground" [`FAMILY "monospace"; `FOREGROUND "red"]; + buffer#create_tag ~name:"green_foreground" [`FAMILY "monospace"; `FOREGROUND "green"]; + buffer#create_tag ~name:"red_background" [`BACKGROUND "red"]; + () + +let tags_created = ref false + +let write color b str = + if not !tags_created then (create_tags b; tags_created := true); + b#set_text ""; + b#insert ~tag_names:[color] str + +let write_add color b str = + if not !tags_created then (create_tags b; tags_created := true); + b#insert ~tag_names:[color] str + + +let blue = write "blue_foreground" +let black = write "black_foreground" +let red = write "red_foreground" +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 () = - e := next_cond !e (fun e -> e.name = "mv_hook" && e.kind = Call) +let goto_hook_call b = + e := next_cond !e (fun e -> e.name = "mv_hook" && e.kind = Call); + blue_add b#buffer "----------------------------------------"; + blue_add b#buffer "----------------------------------------\n"; + blue_add b#buffer (str_of_sasa_event false !e) + let goto_hook_exit () = e := next_cond !e (fun e -> e.name = "mv_hook" && e.kind = Exit) @@ -133,6 +170,7 @@ let init_rdbg_hook () = let set_tooltip b = b#misc#set_tooltip_text + let custom_daemon p gtext vbox step_button round_button = (* création du rdbg_mv_hook et de tout ce qu'il faut autour *) init_rdbg_hook (); @@ -159,7 +197,8 @@ 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_call ();goto_hook_call (); + goto_hook_exit (); + goto_hook_call gtext; d() ); let nodes_enabled = rdbg_nodes_enabled !e in @@ -170,15 +209,16 @@ let custom_daemon p gtext vbox step_button round_button = | Distributed | Synchronous | Central | LocCentral -> assert false (* SNO *) | ManualCentral -> ( - let txt = Printf.sprintf "ManualCentral step: %s\n%s" node (str_of_sasa_event false !e) in - gtext#buffer#set_text txt; + 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%s" (str_of_sasa_event false !e) in - gtext#buffer#set_text txt; + 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 ); @@ -229,7 +269,9 @@ let custom_daemon p gtext vbox step_button round_button = ~height:300 ~shadow_type:`OUT ~packing:pushbox_grid#add () in - let pushbox_scrolled_grid_box = GPack.vbox ~homogeneous:true ~packing:pushbox_scrolled_grid#add () in + let pushbox_scrolled_grid_box = + GPack.vbox ~homogeneous:true ~packing:pushbox_scrolled_grid#add () + in let pushbox_line = GPack.hbox ~packing:pushbox_scrolled_grid_box#add () in let pushbox_line_ref = ref pushbox_line in let pushbox_map = Hashtbl.create n in @@ -249,7 +291,7 @@ let custom_daemon p gtext vbox step_button round_button = ~callback: (fun _ -> update_rdbg_hook name true; goto_hook_exit (); - goto_hook_call (); + goto_hook_call gtext; refresh (); false)); Hashtbl.add pushbox_map name pushbox @@ -332,12 +374,24 @@ let custom_daemon p gtext vbox step_button round_button = in Hashtbl.add refresh_fun_tbl "" update_all_checkboxes; - let set_dd_mode () = daemon_kind := Distributed; refresh () in - let set_sd_mode () = daemon_kind := Synchronous; refresh () in - let set_cd_mode () = daemon_kind := Central; refresh () in - let set_lcd_mode () = daemon_kind := LocCentral; refresh () in - let set_manual_mode () = daemon_kind := Manual; refresh () in - let set_manual_central_mode () = daemon_kind := ManualCentral; refresh () in + let set_dd_mode () = + black gtext#buffer"==> Switch to a distributed daemon\n"; + daemon_kind := Distributed; refresh () in + let set_sd_mode () = + black gtext#buffer"==> Switch to a synchronous daemon\n"; + daemon_kind := Synchronous; refresh () in + let set_cd_mode () = + black_add gtext#buffer"==> Switch to a central daemon\n"; + daemon_kind := Central; refresh () in + let set_lcd_mode () = + black gtext#buffer"==> Switch to a locally central daemon\n"; + daemon_kind := LocCentral; refresh () in + let set_manual_mode () = + black gtext#buffer"==> Switch to a manual daemon\n"; + daemon_kind := Manual; refresh () in + let set_manual_central_mode () = + black gtext#buffer"==> Switch to a manual central daemon\n"; + daemon_kind := ManualCentral; refresh () in ignore(dk_dd#connect#clicked ~callback:set_dd_mode); ignore(dk_sd#connect#clicked ~callback:set_sd_mode); ignore(dk_cd#connect#clicked ~callback:set_cd_mode); @@ -374,19 +428,27 @@ let custom_daemon p gtext vbox step_button round_button = 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 () + goto_hook_exit (); + goto_hook_call gtext; + d () ) | Synchronous -> ( Hashtbl.clear daemongui_activate; List.iter (fun n -> Hashtbl.replace daemongui_activate n true) nodes; - goto_hook_exit (); goto_hook_call (); d () + goto_hook_exit (); + goto_hook_call gtext; + 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 -> Hashtbl.replace daemongui_activate n true) to_activate; - goto_hook_exit (); goto_hook_call (); d () + List.iter (fun n -> + Printf.printf "Activating %s\n" n; + Hashtbl.replace daemongui_activate n true) to_activate; + goto_hook_exit (); + goto_hook_call gtext; + d () ) | LocCentral -> ( let get_neigbors x = @@ -400,10 +462,15 @@ let custom_daemon p gtext vbox step_button round_button = 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 () + goto_hook_exit (); + goto_hook_call gtext; + d () ) | ManualCentral -> () (* SNO; the step is done in pushbox callbacks *) - | Manual -> goto_hook_exit (); goto_hook_call (); d () + | Manual -> + goto_hook_exit (); + goto_hook_call gtext; + d () in step @@ -419,6 +486,7 @@ let libui_prefix = prefix ^ "/lib/rdbgui4sasa" let oc_stdin = stdout let ic_stdout = stdin + open GButton (* GTK3 *) let main () = @@ -439,38 +507,10 @@ let main () = 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 - in - let p str = - text_out#set_buffer (GText.buffer ~text:str ()); - Printf.printf "%s\n%!" str; in - (* It should be better to rely on the gtk event handler + let p str = black text_out#buffer str in + (* It should be better to rely on the gtk event handler *) - let sw1 = GBin.scrolled_window ~border_width:10 ~shadow_type:`IN ~height:30 ~width:50 - ~packing:box#add () - in - sw1#misc#set_tooltip_text "This window displays the commands sent to the rdbg cli"; - let text_in = GText.view ~wrap_mode:`CHAR ~height:250 ~editable:true ~width:50 - ~packing: sw1#add () ~cursor_visible:true - in - let rec read_text_in () = - let buff = text_in#buffer#get_text () in - let size = String.length buff in - if size >0 then ( - let last = String.get buff (size - 1) in - if last = '\n' then ( - Printf.fprintf oc_stdin "%s\n%!" buff; - Printf.printf "%s\n%!" buff; - text_in#set_buffer (GText.buffer ~text:"(rdbg) " ()) - ) else () - ); - Unix.sleepf 0.1; - read_text_in () - in - let _ = Thread.create read_text_in () in - *) - (* Printf.fprintf oc_stdin "#use \"sasa-rdbg-cmds.ml\";;\n%!"; *) - (* Printf.fprintf oc_stdin "print_sasa_event false !e;;\n%!"; (* print the first event *) *) let bbox = GPack.hbox ~packing: box#add () in let change_label button str = @@ -480,14 +520,17 @@ let main () = refresh () in let button_cb 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 (); - let txt = Printf.sprintf "%s" (str_of_sasa_event false !e) in - text_out#buffer#set_text txt; refresh () in let button_cb_string cmd () = - let txt = Printf.sprintf "%s" (cmd ()) in - text_out#buffer#set_text txt; + let txt = Printf.sprintf "\n%s" (cmd ()) in + (* text_out#buffer#set_text txt; *) + blue_add text_out#buffer txt; refresh () in @@ -513,6 +556,10 @@ let main () = ze_step(); d() in + let rec next_round_gui rn = + ze_step(); (* il faut un step qui mette à jour la table des rondes. c'est pas le cas ? *) + if rn < !roundnb || is_silent !e then () else (next_round_gui rn) + in set_tooltip step_button "Move FORWARD to the next STEP"; change_label step_button "_Step"; @@ -520,11 +567,13 @@ let main () = set_tooltip round_button "Move FORWARD to the next ROUND"; change_label round_button "_Round"; ignore (round_button#connect#clicked - ~callback:(button_cb (fun () -> nr(); goto_hook_call()))); + ~callback:(button_cb (fun () -> + next_round_gui !roundnb; + if !e.name <> "mv_hook" && !e.kind <> Call then goto_hook_call text_out))); 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()))); + ~callback:(button_cb (fun () -> pr();pr(); goto_hook_call text_out))); let legitimate () = let legitimate_button = button ~use_mnemonic:true ~packing:bbox#add () in @@ -557,9 +606,9 @@ let main () = in if args.oracles <> [] then ( 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)) + (* let image = GMisc.image ~file:"../rdbg-utils/oracle_small.jpg" () in *) + (* viol_button#set_image image#coerce; *) + (button_cb_string viol_string)) ); let _ = make_button `UNDO "_Undo" "Undo the last move" (button_cb (fun ()->u();d())) in let _ = make_button `REFRESH "Restar_t" "Restart from the beginning" @@ -574,7 +623,7 @@ let main () = but the hook does not need input at this first step *) goto_hook_exit (); - goto_hook_call (); + goto_hook_call text_out; d())) in let _ = make_button `REFRESH "_New Seed" "Restart from the beginning using a New Seed" @@ -591,7 +640,7 @@ let main () = but the hook does not need input at this first step *) goto_hook_exit (); - goto_hook_call (); + goto_hook_call text_out; d())) in let _ = make_button `MEDIA_PLAY "_Sim2chro" "Launch sim2chro on the generated data (so far)" @@ -606,7 +655,29 @@ let main () = 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 () + 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 + in + let rdbg_log = open_in "rdbg.log" in + create_tags text_in#buffer; + let rec read_rdbglog () = + try + let str = input_line rdbg_log in + text_in#buffer#insert ~tag_names:["black_foreground"] (str^"\n"); + let end_mark = text_in#buffer#create_mark text_in#buffer#end_iter in + text_in#scroll_to_mark (`MARK end_mark); + read_rdbglog () + with End_of_file -> + Unix.sleepf 1.0; + 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 () diff --git a/tools/rdbg4sasa/sasa-rdbg-cmds.ml b/tools/rdbg4sasa/sasa-rdbg-cmds.ml index 19c2284d..3ff96036 100644 --- a/tools/rdbg4sasa/sasa-rdbg-cmds.ml +++ b/tools/rdbg4sasa/sasa-rdbg-cmds.ml @@ -55,8 +55,7 @@ let dot_view : (unit -> unit) ref = let d () = !dot_view () let sd () = s();!dot_view();; -let nd () = n();!dot_view();; -let bd () = b();!dot_view();; +let bd()= e:=prev !e ; emacs_udate !e; pe();!dot_view();; (**********************************************************************) @@ -141,7 +140,7 @@ let update_round_nb e = | None -> () | Some (n,_) -> roundnb := n -(* go to next and previous rounds *) +(* go to next round *) let next_round e = let ne = next_cond e round in ne @@ -185,7 +184,7 @@ let only_true l = List.filter (fun (_,_, v) -> v = B true) l (* Only print the active process values *) let str_of_sasa_event short e = let enab, act, vars = split_data e.data in - (* let enab = only_true enab in *) + let enab = only_true enab in let act = only_true act in let act_pid = List.map (fun (pid,_,_) -> pid) act in let vars = List.filter (fun (pid, _,_) -> List.mem pid act_pid) vars in @@ -194,9 +193,15 @@ 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" f + | Some F f -> Printf.sprintf "potential = %.1f\n" f | _ -> "" in + let leg = match List.assoc_opt "legitimate" e.data with + | Some B true -> Printf.sprintf "The current configuration is legitimate\n" + | Some B false -> "" + | _ -> "" + in + let silent = if enab = [] then "The current configuration is silent\n" else "" in let vars = List.rev vars in update_round_nb e; (if short then @@ -204,10 +209,13 @@ 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 \nActive node states: %s\n%s\n" !roundnb e.step - (if e.step <> e.nb then ("\nEvent nb " ^ (string_of_int e.nb)) else "") - (String.concat " " (List.map to_string_var vars)) pot - ) ^ (RdbgStdLib.string_of_event e) + 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 "") + (RdbgStdLib.string_of_event e) + (if vars = [] then "" else + ("Active node states: "^(String.concat " " (List.map to_string_var vars)))) + pot leg silent + ) let print_sasa_event short e = if e.kind <> Ltop then print_event e else @@ -266,7 +274,7 @@ let _ = add_doc_entry let is_silent e = match List.assoc_opt "silent" e.data with | Some B b -> b - | _ -> assert false + | _ -> 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 ();; @@ -282,7 +290,7 @@ let _ = add_doc_entry let is_legitimate e = match List.assoc_opt "legitimate" e.data with | Some B b -> b - | _ -> assert false + | _ -> 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 ();; @@ -309,8 +317,7 @@ let _ = add_doc_entry "sd" "unit -> unit" "go to the next step and update the network with one of the GraphViz tools" "sasa" "sasa-rdbg-cmds.ml"; - add_doc_entry "nd" "unit -> unit" "go to the next event and update the network" "sasa" "sasa-rdbg-cmds.ml"; - add_doc_entry "bd" "unit -> unit" "go to the previous event and update the network" "sasa" "sasa-rdbg-cmds.ml"; + add_doc_entry "bd" "unit -> unit" "go to the previous step and update the network" "sasa" "sasa-rdbg-cmds.ml"; add_doc_entry "nr" "unit -> unit" "go to the next round and update the network" "sasa" "sasa-rdbg-cmds.ml"; add_doc_entry "pr" "unit -> unit" "go to the previous round and update the network" "sasa" "sasa-rdbg-cmds.ml"; add_doc_entry "d_par" "unit -> unit" "cf d (for topology with a parent field)" "sasa" "sasa-rdbg-cmds.ml"; -- GitLab