From 29e7daea2d613f1a3b375934446f7f9b6c489021 Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Fri, 11 Jul 2014 16:59:13 +0200 Subject: DOES NOT WORK AT ALL --- abstract/abs_interp_dynpart.ml | 277 +++++++++++++++++++++-------------------- tests/source/cdrom.scade | 10 +- 2 files changed, 150 insertions(+), 137 deletions(-) diff --git a/abstract/abs_interp_dynpart.ml b/abstract/abs_interp_dynpart.ml index bc0755b..65255ca 100644 --- a/abstract/abs_interp_dynpart.ml +++ b/abstract/abs_interp_dynpart.ml @@ -501,150 +501,156 @@ end = struct let qc = ref None in - (* put true or false conditions into location definition *) - Hashtbl.iter - (fun q (loc : location) -> - let rec iter () = - try - let cond, _ = List.find - (fun (c, _) -> - is_bot (apply_cl loc.v (conslist_of_f c)) - || is_bot (apply_cl loc.v (conslist_of_f (BNot c)))) - (ternary_conds loc.f) - in - let tr = - if is_bot (apply_cl loc.v (conslist_of_f cond)) - then BNot cond - else cond - in - loc.def <- apply_cl loc.def (conslist_of_f tr); - loc.f <- simplify_k [tr] loc.f; - loc.f <- simplify_k (get_root_true loc.f) loc.f; - loc.cl <- conslist_of_f loc.f; - iter() - with Not_found -> () - in iter ()) - e.loc; - - (* find splitting condition *) - let voi = List.map (fun (a, b, c) -> c) e.guarantees in - - Hashtbl.iter - (fun q (loc:location) -> - if loc.depth < e.opt.max_dp_depth then - let cs = ternary_conds loc.f in - List.iter - (fun (c, exprs) -> - let cases_t = apply_cl_all_cases (top e) (conslist_of_f c) in - let cases_f = apply_cl_all_cases (top e) (conslist_of_f (BNot c)) in - let cases = List.mapi (fun i c -> i, c) (cases_t @ cases_f) in - if - List.length - (List.filter - (fun (_, case) -> not (is_bot (meet loc.v case))) - cases) - >= 2 - then - (* calculate which transitions qi -> q stay or are destroyed (approximation) *) - let in_tc = - List.flatten @@ 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 - List.map - (fun (ci, case) -> qi, ci, not (is_bot (meet v case))) - cases) - loc.in_t + if Hashtbl.length e.loc < e.opt.max_dp_width then begin + (* put true or false conditions into location definition *) + Hashtbl.iter + (fun q (loc : location) -> + let rec iter () = + try + let cond, _ = List.find + (fun (c, _) -> + is_bot (apply_cl loc.v (conslist_of_f c)) + || is_bot (apply_cl loc.v (conslist_of_f (BNot c)))) + (ternary_conds loc.f) in - (* calculate which transitions q -> qo stay or are destroyed (approximation) *) - let out_tc = - List.flatten @@ List.map - (fun (ci, case) -> - let v = meet loc.v case in - List.map - (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 qo, ci, not (is_bot w)) - loc.out_t) - cases + let tr = + if is_bot (apply_cl loc.v (conslist_of_f cond)) + then BNot cond + else cond in - (* calculate which cases have a good number of disappearing transitions *) - let fa = - let cs_sc = - List.map + loc.def <- apply_cl loc.def (conslist_of_f tr); + loc.f <- simplify_k [tr] loc.f; + loc.f <- simplify_k (get_root_true loc.f) loc.f; + loc.cl <- conslist_of_f loc.f; + iter() + with Not_found -> () + in iter ()) + e.loc; + + (* find splitting condition *) + let voi = List.map (fun (a, b, c) -> c) e.guarantees in + + Hashtbl.iter + (fun q (loc:location) -> + if loc.depth < e.opt.max_dp_depth then + let cs = ternary_conds loc.f in + List.iter + (fun (c, exprs) -> + let cases_t = apply_cl_all_cases (top e) (conslist_of_f c) in + let cases_f = apply_cl_all_cases (top e) (conslist_of_f (BNot c)) in + let cases = List.mapi (fun i c -> i, c) (cases_t @ cases_f) in + if + List.length + (List.filter + (fun (_, case) -> not (is_bot (meet loc.v case))) + cases) + >= 2 + then + (* calculate which transitions qi -> q stay or are destroyed (approximation) *) + let in_tc = + List.flatten @@ 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 + List.map + (fun (ci, case) -> qi, ci, not (is_bot (meet v case))) + cases) + loc.in_t + in + (* calculate which transitions q -> qo stay or are destroyed (approximation) *) + let out_tc = + List.flatten @@ List.map (fun (ci, case) -> - let a = - List.length - (List.filter (fun (qi, c, a) -> not a && c = ci) in_tc) - in - let b = - List.length - (List.filter (fun (qo, c, a) -> not a && c = ci) out_tc) - in - a + b + a * b) + let v = meet loc.v case in + List.map + (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 qo, ci, not (is_bot w)) + loc.out_t) cases in - 5 * List.fold_left max 0 cs_sc - in - (* calculate which states become inaccessible *) - let fb = - if fa = 0 || List.for_all (fun (_, _, a) -> a) out_tc - then 0 - else - let ff id = (* transition function for new graph *) - if id >= 1000000 then - let case = id - 1000000 in - List.map (fun (qo, _, _) -> qo) - (List.filter (fun (_, c, a) -> c = case && a) out_tc) + (* calculate which cases have a good number of disappearing transitions *) + let fa = + let cs_sc = + List.map + (fun (ci, case) -> + let a = + List.length + (List.filter (fun (qi, c, a) -> not a && c = ci) in_tc) + in + let b = + List.length + (List.filter (fun (qo, c, a) -> not a && c = ci) out_tc) + in + a * b + (if a + b > 0 then 1 else 0)) + cases + in + let a = List.fold_left max 0 cs_sc in + let b = 5 * a in + if a > 0 && b = 0 then 1 else b + in + if fa <> 0 then begin + (* calculate which states become inaccessible *) + let fb = + if List.for_all (fun (_, _, a) -> a) out_tc + then 0 else - let out_t = (Hashtbl.find e.loc id).out_t in - if List.mem loc.id out_t then - (List.map (fun (_, c, _) -> c + 1000000) - (List.filter (fun (qi, _, a) -> qi = id && a) in_tc)) - @ (List.filter ((<>) id) out_t) - else out_t + let ff id = (* transition function for new graph *) + if id >= 1000000 then + let case = id - 1000000 in + List.map (fun (qo, _, _) -> qo) + (List.filter (fun (_, c, a) -> c = case && a) out_tc) + else + let out_t = (Hashtbl.find e.loc id).out_t in + if List.mem loc.id out_t then + (List.map (fun (_, c, _) -> c + 1000000) + (List.filter (fun (qi, _, a) -> qi = id && a) in_tc)) + @ (List.filter ((<>) id) out_t) + else out_t + in + let memo = Hashtbl.create 12 in + let rec do_x id = + if not (Hashtbl.mem memo id) then begin + Hashtbl.add memo id (); + List.iter do_x (ff id) + end + in + Hashtbl.iter (fun i loc2 -> if loc2.is_init && i <> loc.id then do_x i) e.loc; + if loc.is_init then List.iter (fun (ci, _) -> do_x (ci+1000000)) cases; + let disappear_count = (Hashtbl.length e.loc + List.length cases) - (Hashtbl.length memo) in + 21 * disappear_count in - let memo = Hashtbl.create 12 in - let rec do_x id = - if not (Hashtbl.mem memo id) then begin - Hashtbl.add memo id (); - List.iter do_x (ff id) - end + (* calculate in/out count, weighted by changing guarantees *) + let fc = + 0 * (2 * List.length loc.out_t + List.length loc.in_t) in - Hashtbl.iter (fun i loc2 -> if loc2.is_init && i <> loc.id then do_x i) e.loc; - if loc.is_init then List.iter (fun (ci, _) -> do_x (ci+1000000)) cases; - let disappear_count = (Hashtbl.length e.loc + List.length cases) - (Hashtbl.length memo) in - 21 * disappear_count - in - (* calculate number of VOI (variables of interest) that are affected *) - let fc = - let vlist = refd_evars_of_f exprs in - 10 * List.length - (List.filter (fun v -> List.mem v vlist) voi) in - (* give score to split *) - let fd = 2 * List.length loc.out_t + List.length loc.in_t in - let score = - if fa = 0 then 0 else - fa + fb + fc + fd - in - Format.printf " %5d + %5d + %5d + %5d = %5d (q%d)@." fa fb fc fd score loc.id; - if score > 0 && - match !qc with - | None -> true - | Some (s, _, _, _, _) -> score >= s - then - qc := Some(score, q, c, cases_t, cases_f) - ) - cs - ) - e.loc; + (* calculate number of VOI (variables of interest) that are affected *) + let fd = + let vlist = refd_evars_of_f exprs in + 3 * List.length + (List.filter (fun v -> List.mem v vlist) voi) in + (* give score to split *) + let score = + if fa = 0 then 0 else + fa + fb + fc + fd + in + Format.printf " %5d + %5d + %5d + %5d = %5d (q%d)@." fa fb fc fd score loc.id; + if score > 0 && + match !qc with + | None -> true + | Some (s, _, _, _, _) -> score >= s + then + qc := Some(score, q, c, cases_t, cases_f) + end) + cs + ) + e.loc; - if Hashtbl.length e.loc < e.opt.max_dp_width then match !qc with | None -> Format.printf "@.Found no more possible refinement.@.@." @@ -673,6 +679,7 @@ end = struct List.iter (handle_case (BNot c)) cases_f; iter (n+1) + end in iter 0; (* Check guarantees *) diff --git a/tests/source/cdrom.scade b/tests/source/cdrom.scade index 92438c3..03501d5 100644 --- a/tests/source/cdrom.scade +++ b/tests/source/cdrom.scade @@ -1,5 +1,6 @@ -node cdrom(speed: int) returns (plus, minus, error: bool) +node cdrom(probe speed: int) returns (plus, minus, error: bool) var ps, count: int; + _a, _b, _la, _lb: bool; let ps = 0 -> pre speed; @@ -11,9 +12,14 @@ let plus = (ps <= 9); minus = (ps >= 11); + _a = speed < 8; + _b = speed > 12; + _la = true -> pre _a; + _lb = false -> pre _b; + count = if speed < 8 or speed > 12 then (0 -> pre count) + 1 else 0; error = (count >= 15); - guarantee g: not error and (true -> not pre error); + guarantee g: not error; tel -- cgit v1.2.3