diff --git a/test/my-rdbg-tuning.ml b/test/my-rdbg-tuning.ml
index 7254788330bdcfde26298023777f3dd09361bcb7..f495c1de02d05143018cb015c50f78a1a3255c25 100644
--- a/test/my-rdbg-tuning.ml
+++ b/test/my-rdbg-tuning.ml
@@ -32,19 +32,78 @@ let emacs_udate e =
hl_atoms si_list
with
Match_failure _ -> ()
-
-let _ = time_travel true;;
+
+
+(**********************************************************************)
+(* implement an undo command *)
+let redos = ref [1];;
+let store i = redos := i::!redos;;
+
+(**********************************************************************)
+(**********************************************************************)
+(* print_event tuning *)
+
+(* split the vars into returns (the enab vars, the activated vars,
+ the other vars) nb: in the "Enab" prefix is removed from enab vars
+ 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 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 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 vars = List.rev vars in
+ Printf.printf "[%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 _ =
+ del_hook "print_event";
+ add_hook "print_event" print_sasa_event
+
+(**********************************************************************)
+
+let _ = time_travel true;;
let e = ref (RdbgStdLib.run());;
-let s () = e:=step !e; ignore(emacs_udate !e);;
-let si i = e:=stepi !e i; ignore(emacs_udate !e);;
-let n () = e:=next !e; ignore(emacs_udate !e);;
-let ni i = e:= nexti !e i;emacs_udate !e;;
-let g i = e:= goto !e i;emacs_udate !e;;
-let b () = e:= back !e ;emacs_udate !e;;
-let bi i = e:= backi !e i;emacs_udate !e;;
-let r () = !e.Event.reset(); e:=RdbgStdLib.run();emacs_udate !e;;
-let c () = e:= continue !e;emacs_udate !e;;
-let cb () = e:= rev !e;emacs_udate !e;;
+
+
+let s () = e:=step !e; emacs_udate !e; store !e.nb;;
+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; redos := [1];;
+let c () = e:= continue !e;emacs_udate !e; store !e.nb;;
+let cb () = e:= rev !e;emacs_udate !e; store !e.nb;;
+let undo () =
+ match !redos with
+ | _::i::t -> redos := i::t; e:=goto !e i;emacs_udate !e
+ | _ -> e:=goto !e 1; emacs_udate !e
+
+let u = undo
(**********************************************************************)
open Callgraph;;
@@ -108,6 +167,7 @@ Here is the list of rdbg Level 0 commands:
l: print this list of L0 commands
i: print information relative to the current session parameters
r: restart
+ u: undo the last move
q: quit rdbg
";;
@@ -122,7 +182,7 @@ Here is the list of rdbg Level 0 commands:
let p = Topology.read dotfile;;
(* shortcuts for dot viewer *)
-let d () = dot p dotfile !e;;
+let dot () = dot p dotfile !e;;
let ne () = neato p dotfile !e;;
let tw () = twopi p dotfile !e;;
let ci () = circo p dotfile !e;;
@@ -138,8 +198,9 @@ let os () = osage p dotfile !e;;
let dot_view : (unit -> unit) ref =
ref ( (* choosing a reasonable default viewer *)
if String.length dotfile > 4 && String.sub dotfile 0 4 = "ring" then ci else
- if Algo.is_directed () then d else ne)
-
+ if Algo.is_directed () then dot else ne)
+
+let d = !dot_view
(* Move forward until convergence, i.e., when no data changes *)
let rec go () =
@@ -210,53 +271,12 @@ 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 ();;
-(**********************************************************************)
-(* print_event tuning *)
-
-(* split the vars into returns (the enab vars, the activated vars,
- the other vars) nb: in the "Enab" prefix is removed from enab vars
- 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 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 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 vars = List.rev vars in
- Printf.printf "[%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))
-
+(* shortcuts to the default and sasa event printers *)
let pe () = print_event !e;;
let spe () = print_sasa_event !e;;
-let _ =
- del_hook "print_event";
- add_hook "print_event" print_sasa_event
(**********************************************************************)
-(* Goto to the next oracle violation *)
+(* 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 &&
@@ -305,7 +325,7 @@ let pdf_viewer =
if Sys.command "which evince" = 0 then "evince" else
failwith "No pdf viewer is found"
-let _ =
+let _ =
!dot_view ();
let cmd = Printf.sprintf "%s sasa-%s.pdf&" pdf_viewer dotfile in
Printf.printf "%s\n!" cmd;