diff --git a/tools/rdbg4sasa/gtkgui.ml b/tools/rdbg4sasa/gtkgui.ml index 7afb6cf59550d86bc8070fa92e0db411dac4a5c0..006cd0c69ae9a6a828a15e71382d086d82ff85be 100644 --- a/tools/rdbg4sasa/gtkgui.ml +++ b/tools/rdbg4sasa/gtkgui.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 14/05/2021 (at 15:40) by Erwan Jahier> *) +(* Time-stamp: <modified the 19/05/2021 (at 17:04) by Erwan Jahier> *) #thread #require "lablgtk3" @@ -482,7 +482,8 @@ let main () = in let button_cb_string cmd () = let txt = Printf.sprintf "%s" (cmd ()) in - text_out#buffer#set_text txt + text_out#buffer#set_text txt; + refresh () in let back_step_button = button ~use_mnemonic:true ~stock:`GO_BACK ~packing:bbox#add () in @@ -513,10 +514,12 @@ let main () = ignore (step_button#connect#clicked ~callback:(button_cb step)); set_tooltip round_button "Move FORWARD to the next ROUND"; change_label round_button "_Round"; - ignore (round_button#connect#clicked ~callback:(button_cb nr)); + ignore (round_button#connect#clicked + ~callback:(button_cb (fun () -> nr(); 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 pr)); + ignore (back_round_button#connect#clicked + ~callback:(button_cb (fun () -> pr();pr(); goto_hook_call()))); let legitimate () = let legitimate_button = button ~use_mnemonic:true ~packing:bbox#add () in diff --git a/tools/rdbg4sasa/sasa-rdbg-cmds.ml b/tools/rdbg4sasa/sasa-rdbg-cmds.ml index 03bf1a8a168e7ded1abb75782e46fc45dcfbcbb0..19c2284dee449d0b3f74f7844238696092543167 100644 --- a/tools/rdbg4sasa/sasa-rdbg-cmds.ml +++ b/tools/rdbg4sasa/sasa-rdbg-cmds.ml @@ -91,7 +91,12 @@ let (round : RdbgEvent.t -> bool) = round with Not_found -> let round = - e.kind = Ltop && + ( if args.salut_mode then + e.kind = Exit && e.name = "mv_hook" && e.step > 1 + else + e.kind = Ltop + ) + && let (pl : process list) = get_processes e in let rm_me = get_removable pl in if !verbose then ( @@ -139,8 +144,8 @@ let update_round_nb e = (* go to next and previous rounds *) let next_round e = let ne = next_cond e round in - if ne.kind = e.kind then ne else next e - + ne + let nr () = e:=next_round !e; store !e.nb; !dot_view ();; let pr () = e:=goto_last_ckpt !e.nb; @@ -188,17 +193,21 @@ let str_of_sasa_event short e = let to_string_var (pid, n, v) = 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 + | _ -> "" + in let vars = List.rev vars in update_round_nb e; - if short then - Printf.sprintf "[round %i, step %i%s] %s\n" !roundnb e.step + (if short then + Printf.sprintf "[round %i, step %i%s] %s %s\n" !roundnb e.step pot (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" !roundnb e.step + 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)) - + (String.concat " " (List.map to_string_var vars)) pot + ) ^ (RdbgStdLib.string_of_event e) let print_sasa_event short e = if e.kind <> Ltop then print_event e else @@ -236,6 +245,21 @@ let _ = add_doc_entry "viol" "unit -> unit" "Move forward until the oracle is violated" "sasa" "sasa-rdbg-cmds.ml" +(**********************************************************************) +(* Potential *) + +let potential_opt () = List.assoc_opt "potential" !e.data + +let potential () = + match potential_opt () with + | Some F f -> Some f + | _ -> None + +let _ = add_doc_entry + "potential" "unit -> float option" "returns the current potential if available" + "sasa" "sasa-rdbg-cmds.ml" + + (**********************************************************************) (* Move forward until silence *)