Commit 7b88e1cc authored by erwan's avatar erwan
Browse files

Fix: the forward and backward rounds with salut

parent 47f12787
(* 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
......
......@@ -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 *)
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment