diff --git a/test/async-unison/async_unison_oracle.ml b/test/async-unison/async_unison_oracle.ml index a55a7d28b3e1be383a656eccdc4bf0946a47c7b6..500a182750dfd1e2688c17dab666a05f744c1df5 100644 --- a/test/async-unison/async_unison_oracle.ml +++ b/test/async-unison/async_unison_oracle.ml @@ -11,14 +11,14 @@ let (get_enab: sl -> sl * sl) = let is_state_var vname = String.sub vname 0 5= "Enab_" in List.partition (fun (n,v) -> is_state_var n) sl -let (get_states_enab_acti: Event.t -> sl * sl * sl) = fun e -> +let (get_states_enab_acti: RdbgEvent.t -> sl * sl * sl) = fun e -> let sl = e.data in let states, sl = get_states sl in let enab, acti = get_enab sl in states, enab, acti open Topology -let (is_stable : Event.t -> bool) = fun e -> +let (is_stable : RdbgEvent.t -> bool) = fun e -> let states, _, _ = get_states_enab_acti e in let pidl = List.map (fun n -> n.id) p.nodes in let get_val p = @@ -80,7 +80,7 @@ let go () = assert (!rn < diameter * n ); was_stable := true ); - try aux () with Event.End _ -> !rn + try aux () with RdbgEvent.End _ -> !rn in time aux () diff --git a/test/my-rdbg-tuning.ml b/test/my-rdbg-tuning.ml index 9d47086b892a29704bbcafeca1c6f6d9e092db37..161b8cf829b38ee468520bc3ef8d66b4eab28a95 100644 --- a/test/my-rdbg-tuning.ml +++ b/test/my-rdbg-tuning.ml @@ -62,8 +62,7 @@ let split_data (l:Data.subst list) : s list * s list * s list = let only_true l = List.filter (fun (_,_, v) -> v = B true) l (* Only print the active process values *) -let print_sasa_event e = - if e.kind <> Ltop then print_event e else +let str_of_sasa_event e = let enab, act, vars = split_data e.data in (* let enab = only_true enab in *) let act = only_true act in @@ -74,16 +73,25 @@ let print_sasa_event e = Printf.sprintf "%s_%s=%s" pid n (Data.val_to_string string_of_float v) in let vars = List.rev vars in - Printf.printf "[%i%s] %s\n%!" e.step + Printf.sprintf "[%i%s] %s\n" e.step (if e.step <> e.nb then (":" ^ (string_of_int e.nb)) else "") (String.concat " " (List.map to_string_var vars)) +let print_sasa_event e = + if e.kind <> Ltop then print_event e else + ( + print_string (str_of_sasa_event e); + flush stdout + ) + let _ = del_hook "print_event"; add_hook "print_event" print_sasa_event (**********************************************************************) (* handy short-cuts *) +let roundnb = ref 0 +let roundtbl = Hashtbl.create 1 let _ = time_travel true;; let e = ref (RdbgStdLib.run());; @@ -92,11 +100,19 @@ let si i = e:=stepi !e i; emacs_udate !e; store !e.nb;; let n () = e:=next !e ; emacs_udate !e; store !e.nb;; let ni i = e:=nexti !e i; emacs_udate !e; store !e.nb;; let g i = e:=goto !e i; emacs_udate !e; store !e.nb;; -let b () = e:=back !e ; emacs_udate !e; store !e.nb;; -let bi i = e:=backi !e i; emacs_udate !e; store !e.nb;; -let r () = !e.Event.reset(); e:=RdbgStdLib.run();emacs_udate !e; store !e.nb;; +let b () = + e:=back !e; + roundnb := Hashtbl.find roundtbl !e.nb; + emacs_udate !e; store !e.nb;; +let bi i = e:=backi !e i; roundnb := Hashtbl.find roundtbl !e.nb; + emacs_udate !e; store !e.nb;; +let r () = !e.RdbgEvent.reset(); e:=RdbgStdLib.run(); + roundnb := 1; + Hashtbl.clear roundtbl; + emacs_udate !e; store !e.nb;; let c () = e:= continue !e;emacs_udate !e; store !e.nb;; -let cb () = e:= rev !e;emacs_udate !e; store !e.nb;; +let cb () = e:= rev !e;roundnb := Hashtbl.find roundtbl !e.nb; + emacs_udate !e; store !e.nb;; let fc predicate = e := next_np !e; while not (predicate ()) do e := next_np !e; done; get_hook "print_event" !e; @@ -105,13 +121,16 @@ let fc predicate = let bc predicate = e := back !e; while not (predicate ()) do e := back !e; done; get_hook "print_event" !e; + roundnb := Hashtbl.find roundtbl !e.nb; emacs_udate !e; store !e.nb;; let sinfo () = match !e.sinfo with Some si -> si() | None -> failwith "no source info";; let undo () = match !redos with - | _::i::t -> redos := i::t; e:=goto !e i;emacs_udate !e + | _::i::t -> + redos := i::t; e:=goto !e i;emacs_udate !e; + roundnb := Hashtbl.find roundtbl !e.nb; | _ -> e:=goto !e 1; emacs_udate !e ;; let u = undo ;; @@ -201,6 +220,10 @@ let blist () = !breakpoints;; let nm str = e:= next_match !e str ;; let pm str = e:=previous_match !e str ;; +let next_cond e c = + let e = next_cond e c in + store e.nb; + e (* go to the exit of the current event *) let exit () = @@ -331,9 +354,12 @@ let verbose = ref false let last_round = ref 0 let mask = ref [] (* nodes we look the activation of *) -let (round : Event.t -> bool) = + + +(* called at each event via the time-travel hook *) +let (round : RdbgEvent.t -> bool) = fun e -> - e.kind = Ltop && + e.kind = Ltop && let (pl : process list) = get_processes e in let rm_me = get_removable pl in if !verbose then ( @@ -363,14 +389,22 @@ let (round : Event.t -> bool) = flush stdout ); pidl - ) + ); + try roundnb := Hashtbl.find roundtbl e.nb + with _ -> ( + incr roundnb; + Hashtbl.add roundtbl e.nb !roundnb; + ) ); res (* go to next and previous rounds *) let next_round e = next_cond e round;; let nr () = e:=next_round !e; !dot_view ();; -let pr () = e:=goto_last_ckpt !e.nb; !dot_view ();; +let pr () = + e:=goto_last_ckpt !e.nb; + roundnb := Hashtbl.find roundtbl !e.nb; + !dot_view ();; (* shortcuts to the default and sasa event printers *) let pe () = print_event !e;; @@ -482,12 +516,12 @@ let pdf_viewer = "ls" ) -let _ = +let graph_view () = !dot_view (); let cmd = Printf.sprintf "%s sasa-%s.pdf&" pdf_viewer dotfile in Printf.printf "%s\n!" cmd; - Unix.sleep 1; ignore(Sys.command cmd); - round !e + ignore(round !e) ;; +let _ = graph_view () diff --git a/test/rdbg-utils/dot.ml b/test/rdbg-utils/dot.ml index a6aa03c920a832cfaa15227a4a4a765c193a02d8..f26d190f957a1eef99af10e7726cae5b19e59271 100644 --- a/test/rdbg-utils/dot.ml +++ b/test/rdbg-utils/dot.ml @@ -3,7 +3,7 @@ open Graph open Graph.Dot_ast open Data -open Event +open RdbgEvent open Sasacore open Topology @@ -13,7 +13,7 @@ type process = { vars: (string * Data.v) list (* pid local vars*) } -let (is_parent: string -> string -> int -> Event.t -> bool) = +let (is_parent: string -> string -> int -> RdbgEvent.t -> bool) = fun par_var a i e -> (* XXX marche ssi une variable s'appelle par! je devrais au moins generaliser avec l'existence @@ -25,7 +25,7 @@ let (is_parent: string -> string -> int -> Event.t -> bool) = | _ -> false -let (get_processes : Event.t -> process list) = +let (get_processes : RdbgEvent.t -> process list) = fun e -> (* if e.kind <> Ltop then ( print_string "dot should be called from Ltop event\n"; @@ -187,7 +187,7 @@ subgraph undir {\n\t edge [dir=none]\n%s} " trans_dir_str trans_undir_str nodes_decl trans_str; flush oc; close_out oc; - if Sys.command (Printf.sprintf "%s -Tpdf sasa-%s -o sasa-%s.pdf" engine f f) > 0 + if Sys.command (Printf.sprintf "%s -Tpdf sasa-%s -o sasa-%s.pdf&" engine f f) > 0 then ( flush stdout