diff --git a/test/my-rdbg-tuning.ml b/test/my-rdbg-tuning.ml index fa7e9df817be0a06d91e1543b993188d8f79965a..7254788330bdcfde26298023777f3dd09361bcb7 100644 --- a/test/my-rdbg-tuning.ml +++ b/test/my-rdbg-tuning.ml @@ -210,6 +210,51 @@ 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)) + +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 *) let goto_next_false_oracle e = @@ -242,8 +287,8 @@ let l () = sd: go to the next step and display the network with one of the GraphViz tools (*) nd: go to the next event and display the network bd: go to the previous event and display the network - rd: go to the next round and display the network - pd: go to the previous round and display the network + nd: go to the next round and display the network + pr: go to the previous round and display the network (*) In order to change the current graph drawing engine, you can use the dot_view command as follows: dot_view := ci