summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--abstract/abs_interp.ml6
-rw-r--r--abstract/abs_interp_dynpart.ml176
-rw-r--r--abstract/abs_interp_edd.ml10
-rw-r--r--abstract/formula.ml17
-rw-r--r--abstract/transform.ml7
-rw-r--r--abstract/varenv.ml6
-rw-r--r--tests/source/cdrom.scade19
7 files changed, 178 insertions, 63 deletions
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index 2597a63..b5fc684 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -171,7 +171,7 @@ end = struct
(* program expressions *)
cl : conslist;
- guarantees : (id * bool_expr) list;
+ guarantees : (id * bool_expr * id) list;
(* abstract interpretation *)
cycle : (id * id * typ) list; (* s'(x) = s(y) *)
@@ -283,7 +283,7 @@ end = struct
let guarantees = Transform.guarantees_of_prog rp in
Format.printf "Guarantees:@.";
- List.iter (fun (id, f) ->
+ List.iter (fun (id, f, _) ->
Format.printf " %s: %a@." id Formula_printer.print_expr f)
guarantees;
Format.printf "@.";
@@ -433,7 +433,7 @@ end = struct
Format.printf "Accessible: %a@." print_dd final;
- let check_guarantee (id, f) =
+ let check_guarantee (id, f, _) =
let cl = Formula.conslist_of_f f in
Format.printf "@[<hv 4>%s:@ %a ⇒ ⊥ @ "
id Formula_printer.print_conslist cl;
diff --git a/abstract/abs_interp_dynpart.ml b/abstract/abs_interp_dynpart.ml
index 006854e..bc0755b 100644
--- a/abstract/abs_interp_dynpart.ml
+++ b/abstract/abs_interp_dynpart.ml
@@ -48,7 +48,7 @@ end = struct
(* program expressions *)
f : bool_expr;
- guarantees : (id * bool_expr) list;
+ guarantees : (id * bool_expr * id) list;
(* data *)
loc : (int, location) Hashtbl.t;
@@ -168,7 +168,7 @@ end = struct
Format.printf "Complete formula:@.%a@.@." Formula_printer.print_expr f;
let facts = get_root_true f in
- let f, rp, _ = List.fold_left
+ let f, rp, repls = List.fold_left
(fun (f, (rp : rooted_prog), repls) eq ->
match eq with
| BEnumCons(E_EQ, a, EIdent b)
@@ -190,7 +190,7 @@ end = struct
let rp =
{ rp with all_vars =
List.filter (fun (_, id, _) -> id <> repl) rp.all_vars } in
- let repls = (repl, keep)::
+ let repls = [repl, keep; "L"^repl, "L"^keep]@
(List.map (fun (r, k) -> r, if k = repl then keep else k) repls) in
f, rp, repls
end
@@ -203,8 +203,11 @@ end = struct
Formula_printer.print_expr f;
let guarantees = Transform.guarantees_of_prog rp in
+ let guarantees = List.map
+ (fun (id, f, v) -> id, formula_replace_evars repls f, v)
+ guarantees in
Format.printf "Guarantees:@.";
- List.iter (fun (id, f) ->
+ List.iter (fun (id, f, _) ->
Format.printf " %s: %a@." id Formula_printer.print_expr f)
guarantees;
Format.printf "@.";
@@ -266,7 +269,7 @@ end = struct
*)
let rec ternary_conds = function
| BAnd(a, b) -> ternary_conds a @ ternary_conds b
- | BTernary(c, a, b) -> [c]
+ | BTernary(c, a, b) as x -> [c, x]
| _ -> []
(*
@@ -328,7 +331,7 @@ 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;
@@ -338,20 +341,30 @@ end = struct
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>@ ";
+ Format.fprintf fmt "digraph G{@.";
Hashtbl.iter
(fun id loc ->
if loc.is_init then
- Format.fprintf fmt "q%d [shape=doublecircle, label=\"q%d [%a]\"];@ "
+ 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]\"];@ "
+ 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)
+ let n1 = List.length loc.violate_g in
+ List.iter
+ (fun v ->
+ let n2 = List.length (Hashtbl.find e.loc v).violate_g in
+ let c, w =
+ if n2 > n1 then "#770000", 1
+ else "black", 2
+ in
+ Format.fprintf fmt " q%d -> q%d [color = \"%s\", weight = %d];@."
+ id v c w)
+ loc.out_t)
e.loc;
- Format.fprintf fmt "@]@.}@.";
+ Format.fprintf fmt "}@.";
close_out o
@@ -376,7 +389,7 @@ end = struct
loc.v <- bottom e)
e.loc;
- print_locs_defs e;
+ (*print_locs_defs e;*)
(* Iterate *)
let it_counter = ref 0 in
@@ -413,7 +426,7 @@ end = struct
else iter (n+1) j
in
let y = iter 0 start in
- let z = fix eq_v f y in
+ let z = f y in
let u = pass_cycle e.ve z in
if e.opt.verbose_ci then
@@ -463,15 +476,17 @@ end = struct
Hashtbl.iter
(fun _ loc ->
let verif, violate = List.partition
- (fun (_, f) ->
+ (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)
+ loc.verif_g <- List.map (fun (a, b, c) -> a) verif;
+ loc.violate_g <- List.map (fun (a, b, c) -> a) violate)
e.loc;
- print_locs e
+ print_locs e;
+
+ ()
@@ -491,8 +506,8 @@ end = struct
(fun q (loc : location) ->
let rec iter () =
try
- let cond = List.find
- (fun c ->
+ 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)
@@ -512,56 +527,113 @@ end = struct
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 ->
+ (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 = cases_t @ cases_f 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)))
+ (fun (_, case) -> not (is_bot (meet loc.v case)))
cases)
>= 2
then
- 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
+ (* 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 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 is_bot w)
- cases
- in if n > 0 then 1. else 0.)
- loc.out_t)
+ in qo, ci, not (is_bot w))
+ loc.out_t)
+ cases
+ in
+ (* 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 + a * b)
+ cases
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))
+ 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)
+ 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
+ (* 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
- if
+ 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
@@ -604,7 +676,7 @@ end = struct
in iter 0;
(* Check guarantees *)
- let check_guarantee (id, f) =
+ let check_guarantee (id, f, _) =
Format.printf "@[<v 4>";
let cl = Formula.conslist_of_f f in
Format.printf "%s:@ %a ⇒ ⊥ @ "
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index bff8e2b..31fe5aa 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -589,7 +589,7 @@ end = struct
(* program expressions *)
init_cl : conslist;
cl : conslist;
- guarantees : (id * bool_expr) list;
+ guarantees : (id * bool_expr * id) list;
}
@@ -801,7 +801,7 @@ end = struct
let rp =
{ rp with all_vars =
List.filter (fun (_, id, _) -> id <> repl) rp.all_vars } in
- let repls = (repl, keep; "L"^repl, "L"^keep)::
+ let repls = [repl, keep; "L"^repl, "L"^keep]@
(List.map
(fun (r, k) -> r,
if k = repl then keep else
@@ -829,10 +829,10 @@ end = struct
let guarantees = Transform.guarantees_of_prog rp in
let guarantees = List.map
- (fun (id, f) -> id, formula_replace_evars repls f)
+ (fun (id, f, v) -> id, formula_replace_evars repls f, v)
guarantees in
Format.printf "Guarantees:@.";
- List.iter (fun (id, f) ->
+ List.iter (fun (id, f, _) ->
Format.printf " %s: %a@." id Formula_printer.print_expr f)
guarantees;
Format.printf "@.";
@@ -936,7 +936,7 @@ end = struct
Format.printf "@.Final:@.@[<hov>%a@]@." edd_print final;
(* Check guarantees *)
- let check_guarantee (id, f) =
+ let check_guarantee (id, f, _) =
let cl = Formula.conslist_of_f f in
Format.printf "@[<hv 4>%s:@ %a ⇒ ⊥ @ "
id Formula_printer.print_conslist cl;
diff --git a/abstract/formula.ml b/abstract/formula.ml
index f2a3bd1..650f8f4 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -76,8 +76,9 @@ let f_or a b =
let f_ternary c a b =
if is_true c then a
else if is_false c then b
- else
- BTernary(c, a, b)
+ else if is_true a && is_false b then c
+ else if is_true b && is_false a then BNot c
+ else BTernary(c, a, b)
let f_e_op op a b = match a, b with
| EItem i, EItem j -> BConst (if op = E_EQ then i = j else i <> j)
@@ -263,3 +264,15 @@ let rec formula_replace_evars repls e =
| x -> x
+
+(*
+ extract names of variables referenced in formula
+*)
+
+let rec refd_evars_of_f = function
+ | BAnd (a, b) | BOr(a, b) -> refd_evars_of_f a @ refd_evars_of_f b
+ | BNot a -> refd_evars_of_f a
+ | BTernary(a, b, c) -> refd_evars_of_f a @ refd_evars_of_f b @ refd_evars_of_f c
+ | BEnumCons(_, e, EItem _) -> [e]
+ | BEnumCons(_, e, EIdent f) -> [e; f]
+ | _ -> []
diff --git a/abstract/transform.ml b/abstract/transform.ml
index 5fe4ed1..20512aa 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -545,7 +545,12 @@ let rec g_of_scope td (node, prefix, eqs) clock_scope cond =
| AST_assign(_, e) | AST_assume(_, e) ->
expr_g e
| AST_guarantee((id, _), e) ->
- (id, f_and cond (f_of_expr td (node, prefix, clock_scope) (AST_not(e), snd e)))
+ let gn = node^"/g_"^id in
+ (id,
+ f_and
+ cond
+ (f_of_expr td (node, prefix, clock_scope) (AST_not(e), snd e)),
+ gn)
:: (expr_g e)
| AST_activate (b, _) ->
let rec cond_g cond = function
diff --git a/abstract/varenv.ml b/abstract/varenv.ml
index 450bef3..4d6caca 100644
--- a/abstract/varenv.ml
+++ b/abstract/varenv.ml
@@ -256,6 +256,12 @@ let mk_varenv (rp : rooted_prog) f cl =
let ev_order = Hashtbl.create (List.length evars) in
List.iteri (fun i x -> Hashtbl.add ev_order x i) evars_ord;
+ let enum_vars = List.sort
+ (fun (id1, _) (id2, _) ->
+ compare (Hashtbl.find ev_order id1) (Hashtbl.find ev_order id2))
+ enum_vars
+ in
+
Format.printf "Order for variables: @[<hov>[%a]@]@."
(print_list Formula_printer.print_id ", ") evars_ord;
diff --git a/tests/source/cdrom.scade b/tests/source/cdrom.scade
new file mode 100644
index 0000000..92438c3
--- /dev/null
+++ b/tests/source/cdrom.scade
@@ -0,0 +1,19 @@
+node cdrom(speed: int) returns (plus, minus, error: bool)
+var ps, count: int;
+let
+ ps = 0 -> pre speed;
+
+ assume h1 : speed - ps <= 4 and speed - ps >= -4;
+ assume h2 : if (false -> pre plus) then (speed - ps > 0)
+ else if (false -> pre minus) then (speed - ps < 0)
+ else true;
+
+ plus = (ps <= 9);
+ minus = (ps >= 11);
+
+ 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);
+tel
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-21 12:27:19 +0000