summaryrefslogtreecommitdiff
path: root/abstract
diff options
context:
space:
mode:
Diffstat (limited to 'abstract')
-rw-r--r--abstract/abs_interp_dynpart.ml139
-rw-r--r--abstract/abs_interp_edd.ml4
-rw-r--r--abstract/transform.ml14
3 files changed, 116 insertions, 41 deletions
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-21 16:55:03 +0000