Commit c47c5261 authored by erwan's avatar erwan
Browse files

Update: use the new RdbgStdLib.rev_cond_gen to round backwards (rdbg > 1.195.0)

parent bf4fe763
;; Time-stamp: <modified the 02/05/2021 (at 13:38) by Erwan Jahier>
;; Time-stamp: <modified the 09/06/2021 (at 15:07) by Erwan Jahier>
(library
(name sasacore)
(public_name sasacore)
(libraries dynlink ocamlgraph lutils)
(flags -noassert)
; (flags -noassert)
;;
; (wrapped false)
(library_flags -linkall)
......
(* Time-stamp: <modified the 03/06/2021 (at 14:35) by Erwan Jahier> *)
(* Time-stamp: <modified the 10/06/2021 (at 18:29) by Erwan Jahier> *)
#thread
#require "lablgtk3"
......@@ -118,7 +118,8 @@ let display_event b =
let custom_mode_ref = ref custom_mode
(* *)
let goto_hook_call e =
let goto_hook_call e =
if !custom_mode_ref then
next_cond e (fun e -> e.name = "mv_hook" && e.kind = Call)
else
......@@ -135,7 +136,7 @@ let goto_top e =
next_cond e (fun e -> e.kind = Ltop)
else
e
let init_rdbg_hook () =
let guidaemon sl =
if sl = [] then
......@@ -149,7 +150,9 @@ let init_rdbg_hook () =
in
Some res
else
let sl = List.filter (fun (n,v) -> String.length n > 5 && String.sub n 0 5 = "Enab_") sl in
let sl = List.filter
(fun (n,v) -> String.length n>5 && String.sub n 0 5 = "Enab_") sl
in
let res = List.map (fun (n,enabled) ->
(* n est de la forme Enab_node_state, enabled est un Data.v *)
let str = String.sub n 5 ((String.length n)-5) in
......@@ -186,8 +189,29 @@ let init_rdbg_hook () =
let set_tooltip b = b#misc#set_tooltip_text
let custom_daemon p gtext vbox step_button back_step_button round_button legitimate_button =
let start () =
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 *)
e:=goto_hook_exit !e;
if !custom_mode_ref then e := goto_hook_call !e;
redos := [!e.nb];
ckpt_list := [!e];
!e.save_state !e.nb
let restart p _ =
let seed = Seed.get dotfile in
Seed.set seed;
p (Printf.sprintf "Restarting using the seed %d" seed);
!e.RdbgEvent.reset();
e:=RdbgStdLib.run ~call_hooks:true ();
round_reset ();
start ();
d()
let custom_daemon p gtext vbox step_button back_step_button round_button
legitimate_button undo_button =
(* création du rdbg_mv_hook et de tout ce qu'il faut autour *)
init_rdbg_hook ();
......@@ -210,21 +234,18 @@ let custom_daemon p gtext vbox step_button back_step_button round_button legitim
set_tooltip dk_manual (Printf.sprintf "Set the manual mode");
set_tooltip dk_manual_central (Printf.sprintf "Set the manual central mode");
(* Necessary for salut (to perform a fake step that let sasa provide
the first set of enables) *)
if args.salut_mode then e := goto_hook_exit !e;
e := goto_hook_call !e;
start ();
blue_add gtext#buffer (str_of_sasa_event false !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é *)
let update_rdbg_hook node activate =
(match !daemon_kind with
| Distributed | Synchronous | Central | LocCentral ->
assert false (* SNO *)
| ManualCentral -> (
let txt = Printf.sprintf "ManualCentral step: %s\n\n%s" node (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.filter_map_inplace (fun n status -> Some (n = node)) daemongui_activate;
......@@ -361,6 +382,7 @@ let custom_daemon p gtext vbox step_button back_step_button round_button legitim
show step_button; show checkbox_grid;
hide back_step_button;
hide legitimate_button;
hide undo_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
......@@ -372,6 +394,7 @@ let custom_daemon p gtext vbox step_button back_step_button round_button legitim
);
checkbox#set_sensitive enabled
| ManualCentral ->
hide undo_button;
hide legitimate_button;
(match !oracle_button_ref with Some b -> hide b | None -> ());
(* hide back_step_button; *)
......@@ -381,7 +404,10 @@ let custom_daemon p gtext vbox step_button back_step_button round_button legitim
let pushbox = Hashtbl.find pushbox_map node in
if enabled then show pushbox else hide pushbox;
pushbox#set_sensitive enabled
| Distributed | Synchronous | Central | LocCentral ->
| Synchronous | Distributed | Central | LocCentral ->
if !daemon_kind = Synchronous then show undo_button
else hide undo_button;
(match !oracle_button_ref with Some b -> show b | None -> ());
show back_step_button; show step_button; show round_button;
show counter_grid; show legitimate_button;
......@@ -424,7 +450,7 @@ let custom_daemon p gtext vbox step_button back_step_button round_button legitim
(* Affichage d'informations *)
(* gtext#buffer#set_text !gtext_content; *)
let rec get_higher_prioriry nl =
let rec get_higher_priority nl =
let prio n =
let counter = Hashtbl.find counter_map n in
counter#get
......@@ -450,7 +476,7 @@ let custom_daemon p gtext vbox step_button back_step_button round_button legitim
*)
let nodes_enabled = rdbg_nodes_enabled e in
let nodes = List.filter (fun (_,b) -> b) nodes_enabled in
let nodes = get_higher_prioriry nodes in
let nodes = get_higher_priority nodes in
(* p ("==> gtkgui: CALL =" ^ (string_of_event e)); *)
(match !daemon_kind with
| Distributed -> (
......@@ -545,7 +571,7 @@ let main () =
cmd ();
if store_flag then store !e.nb;
if display_event_flag then display_event text_out;
refresh ()
d ()
in
let button_cb_string cmd () =
let txt = Printf.sprintf "\n%s" (cmd ()) in
......@@ -573,9 +599,20 @@ let main () =
let image = GMisc.image ~file:(libui_prefix^"/chut_small.svg") () in
legitimate_button#set_image image#coerce;
let make_button stock lbl msg cmd =
let butt = button ~use_mnemonic:true ~stock:stock ~packing:bbox#add ~label:lbl () in
set_tooltip butt msg;
change_label butt lbl;
ignore (butt#connect#clicked ~callback:cmd);
butt
in
let undo_button = make_button `UNDO "_Undo" "Undo the last move"
(button_cb true false (fun ()->u();d()))
in
let set_daemongui_tbl =
if !custom_mode_ref then
custom_daemon p text_out w step_button back_step_button round_button legitimate_button
custom_daemon p text_out w step_button back_step_button round_button
legitimate_button undo_button
else
(fun _ -> ())
in
......@@ -599,20 +636,31 @@ let main () =
e
in
let back_step_gui () =
let lnext e =
if args.salut_mode then
let e = goto_top e in
if args.salut_mode then
let lnext e =
set_daemongui_tbl e;
let e = goto_top e in
e
else
let e = goto_hook_call e in
in
let ne = rev_cond_gen !e
(fun ne -> ne.step = !e.step-1 && ne.kind = Ltop)
lnext restore_round_nb
in
e:=ne
else
let lnext e =
set_daemongui_tbl e;
if e.kind = Ltop then
(* Necessary for reproductibility because set_daemongui_tbl
calls Random.int (via Daemon) which changes the PRGS! *)
e.restore_state e.nb;
let e = goto_hook_call e in
e
in
let ne = rev_cond_gen !e (fun ne -> ne.step = !e.step-1) lnext in
if ne.kind <> !e.kind || ne.name <> !e.name then
e:=next_cond ne (fun ne -> ne.kind = !e.kind || ne.name = !e.name)
else
in
let ne = rev_cond_gen !e
(fun ne -> ne.step = !e.step-1 && ne.name = "mv_hook" && ne.kind = Call)
lnext restore_round_nb
in
e:=ne
in
ignore (back_step_button#connect#clicked
......@@ -633,7 +681,7 @@ let main () =
(* indeed, in the defaut mode (manual central), it should be hided *)
let rec next_round_gui rn =
if is_silent !e then () else e:=a_gui_step !e;
if rn < !roundnb || is_silent !e then () else (next_round_gui rn);
if rn < !round_st_ref.cpt || is_silent !e then () else (next_round_gui rn);
in
set_tooltip step_button "Move FORWARD to the next STEP";
......@@ -645,7 +693,7 @@ let main () =
~callback:(
button_cb true true (fun () ->
if !custom_mode_ref then (
next_round_gui !roundnb;
next_round_gui !round_st_ref.cpt ;
if !custom_mode_ref && !e.name <> "mv_hook" && !e.kind <> Call
&& not (is_silent !e)
then
......@@ -658,7 +706,15 @@ let main () =
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 true (fun () -> pr();pr(); e:=goto_hook_call !e)));
~callback:(button_cb true true
(fun () ->
e:=goto_last_ckpt !e.nb;
e:=goto_last_ckpt !e.nb;
restore_round_nb !e.nb;
store !e.nb;
e:=goto_hook_call !e;
refresh ()
)));
let graph () =
......@@ -671,37 +727,18 @@ let main () =
in
graph ();
let make_button stock lbl msg cmd =
let butt = button ~use_mnemonic:true ~stock:stock ~packing:bbox#add ~label:lbl () in
set_tooltip butt msg;
change_label butt lbl;
ignore (butt#connect#clicked ~callback:cmd);
butt
in
if args.oracles <> [] then (
let oracle_button =
make_button `OK "_Oracle" "Move FORWARD until an oracle is violated"
(button_cb_string
(fun () -> let str = viol_string () in e:=goto_hook_call !e; d(); store !e.nb; str))
(fun () -> let str = viol_string () in
e:=goto_hook_call !e; d(); store !e.nb; 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 false (fun ()->u();d())) in
let _ = make_button `REFRESH "Restar_t" "Restart from the beginning"
(button_cb true 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
*)
e:=goto_hook_exit !e;
e:=goto_hook_call !e;
d()))
(button_cb true true (restart p))
in
let _ = make_button `REFRESH "_New Seed" "Restart from the beginning using a New Seed"
(button_cb true true
......
This diff is collapsed.
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