Update: some enhancements in the rdbg integration

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;