From c47c5261a13dde27510fddb406be67632e7e78de Mon Sep 17 00:00:00 2001
From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr>
Date: Mon, 7 Jun 2021 15:03:44 +0200
Subject: [PATCH] Update: use the new RdbgStdLib.rev_cond_gen to round
backwards (rdbg > 1.195.0)
---
lib/sasacore/dune | 4 +-
tools/rdbg4sasa/gtkgui.ml | 141 +++++---
tools/rdbg4sasa/sasa-rdbg-cmds.ml | 522 +++++++++++++++++-------------
3 files changed, 387 insertions(+), 280 deletions(-)
diff --git a/lib/sasacore/dune b/lib/sasacore/dune
index 0c19b2d1..c3e52b8e 100644
--- a/lib/sasacore/dune
+++ b/lib/sasacore/dune
@@ -1,10 +1,10 @@
-;; 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)
diff --git a/tools/rdbg4sasa/gtkgui.ml b/tools/rdbg4sasa/gtkgui.ml
index eb21ff64..6e7810fd 100644
--- a/tools/rdbg4sasa/gtkgui.ml
+++ b/tools/rdbg4sasa/gtkgui.ml
@@ -1,4 +1,4 @@
-(* 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
diff --git a/tools/rdbg4sasa/sasa-rdbg-cmds.ml b/tools/rdbg4sasa/sasa-rdbg-cmds.ml
index 627fb956..4c5c532e 100644
--- a/tools/rdbg4sasa/sasa-rdbg-cmds.ml
+++ b/tools/rdbg4sasa/sasa-rdbg-cmds.ml
@@ -23,18 +23,29 @@ let is_legitimate e =
(**********************************************************************)
(** Computing rounds *)
-let roundnb = ref (-666)
-let mask = ref [] (* nodes we look the activation of *) (* XXX use an array! *)
-let roundtbl = Hashtbl.create 10;; (* maps event nb to round + round nb *)
-(* let _ = Hashtbl.add roundtbl 1 (1,true);; *)
+module IntMap = Map.Make(Int)
+
+type round_st = {
+ cpt: int;
+ mask : string list; (* nodes we look the activation of *) (* XXX use an array! *)
+ tbl : (int * bool * string list) IntMap.t
+ (* maps event nb to round, round nb, and mask *)
+ }
+
let verbose = ref false
-let round_init () =
- roundnb := 1;
- mask := [];
- Hashtbl.clear roundtbl
+let round_st_init = {
+ cpt = 1;
+ mask = [];
+ tbl = IntMap.empty
+ }
+
+let round_st_ref = ref round_st_init
+let round_reset () = round_st_ref := round_st_init
-let _ = round_init ();;
+let set_round_st_cpt n = round_st_ref := { !round_st_ref with cpt = n }
+let set_round_st_mask m = round_st_ref := { !round_st_ref with mask = m }
+let set_round_st_tbl t = round_st_ref := { !round_st_ref with tbl = t }
(* a process can be removed from the mask if one action of p is triggered
or if no action of p is enabled *)
@@ -56,130 +67,170 @@ let enabled pl = (* returns the enabled processes *)
List.map (fun p -> p.name) el
(* called at each event via the time-travel hook *)
-let (round : RdbgEvent.t -> bool) = fun e ->
- match Hashtbl.find_opt roundtbl e.nb with
+let (round : bool -> RdbgEvent.t -> bool) =
+ fun from_past e ->
+ if from_past then set_round_st_tbl (IntMap.remove e.nb !round_st_ref.tbl);
+ match IntMap.find_opt e.nb !round_st_ref.tbl with
| Some (croundnb, round, cmask) ->
(* Printf.printf "round tabulated at e.nb %d: croundnb=%d round = %b\n%!" *)
(* e.nb croundnb round; *)
- roundnb := croundnb;
- mask := cmask;
+ set_round_st_cpt croundnb;
+ set_round_st_mask cmask;
round
| None ->
- if !mask = [] && is_silent e then false else
- let round =
- ( (* we check if a round occurs when activated processes are available *)
- if args.salut_mode then
- e.kind = Exit && e.name = "mv_hook" && e.step > 1
+ if !round_st_ref.mask = [] && is_silent e then false else
+ let round =
+ if not
+ ( (* we check if a round occurs when activated processes are available *)
+ if args.salut_mode then
+ e.kind = Exit && e.name = "mv_hook" && e.step > 1
+ else
+ e.kind = Ltop
+ )
+ then false
else
- e.kind = Ltop
- )
- &&
- let (pl : process list) = get_processes e in
- if !mask = [] then mask := enabled pl; (* occurs at the first possible round *)
- let rm_me = get_removable pl in
- if !verbose then (
- Printf.printf "\nMask (event %d): %s\n" e.nb (String.concat "," !mask);
- Printf.printf "To remove from mask: %s\n%!" (String.concat "," rm_me)
- );
- mask := List.filter (fun pid -> not (List.mem pid rm_me)) !mask;
- if !verbose then
- Printf.printf "New Mask: %s\n%!" (String.concat "," !mask);
- let res = !mask = [] in
- if res then (
- mask := (
- let mask =
- List.filter
- (fun p -> List.exists (fun (_,e,a) -> e && not(a)) p.actions)
- pl
- in
- let mask = List.map (fun p -> p.name) mask in
- if !verbose then (
- let mask = List.rev mask in
- Printf.printf "Next mask : %s\n%!" (String.concat "," mask);
- flush stdout
- );
- mask
- )
- );
- res
- in
- if round then incr roundnb;
- Hashtbl.add roundtbl e.nb (!roundnb, round, !mask);
- (* Printf.printf "round computed at e.nb %d: croundnb=%d round = %b\n%!"
+ let (pl : process list) = get_processes e in
+ if !round_st_ref.mask = [] then
+ (* occurs at the first possible round, or when all
+ processes in the previous mask were the only triggered
+ processes *)
+ set_round_st_mask (enabled pl);
+ let rm_me = get_removable pl in
+ if !verbose then (
+ Printf.printf "\nMask (event %d): %s\n" e.nb
+ (String.concat "," !round_st_ref.mask);
+ Printf.printf "To remove from mask: %s\n%!" (String.concat "," rm_me)
+ );
+ set_round_st_mask
+ (List.filter (fun pid -> not (List.mem pid rm_me)) !round_st_ref.mask);
+ if !verbose then
+ Printf.printf "New Mask: %s\n%!" (String.concat "," !round_st_ref.mask);
+ let res = !round_st_ref.mask = [] in
+ if res then (
+ set_round_st_mask (
+ let mask =
+ List.filter
+ (fun p -> List.exists (fun (_,e,a) -> e && not(a)) p.actions)
+ pl
+ in
+ let mask = List.map (fun p -> p.name) mask in
+ if !verbose then (
+ let mask = List.rev mask in
+ Printf.printf "Next mask : %s\n%!" (String.concat "," mask);
+ flush stdout
+ );
+ mask
+ )
+ );
+ res
+ in
+ if round then set_round_st_cpt (!round_st_ref.cpt + 1);
+ if !verbose then
+ Printf.printf "IntMap.add e.nb=%d round_nb=%d round= %b mask=%s\n%!"
+ e.nb !round_st_ref.cpt round (String.concat "," !round_st_ref.mask);
+ set_round_st_tbl
+ (IntMap.add e.nb (!round_st_ref.cpt, round, !round_st_ref.mask)
+ !round_st_ref.tbl);
+ (* Printf.printf "round computed at e.nb %d: croundnb=%d round = %b\n%!"
e.nb !roundnb round; *)
- round
+ round
-let update_round_nb e =
- match Hashtbl.find_opt roundtbl e.nb with
- | None -> ()
- | Some (n,_, m) -> roundnb := n; mask := m
+
+let restore_round_nb i =
+ match IntMap.find_opt i !round_st_ref.tbl with
+ | None ->
+ (* Printf.printf "restore_round_nb: At event %d, nothing to restore\n%!" e.nb ; *)
+ ()
+ | Some (n,_, m) ->
+ (* Printf.printf "restore_round_nb: At event %d, restore the rn %d\n%!" e.nb n; *)
+ set_round_st_cpt n;
+ set_round_st_mask m;
+ ()
+
+let sasa_next e =
+ let ne = e.next () in
+ List.iter
+ (fun str -> if str<>"print_event" then (RdbgStdLib.get_hook str) ne)
+ (RdbgStdLib.list_hooks ());
+ ne
-(* go to next round *)
let next_round e =
- let ne = next_cond e round in
- ne
+ next_cond_gen e (round true) sasa_next
+let back_step e =
+ rev_cond_gen e (fun ne -> ne.kind = e.kind && ne.name = e.name)
+ sasa_next restore_round_nb
+
(**********************************************************************)
(* redefine (more meaningful) step and back-step for sasa *)
let sasa_step e = next_cond e (fun ne -> ne.kind = e.kind && ne.name = e.name)
-let sasa_bstep e = rev_cond e (fun ne -> ne.kind = e.kind && ne.name = e.name)
let s () = e:=sasa_step !e ; emacs_udate !e; store !e.nb;pe()
-let b () = e:=sasa_bstep !e ; emacs_udate !e; store !e.nb;pe()
+let b () =
+ let ne = back_step !e in
+ e:=ne ;
+ emacs_udate !e; store !e.nb;pe()
let p =
try Topology.read dotfile
with _ -> failwith "This is not a sasa rdbg session!";;
-let d_par () = dot true !roundnb p dotfile !e;;
-let dot_par () = dot true !roundnb p dotfile !e;;
-let ne_par () = neato true !roundnb p dotfile !e;;
-let tw_par () = twopi true !roundnb p dotfile !e;;
-let ci_par () = circo true !roundnb p dotfile !e;;
-let fd_par () = fdp true !roundnb p dotfile !e;;
-let sf_par () = sfdp true !roundnb p dotfile !e;;
-let pa_par () = patchwork true !roundnb p dotfile !e;;
-let os_par () = osage true !roundnb p dotfile !e;;
-
-let dot () = dot false !roundnb p dotfile !e;;
-let ne () = neato false !roundnb p dotfile !e;;
-let tw () = twopi false !roundnb p dotfile !e;;
-let ci () = circo false !roundnb p dotfile !e;;
-let fd () = fdp false !roundnb p dotfile !e;;
-let sf () = sfdp false !roundnb p dotfile !e;;
-let pa () = patchwork false !roundnb p dotfile !e;;
-let os () = osage false !roundnb p dotfile !e;;
+let d_par () = dot true !round_st_ref.cpt p dotfile !e;;
+let dot_par () = dot true !round_st_ref.cpt p dotfile !e;;
+let ne_par () = neato true !round_st_ref.cpt p dotfile !e;;
+let tw_par () = twopi true !round_st_ref.cpt p dotfile !e;;
+let ci_par () = circo true !round_st_ref.cpt p dotfile !e;;
+let fd_par () = fdp true !round_st_ref.cpt p dotfile !e;;
+let sf_par () = sfdp true !round_st_ref.cpt p dotfile !e;;
+let pa_par () = patchwork true !round_st_ref.cpt p dotfile !e;;
+let os_par () = osage true !round_st_ref.cpt p dotfile !e;;
+
+let dot () = dot false !round_st_ref.cpt p dotfile !e;;
+let ne () = neato false !round_st_ref.cpt p dotfile !e;;
+let tw () = twopi false !round_st_ref.cpt p dotfile !e;;
+let ci () = circo false !round_st_ref.cpt p dotfile !e;;
+let fd () = fdp false !round_st_ref.cpt p dotfile !e;;
+let sf () = sfdp false !round_st_ref.cpt p dotfile !e;;
+let pa () = patchwork false !round_st_ref.cpt p dotfile !e;;
+let os () = osage false !round_st_ref.cpt p dotfile !e;;
(* To change the default dot/graph viewer:
dot_view := ci;;
-*)
+ *)
let dot_view : (unit -> unit) ref =
ref ( (* Try to chose the most sensible default viewer *)
if String.length dotfile > 4 && String.sub dotfile 0 4 = "ring" then ci else
- if Algo.is_directed () then dot else ne)
-
+ if Algo.is_directed () then dot else ne)
+
let d () = !dot_view ()
let sd () = s();!dot_view();;
let bd()= e:=prev !e ; emacs_udate !e; pe();!dot_view();;
+let nr () =
+ let ne = next_round !e in
+ e := ne;
+ store !e.nb; !dot_view ();;
-let nr () = e:=next_round !e; store !e.nb; !dot_view ();;
let pr () =
e:=goto_last_ckpt !e.nb;
- update_round_nb !e;
+ restore_round_nb !e.nb;
!dot_view ();
store !e.nb
-
+
(* I need to overrides those *)
-let u () = undo (); ignore (round !e);;
+(* won't work in semi-auto modes, but the buttons are hided *)
+let u () = undo (); ignore (round true !e);;
let r () =
- r ();
- round_init ();
- ignore (round !e);
+ !e.RdbgEvent.reset();
+ e:=RdbgStdLib.run ~call_hooks:true ();
+ round_reset ();
+ redos := [1];
+ (* ignore (round false !e); *)
(* if the first event is not a round, add it as a check_point *)
- if !ckpt_list = [] then ckpt_list := [!e];;
+ (* if !ckpt_list = [] then *)
+ ckpt_list := [!e];;
(**********************************************************************)
(* Move forward until silence *)
@@ -188,12 +239,12 @@ let goto_silence e = next_cond e is_silent
let silence () = e:=goto_silence !e; !dot_view ();;
let _ = add_doc_entry
- "silence" "unit -> unit" "Move forward until is_silent returns true"
- "sasa" "sasa-rdbg-cmds.ml";
- add_doc_entry
- "is_silent" "RdbgEvent.t -> bool"
- "does the event correspond to a silent configuration? (i.e., no enable node)"
- "sasa" "sasa-rdbg-cmds.ml";;
+ "silence" "unit -> unit" "Move forward until is_silent returns true"
+ "sasa" "sasa-rdbg-cmds.ml";
+ add_doc_entry
+ "is_silent" "RdbgEvent.t -> bool"
+ "does the event correspond to a silent configuration? (i.e., no enable node)"
+ "sasa" "sasa-rdbg-cmds.ml";;
let goto_legitimate e = next_cond e is_legitimate
@@ -216,58 +267,58 @@ let _ =
names; ie we leave only the pid and the action name *)
type s = (string * string * Data.v)
let split_data (l:Data.subst list) : s list * s list * s list =
- let l = List.map (fun (x,v) -> Str.split (Str.regexp "_") x, v) l in
- let rec sortv (enab, other) (x,v) =
- match x with
- | "Enab"::pid::tail -> (pid, String.concat "_" tail,v)::enab, other
- | pid::tail -> enab, (pid,(String.concat "_" tail),v)::other
- | [] -> assert false
- in
- let enab, other = List.fold_left sortv ([],[]) l in
- let acti_names = List.map (fun (pid, n, v) -> pid, n) enab in
- let act, vars =
- List.partition (fun (pid,n, _) -> List.mem (pid,n) acti_names) other
- in
- enab, act, vars
-
-
+ let l = List.map (fun (x,v) -> Str.split (Str.regexp "_") x, v) l in
+ let rec sortv (enab, other) (x,v) =
+ match x with
+ | "Enab"::pid::tail -> (pid, String.concat "_" tail,v)::enab, other
+ | pid::tail -> enab, (pid,(String.concat "_" tail),v)::other
+ | [] -> assert false
+ in
+ let enab, other = List.fold_left sortv ([],[]) l in
+ let acti_names = List.map (fun (pid, n, v) -> pid, n) enab in
+ let act, vars =
+ List.partition (fun (pid,n, _) -> List.mem (pid,n) acti_names) other
+ in
+ enab, act, vars
+
+
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 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
- let _to_string (pid, n, _) = Printf.sprintf "%s_%s" pid n in
- 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 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
- 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%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))))
- leg silent
- )
-
+ let enab, act, vars = split_data e.data 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
+ let _to_string (pid, n, _) = Printf.sprintf "%s_%s" pid n in
+ 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 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
+ (* restore_round_nb e; *)
+ (if short then
+ Printf.sprintf "[round %i, step %i%s] %s %s\n" !round_st_ref.cpt 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%s\n%s%s\n%s%s" !round_st_ref.cpt 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))))
+ leg silent
+ )
+
let print_sasa_event short e =
if e.kind <> Ltop then print_event e else
(
@@ -288,9 +339,9 @@ let spel () = print_sasa_event false !e;;
(* Goto to the next Lustre oracle violation *)
let goto_next_false_oracle e =
next_cond e (fun e -> e.kind = Exit && e.lang = "lustre" &&
- List.mem ("ok", Bool) e.outputs &&
- not (vb "ok" e))
-
+ List.mem ("ok", Bool) e.outputs &&
+ not (vb "ok" e))
+
let viol_string () =
if args.oracles <> [] then (
e:=goto_next_false_oracle !e; !dot_view (); "An oracle has been violated. Cf the .rif file"
@@ -301,8 +352,8 @@ let viol_string () =
let viol () = Printf.printf "%s\n%!" (viol_string ())
let _ = add_doc_entry
- "viol" "unit -> unit" "Move forward until the oracle is violated"
- "sasa" "sasa-rdbg-cmds.ml"
+ "viol" "unit -> unit" "Move forward until the oracle is violated"
+ "sasa" "sasa-rdbg-cmds.ml"
(**********************************************************************)
(* Potential *)
@@ -315,76 +366,96 @@ let potential () =
| _ -> None
let _ = add_doc_entry
- "potential" "unit -> float option" "returns the current potential if available"
- "sasa" "sasa-rdbg-cmds.ml"
+ "potential" "unit -> float option" "returns the current potential if available"
+ "sasa" "sasa-rdbg-cmds.ml"
(**********************************************************************)
(* Perform the checkpointing at rounds! *)
-let _ = check_ref := fun e -> e.nb = 1 || round e;;
+let _ = check_ref := fun e -> e.nb = 1 || round true e;;
(**********************************************************************)
let _ =
- add_doc_entry "d" "unit -> unit" "update the current network with dot" "sasa" "sasa-rdbg-cmds.ml";
- add_doc_entry "ne" "unit -> unit" "update the current network with neato" "sasa" "sasa-rdbg-cmds.ml";
- add_doc_entry "tw" "unit -> unit" "update the current network with twopi" "sasa" "sasa-rdbg-cmds.ml";
- add_doc_entry "ci" "unit -> unit" "update the current network with circo" "sasa" "sasa-rdbg-cmds.ml";
- add_doc_entry "fd" "unit -> unit" "update the current network with fdp" "sasa" "sasa-rdbg-cmds.ml";
- add_doc_entry "sf" "unit -> unit" "update the current network with sfdp" "sasa" "sasa-rdbg-cmds.ml";
- add_doc_entry "pa" "unit -> unit" "update the current network with patchwork" "sasa" "sasa-rdbg-cmds.ml";
- add_doc_entry "os" "unit -> unit" "update the current network with osage" "sasa" "sasa-rdbg-cmds.ml";
+ add_doc_entry "d"
+ "unit -> unit" "update the current network with dot" "sasa" "sasa-rdbg-cmds.ml";
+ add_doc_entry "ne"
+ "unit -> unit" "update the current network with neato" "sasa" "sasa-rdbg-cmds.ml";
+ add_doc_entry "tw"
+ "unit -> unit" "update the current network with twopi" "sasa" "sasa-rdbg-cmds.ml";
+ add_doc_entry "ci"
+ "unit -> unit" "update the current network with circo" "sasa" "sasa-rdbg-cmds.ml";
+ add_doc_entry "fd"
+ "unit -> unit" "update the current network with fdp" "sasa" "sasa-rdbg-cmds.ml";
+ add_doc_entry "sf"
+ "unit -> unit" "update the current network with sfdp" "sasa" "sasa-rdbg-cmds.ml";
+ add_doc_entry "pa"
+ "unit -> unit" "update the current network with patchwork" "sasa" "sasa-rdbg-cmds.ml";
+ add_doc_entry "os"
+ "unit -> unit" "update the current network with osage" "sasa" "sasa-rdbg-cmds.ml";
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 "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";
- add_doc_entry "ne_par" "unit -> unit" "cf ne (for topology with a parent field)" "sasa" "sasa-rdbg-cmds.ml";
- add_doc_entry "tw_par" "unit -> unit" "cf tw (for topology with a parent field)" "sasa" "sasa-rdbg-cmds.ml";
- add_doc_entry "ci_par" "unit -> unit" "cf ci (for topology with a parent field)" "sasa" "sasa-rdbg-cmds.ml";
- add_doc_entry "fd_par" "unit -> unit" "cf fd (for topology with a parent field)" "sasa" "sasa-rdbg-cmds.ml";
- add_doc_entry "sf_par" "unit -> unit" "cf sf (for topology with a parent field)" "sasa" "sasa-rdbg-cmds.ml";
- add_doc_entry "pa_par" "unit -> unit" "cf pa (for topology with a parent field)" "sasa" "sasa-rdbg-cmds.ml";
- add_doc_entry "os_par" "unit -> unit" "cf os (for topology with a parent field)" "sasa" "sasa-rdbg-cmds.ml";
+ "go to the next step and update the network with one of the GraphViz tools" "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";
+ add_doc_entry "ne_par" "unit -> unit" "cf ne (for topology with a parent field)"
+ "sasa" "sasa-rdbg-cmds.ml";
+ add_doc_entry "tw_par" "unit -> unit" "cf tw (for topology with a parent field)"
+ "sasa" "sasa-rdbg-cmds.ml";
+ add_doc_entry "ci_par" "unit -> unit" "cf ci (for topology with a parent field)"
+ "sasa" "sasa-rdbg-cmds.ml";
+ add_doc_entry "fd_par" "unit -> unit" "cf fd (for topology with a parent field)"
+ "sasa" "sasa-rdbg-cmds.ml";
+ add_doc_entry "sf_par" "unit -> unit" "cf sf (for topology with a parent field)"
+ "sasa" "sasa-rdbg-cmds.ml";
+ add_doc_entry "pa_par" "unit -> unit" "cf pa (for topology with a parent field)"
+ "sasa" "sasa-rdbg-cmds.ml";
+ add_doc_entry "os_par" "unit -> unit" "cf os (for topology with a parent field)"
+ "sasa" "sasa-rdbg-cmds.ml";
()
let l () =
l();
- print_string ("
-- sasa commands
- + Display network with GraphViz tools
- d: "^(RdbgMain.doc_msg "d")^"
- ne: "^(RdbgMain.doc_msg "ne")^"
- tw: "^(RdbgMain.doc_msg "tw")^"
- ci: "^(RdbgMain.doc_msg "ci")^"
- fd: "^(RdbgMain.doc_msg "fd")^"
- sf: "^(RdbgMain.doc_msg "sf")^"
- pa: "^(RdbgMain.doc_msg "pa")^"
- os: "^(RdbgMain.doc_msg "os")^"
-
- nb: for algorithms that have a field named 'par', you can try
- of the following (which only draw the parent arcs)
-
- d_par: "^(RdbgMain.doc_msg "d")^" (parent arcs only)
- ne_par: "^(RdbgMain.doc_msg "ne")^" (parent arcs only)
- tw_par: "^(RdbgMain.doc_msg "tw")^" (parent arcs only)
- ci_par: "^(RdbgMain.doc_msg "ci")^" (parent arcs only)
- fd_par: "^(RdbgMain.doc_msg "fd")^" (parent arcs only)
- sf_par: "^(RdbgMain.doc_msg "sf")^" (parent arcs only)
- pa_par: "^(RdbgMain.doc_msg "pa")^" (parent arcs only)
- os_par: "^(RdbgMain.doc_msg "os")^" (parent arcs only)
-
- + Moving commands [*]
- sd: "^(RdbgMain.doc_msg "sd")^"
- nd: "^(RdbgMain.doc_msg "nd")^"
- bd: "^(RdbgMain.doc_msg "bd")^"
- nr: "^(RdbgMain.doc_msg "nr")^"
- pr: "^(RdbgMain.doc_msg "pr")^"
- [*] in order to change the current graph drawing engine, you can use
-the dot_view reference as follows:
- dot_view := ci
+ print_string (
+ "
+ - sasa commands
+ + Display network with GraphViz tools
+ d: "^(RdbgMain.doc_msg "d")^"
+ ne: "^(RdbgMain.doc_msg "ne")^"
+ tw: "^(RdbgMain.doc_msg "tw")^"
+ ci: "^(RdbgMain.doc_msg "ci")^"
+ fd: "^(RdbgMain.doc_msg "fd")^"
+ sf: "^(RdbgMain.doc_msg "sf")^"
+ pa: "^(RdbgMain.doc_msg "pa")^"
+ os: "^(RdbgMain.doc_msg "os")^"
+
+ nb: for algorithms that have a field named 'par', you can try
+ one of the following (which only draw the parent arcs)
+ d_par: "^(RdbgMain.doc_msg "d")^" (parent arcs only)
+ ne_par: "^(RdbgMain.doc_msg "ne")^" (parent arcs only)
+ tw_par: "^(RdbgMain.doc_msg "tw")^" (parent arcs only)
+ ci_par: "^(RdbgMain.doc_msg "ci")^" (parent arcs only)
+ fd_par: "^(RdbgMain.doc_msg "fd")^" (parent arcs only)
+ sf_par: "^(RdbgMain.doc_msg "sf")^" (parent arcs only)
+ pa_par: "^(RdbgMain.doc_msg "pa")^" (parent arcs only)
+ os_par: "^(RdbgMain.doc_msg "os")^" (parent arcs only)
+
+ + Moving commands [*]
+ sd: "^(RdbgMain.doc_msg "sd")^"
+ nd: "^(RdbgMain.doc_msg "nd")^"
+ bd: "^(RdbgMain.doc_msg "bd")^"
+ nr: "^(RdbgMain.doc_msg "nr")^"
+ pr: "^(RdbgMain.doc_msg "pr")^"
+ [*] in order to change the current graph drawing engine, you can use
+ the dot_view reference as follows:
+ dot_view := ci
");;
@@ -393,21 +464,20 @@ the dot_view reference as follows:
let pdf_viewer =
if Sys.command "which zathura" = 0 then "zathura" else
- if Sys.command "which xpdf" = 0 then "xpdf" else
- if Sys.command "which acroread" = 0 then "acroread" else
- if Sys.command "which evince" = 0 then "evince" else (
- Printf.printf "Warning: no pdf viewer is found to visualize %s\n%!" dotfile;
- "ls"
- )
-
+ if Sys.command "which xpdf" = 0 then "xpdf" else
+ if Sys.command "which acroread" = 0 then "acroread" else
+ if Sys.command "which evince" = 0 then "evince" else (
+ Printf.printf "Warning: no pdf viewer is found to visualize %s\n%!" dotfile;
+ "ls"
+ )
+
let graph_view () =
!dot_view ();
let cmd = Printf.sprintf "%s sasa-%s.pdf&" pdf_viewer dotfile in
Printf.printf "%s\n!" cmd;
- ignore(Sys.command cmd);
- ignore(round !e)
+ ignore(Sys.command cmd)
- ;;
+;;
(* let _ = graph_view () *)
let gv = graph_view
@@ -415,13 +485,13 @@ let _ =
add_doc_entry "gv" "unit -> unit"
"launch a pdf viewer of the current network
-in order to change the current graph drawing engine, you can use
-the dot_view reference as follows:
-(rdbg) dot_view := ci;;
-or
-(rdbg) dot_view := fd;;
+ in order to change the current graph drawing engine, you can use
+ the dot_view reference as follows:
+ (rdbg) dot_view := ci;;
+ or
+ (rdbg) dot_view := fd;;
-In order to get the list of graph drawing engine:
-(rdbg) h sasa
-"
+ In order to get the list of graph drawing engine:
+ (rdbg) h sasa
+ "
"sasa" "sasa-rdbg-cmds.ml";
--
GitLab