diff options
| -rw-r--r-- | .gitignore | 1 | ||||
| -rw-r--r-- | abstract/abs_interp_dynpart.ml | 139 | ||||
| -rw-r--r-- | abstract/abs_interp_edd.ml | 4 | ||||
| -rw-r--r-- | abstract/transform.ml | 14 | ||||
| -rw-r--r-- | tests/source/jeannet.scade | 16 |
5 files changed, 133 insertions, 41 deletions
@@ -18,3 +18,4 @@ analyze # Plots graphs/* +graphs2/* diff --git a/abstract/abs_interp_dynpart.ml b/abstract/abs_interp_dynpart.ml index 32ed890..006854e 100644 --- a/abstract/abs_interp_dynpart.ml +++ b/abstract/abs_interp_dynpart.ml @@ -35,6 +35,9 @@ end = struct mutable out_t : int list; mutable in_t : int list; + + mutable verif_g : id list; + mutable violate_g : id list; } type env = { @@ -230,10 +233,12 @@ end = struct cl = conslist_of_f rstf; in_c = 0; - v = (ED.top ve.evars, ND.bottom ve.nvars); + v = bottom env; out_t = []; in_t = []; + verif_g = []; + violate_g = []; }; Hashtbl.add env.loc 1 { @@ -246,10 +251,12 @@ end = struct cl = conslist_of_f nrstf; in_c = 0; - v = (ED.top ve.evars, ND.bottom ve.nvars); + v = bottom env; out_t = []; in_t = []; + verif_g = []; + violate_g = []; }; env @@ -321,13 +328,33 @@ end = struct (fun id loc -> Format.printf "@."; Format.printf "q%d (depth = %d):@. D: @[<v 2>%a@]@." id loc.depth print_v loc.def; - (*Format.printf " F: (%a)@." Formula_printer.print_expr loc.f;*) + Format.printf " F: (%a)@." Formula_printer.print_expr loc.f; Format.printf " V: %a@." print_v loc.v; Format.printf " -> @[<hov>[%a]@]@." (print_list (fun fmt i -> Format.fprintf fmt "q%d" i) ", ") loc.out_t; ) e.loc + let dump_graphwiz_trans_graph e file = + let o = open_out file in + let fmt = Format.formatter_of_out_channel o in + Format.fprintf fmt "digraph G{@[<v 4>@ "; + + Hashtbl.iter + (fun id loc -> + if loc.is_init then + Format.fprintf fmt "q%d [shape=doublecircle, label=\"q%d [%a]\"];@ " + id id (print_list Format.pp_print_string ", ") loc.violate_g + else + Format.fprintf fmt "q%d [label=\"q%d [%a]\"];@ " + id id (print_list Format.pp_print_string ", ") loc.violate_g; + List.iter (fun v -> Format.fprintf fmt "q%d -> q%d;@ " id v) loc.out_t) + e.loc; + + Format.fprintf fmt "@]@.}@."; + close_out o + + (* chaotic_iter : env -> unit @@ -432,6 +459,18 @@ end = struct e.loc; List.iter (Hashtbl.remove e.loc) !useless; + (* check which states verify/violate guarantees *) + Hashtbl.iter + (fun _ loc -> + let verif, violate = List.partition + (fun (_, f) -> + is_bot (apply_cl loc.v (conslist_of_f f))) + e.guarantees + in + loc.verif_g <- List.map fst verif; + loc.violate_g <- List.map fst violate) + e.loc; + print_locs e @@ -443,6 +482,7 @@ end = struct Format.printf "@.--------------@.Refinement #%d@." n; chaotic_iter e; + dump_graphwiz_trans_graph e (Format.sprintf "/tmp/part%03d.dot" n); let qc = ref None in @@ -474,7 +514,7 @@ end = struct (* find splitting condition *) Hashtbl.iter (fun q (loc:location) -> - if !qc = None && loc.depth < e.opt.max_dp_depth then + if loc.depth < e.opt.max_dp_depth then let cs = ternary_conds loc.f in List.iter (fun c -> @@ -487,31 +527,46 @@ end = struct (fun case -> not (is_bot (meet loc.v case))) cases) >= 2 - && - (List.exists - (fun qi -> - let loci = Hashtbl.find e.loc qi in - let v = apply_cl - (meet (pass_cycle e.ve loci.v) loc.def) - loc.cl in - List.exists - (fun case -> is_bot (meet v case)) - cases) - loc.in_t - || List.exists - (fun case -> - let v = meet loc.v case in - List.exists - (fun qo -> - let loco = Hashtbl.find e.loc qo in - let w = apply_cl - (meet (pass_cycle e.ve v) loco.def) - loco.cl in - is_bot w) - loc.out_t) - cases) then - qc := Some(q, c, cases_t, cases_f) + let score = + let w1 = List.fold_left (+.) 0. + (List.map + (fun qi -> + let loci = Hashtbl.find e.loc qi in + let v = apply_cl + (meet (pass_cycle e.ve loci.v) loc.def) + loc.cl in + let n = List.length @@ List.filter + (fun case -> is_bot (meet v case)) + cases + in if n > 0 then 1. else 0.) + loc.in_t) + in + let w2 = List.fold_left (+.) 0. + (List.map + (fun qo -> + let loco = Hashtbl.find e.loc qo in + let n = List.length @@ List.filter + (fun case -> + let v = meet loc.v case in + let w = apply_cl + (meet (pass_cycle e.ve v) loco.def) + loco.cl + in is_bot w) + cases + in if n > 0 then 1. else 0.) + loc.out_t) + in + ((w1 /. 1. (*(float_of_int (List.length loc.in_t))*)) + +. (w2 /. 1. (*(float_of_int (List.length loc.out_t))*))) + /. (float_of_int (List.length cases)) + in + if + match !qc with + | None -> true + | Some (s, _, _, _, _) -> score >= s + then + qc := Some(score, q, c, cases_t, cases_f) ) cs ) @@ -521,7 +576,7 @@ end = struct match !qc with | None -> Format.printf "@.Found no more possible refinement.@.@." - | Some (q, c, cases_t, cases_f) -> + | Some (score, q, c, cases_t, cases_f) -> Format.printf "@.Refine q%d : @[<v 2>[ %a ]@]@." q (print_list print_v ", ") (cases_t@cases_f); @@ -556,9 +611,9 @@ end = struct id Formula_printer.print_conslist cl; let violate = ref [] in Hashtbl.iter - (fun id loc -> - if not (is_bot (apply_cl loc.v cl)) then - violate := id::!violate) + (fun lid loc -> + if List.mem id loc.violate_g then + violate := lid::!violate) e.loc; if !violate = [] then Format.printf "OK" @@ -571,9 +626,27 @@ end = struct Format.printf "Guarantee @[<v 0>"; List.iter check_guarantee e.guarantees; Format.printf "@]@." + end; + + (* Examine probes *) + if List.exists (fun (p, _, _) -> p) e.ve.all_vars then begin + let final = + Hashtbl.fold + (fun _ loc v -> join v loc.v) + e.loc (bottom e) in + + Format.printf "Probes: @[<v 0>"; + List.iter (fun (p, id, ty) -> + if p then match ty with + | TInt | TReal -> + Format.printf "%a ∊ %a@ " Formula_printer.print_id id + ND.print_itv (ND.project (snd final) id) + | TEnum _ -> Format.printf "%a : enum variable@ " + Formula_printer.print_id id) + e.ve.all_vars; + Format.printf "@]@." end - end diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml index 23d4734..bff8e2b 100644 --- a/abstract/abs_interp_edd.ml +++ b/abstract/abs_interp_edd.ml @@ -971,9 +971,9 @@ end = struct List.iter (fun (p, id, ty) -> if p then match ty with | TInt | TReal -> - Format.printf "%a ∊ %a@." Formula_printer.print_id id + Format.printf "%a ∊ %a@ " Formula_printer.print_id id ND.print_itv (ND.project final_flat id) - | TEnum _ -> Format.printf "%a : enum variable@." + | TEnum _ -> Format.printf "%a : enum variable@ " Formula_printer.print_id id) e.ve.all_vars; Format.printf "@]@." diff --git a/abstract/transform.ml b/abstract/transform.ml index 0144637..5fe4ed1 100644 --- a/abstract/transform.ml +++ b/abstract/transform.ml @@ -442,12 +442,14 @@ let rec f_of_scope active td (node, prefix, eqs) (clock_scope, rst_exprs as cs) (must_reset_c cr (fun _ -> false)) (BEnumCons(E_EQ, nstv, EItem st.st_name)) | (c, (target, l), rst)::q -> - f_ternary - (f_of_expr td (node, prefix, clock_scope) c) - (f_and - (BEnumCons(E_EQ, nstv, EItem target)) - (must_reset_c cr (fun i -> rst && i = target))) - (aux q) + let c = f_of_expr td (node, prefix, clock_scope) c in + let b1 = + f_and + (BEnumCons(E_EQ, nstv, EItem target)) + (must_reset_c cr (fun i -> rst && i = target)) + in + let b2 = aux q in + f_ternary c b1 b2 in let trans_code = must_reset_c cnr (fun _ -> false) in let trans_code = f_and trans_code (aux st.until) in diff --git a/tests/source/jeannet.scade b/tests/source/jeannet.scade new file mode 100644 index 0000000..9fca060 --- /dev/null +++ b/tests/source/jeannet.scade @@ -0,0 +1,16 @@ +node test() returns(x, y, probe z: int; a, b: bool) +var px, py: int; +let + a = false -> pre b; + b = true -> not pre a; + + px = pre x; + py = pre y; + + x = 0 -> (if a = b then px + 1 else px); + y = 0 -> (if a = b then py else py + 1); + + z = x - y; + + guarantee g1: x >= y; +tel |