Skip to content
Snippets Groups Projects
Commit 7cd70503 authored by erwan's avatar erwan
Browse files

Test: add a print_sasa_event and use it by default

parent e7e48454
No related branches found
No related tags found
No related merge requests found
......@@ -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
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment