From d6db8e934346d3a4ff2bb1470a9512462419bf03 Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Tue, 8 Jul 2014 16:01:36 +0200 Subject: Add ternaries, simplifications. BIG BUG FOUND (init/reset translation) --- abstract/abs_interp_edd.ml | 5 ++ abstract/formula.ml | 68 ++++++++++++++++++++++++ abstract/formula_printer.ml | 8 ++- abstract/transform.ml | 122 ++++++++++++++++++++++---------------------- main.ml | 4 +- 5 files changed, 144 insertions(+), 63 deletions(-) diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml index b80ca14..b139f9e 100644 --- a/abstract/abs_interp_edd.ml +++ b/abstract/abs_interp_edd.ml @@ -775,6 +775,11 @@ end = struct let init_env opt rp = let init_f, f = Transform.f_of_prog rp false in let _, f_g = Transform.f_of_prog rp true in + + let init_f = simplify_k (get_root_true init_f) init_f in + let f = simplify_k (get_root_true f) f in + let f_g = simplify_k (get_root_true f_g) f_g in + Format.printf "Init formula:@.%a@.@." Formula_printer.print_expr init_f; Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f; diff --git a/abstract/formula.ml b/abstract/formula.ml index 0045489..1882c85 100644 --- a/abstract/formula.ml +++ b/abstract/formula.ml @@ -48,6 +48,8 @@ type bool_expr = (* boolean operators *) | BAnd of bool_expr * bool_expr | BOr of bool_expr * bool_expr + | BTernary of bool_expr * bool_expr * bool_expr + (* (A and B) or ((not A) and C) *) | BNot of bool_expr let is_false = function @@ -71,6 +73,11 @@ let f_or a b = else if is_false b then a else BOr(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) + 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) | EIdent x, v | v, EIdent x -> BEnumCons(op, x, v) @@ -82,6 +89,8 @@ let rec eliminate_not = function | BNot e -> eliminate_not_negate e | BAnd(a, b) -> BAnd(eliminate_not a, eliminate_not b) | BOr(a, b) -> BOr(eliminate_not a, eliminate_not b) + | BTernary(c, a, b) -> + BTernary(eliminate_not c, eliminate_not a, eliminate_not b) | x -> x and eliminate_not_negate = function | BConst x -> BConst(not x) @@ -100,6 +109,7 @@ and eliminate_not_negate = function | AST_GE -> AST_LT in BRel(r', a, b, is_real) + | BTernary _ -> assert false | BAnd(a, b) -> BOr(eliminate_not_negate a, eliminate_not_negate b) | BOr(a, b) -> @@ -159,4 +169,62 @@ let rec conslist_of_f = function | _, CLTrue -> econs, cons, ra | _, _ -> econs, cons, CLAnd(ra, rb) end + | BTernary(c, a, b) -> + conslist_of_f (BOr (BAnd(c, a), BAnd(BNot(c), b))) + + +(* + Simplify formula considering something is true +*) + +let rec get_root_true = function + | BAnd(a, b) -> + get_root_true a @ get_root_true b + | BEnumCons e -> [BEnumCons e] + | BRel (a, b, c, d) -> [BRel (a, b, c, d)] + | _ -> [] + +let rec simplify true_eqs e = + if List.exists + (fun f -> + try eliminate_not e = eliminate_not f with _ -> false) + true_eqs + then BConst true + else if List.exists + (fun f -> + match e, f with + | BEnumCons(E_EQ, a, EItem v), BEnumCons(E_EQ, b, EItem w) + when a = b && v <> w -> true + | _ -> try eliminate_not e = eliminate_not_negate f with _ -> false) + true_eqs + then BConst false + else + match e with + | BAnd(a, b) -> + f_and + (simplify true_eqs a) + (simplify true_eqs b) + | BOr(a, b) -> + f_or + (simplify true_eqs a) + (simplify true_eqs b) + | BTernary(c, a, b) -> + let c, a, b = + simplify true_eqs c, + simplify true_eqs a, + simplify true_eqs b in + begin match c with + | BConst true -> a + | BConst false -> b + | _ -> BTernary(c, a, b) + end + | BNot(n) -> + begin match simplify true_eqs n with + | BConst e -> BConst (not e) + | x -> BNot x + end + | v -> v + +let rec simplify_k true_eqs e = + List.fold_left f_and (simplify true_eqs e) true_eqs diff --git a/abstract/formula_printer.ml b/abstract/formula_printer.ml index 9c6c403..a5359a8 100644 --- a/abstract/formula_printer.ml +++ b/abstract/formula_printer.ml @@ -17,6 +17,7 @@ let ne_prec = function | _ -> 100 let be_prec = function + | BTernary _ -> 10 | BRel(op, _, _, _) -> binary_rel_precedence op | BAnd _ -> binary_bool_precedence AST_AND | BOr _ -> binary_bool_precedence AST_OR @@ -97,11 +98,16 @@ let rec print_bool_expr fmt e = match e with if be_prec b < be_prec e || is_or b then Format.fprintf fmt "@[(%a)@]" print_bool_expr b else Format.fprintf fmt "@[%a@]" print_bool_expr b - | BOr (a, b) -> print_ch fmt print_bool_expr be_prec a be_prec e; Format.fprintf fmt "@ ∨ "; print_ch fmt print_bool_expr be_prec b be_prec e + | BTernary(c, a, b) -> + print_ah fmt print_bool_expr be_prec c be_prec e; + Format.fprintf fmt "@ ? "; + print_ah fmt print_bool_expr be_prec a be_prec e; + Format.fprintf fmt "@ : "; + print_ah fmt print_bool_expr be_prec b be_prec e; | BNot (a) -> Format.pp_print_string fmt "¬"; print_ch fmt print_bool_expr be_prec a be_prec e diff --git a/abstract/transform.ml b/abstract/transform.ml index e0f32c2..9bce192 100644 --- a/abstract/transform.ml +++ b/abstract/transform.ml @@ -88,25 +88,27 @@ let rec f_of_neexpr td (node, prefix, clock_scope) where expr = | AST_arrow(a, b) -> if td.rp.init_scope clock_scope then - f_or - (f_and (f_e_eq (EIdent (clock_scope^"init")) (EItem bool_true)) - (sub where a)) - (f_and (f_e_eq (EIdent (clock_scope^"init")) (EItem bool_false)) - (sub where b)) + f_ternary + (f_e_eq (EIdent (clock_scope^"init")) (EItem bool_true)) + (sub where a) + (sub where b) else if not (td.rp.no_time_scope clock_scope) then - f_or - (f_and (BRel(AST_EQ, NIdent(clock_scope^"time"), NIntConst 0, false)) - (sub where a)) - (f_and (BRel(AST_GE, NIdent(clock_scope^"time"), NIntConst 1, false)) - (sub where b)) - else + f_ternary + (BRel(AST_GE, NIdent(clock_scope^"time"), NIntConst 1, false)) + (sub where b) + (sub where a) + else begin + Format.eprintf "WARNING: scope %s needs a clock (init var or time var)!@." + clock_scope; f_or (sub where a) (sub where b) + end (* other *) | AST_if(c, a, b) -> - f_or - (f_and (f_of_expr td (node, prefix, clock_scope) c) (sub where a)) - (f_and (BNot(f_of_expr td (node, prefix, clock_scope) c)) (sub where b)) + f_ternary + (f_of_expr td (node, prefix, clock_scope) c) + (sub where a) + (sub where b) | AST_instance ((f, _), args, nid) -> let (n, _) = find_node_decl td.rp.p f in where @@ -125,11 +127,10 @@ let rec f_of_neexpr td (node, prefix, clock_scope) where expr = in rl l [] (* boolean values treated as enumerated types *) | _ when type_expr td.rp node expr = [bool_type] -> - f_or - (f_and (f_of_expr td (node, prefix, clock_scope) expr) - (where [EE (EItem bool_true)])) - (f_and (f_of_expr td (node, prefix, clock_scope) (AST_not(expr), snd expr)) - (where [EE (EItem bool_false)])) + f_ternary + (f_of_expr td (node, prefix, clock_scope) expr) + (where [EE (EItem bool_true)]) + (where [EE (EItem bool_false)]) | _ -> le type_error "Expected numerical/enumerated value" @@ -167,20 +168,21 @@ and f_of_bexpr td (node, prefix, clock_scope) where expr = | AST_arrow(a, b) -> if td.rp.init_scope clock_scope then - f_or - (f_and (f_e_eq (EIdent (clock_scope^"init")) (EItem bool_true)) - (sub where a)) - (f_and (f_e_eq (EIdent (clock_scope^"init")) (EItem bool_false)) - (sub where b)) + BTernary( + (f_e_eq (EIdent (clock_scope^"init")) (EItem bool_true)), + (sub where a), + (sub where b)) else if not (td.rp.no_time_scope clock_scope) then - f_or - (f_and (BRel(AST_EQ, NIdent(clock_scope^"time"), NIntConst 0, false)) + BTernary( + (BRel(AST_GE, NIdent(clock_scope^"time"), NIntConst 1, false)), + (sub where b), (sub where a)) - (f_and (BRel(AST_GE, NIdent(clock_scope^"time"), NIntConst 1, false)) - (sub where b)) - else + else begin + Format.eprintf "WARNING: scope %s needs a clock (init var or time var)!@." + clock_scope; f_or (sub where a) (sub where b) + end (* Enumerations... *) | _ when type_expr td.rp node expr = [bool_type] -> let ff = function @@ -201,8 +203,6 @@ and f_of_expr td (node, prefix, clock_scope) expr = let reset_cond rst_exprs = List.fold_left f_or (BConst false) rst_exprs -let no_reset_cond rst_exprs = - List.fold_left (fun ff c -> f_and ff (BNot c)) (BConst true) rst_exprs let clock_scope_here (node, prefix, _) = node^"/"^prefix @@ -228,7 +228,7 @@ let gen_clock td (node, prefix, _) active rst_exprs = false) else BConst true) (if td.rp.init_scope clock_scope - then f_e_eq (EIdent(clock_scope^"init")) (EItem bool_false) + then BEnumCons (E_NE, clock_scope^"init", EItem bool_true) else BConst true) else f_and @@ -245,9 +245,10 @@ let gen_clock td (node, prefix, _) active rst_exprs = if rst_code = BConst true && no_rst_code = BConst true then BConst true else - f_or - (f_and (reset_cond rst_exprs) rst_code) - (f_and (no_reset_cond rst_exprs) no_rst_code) + f_ternary + (reset_cond rst_exprs) + rst_code + no_rst_code in (clock_scope, rst_exprs), clock_eq @@ -338,11 +339,10 @@ let rec f_of_scope active td (node, prefix, eqs) (clock_scope, rst_exprs as cs) f_and (f_of_expr td (node, prefix, clock_scope) e) (BEnumCons(E_EQ, gn, EItem bool_true)) else - f_or - (f_and (f_of_expr td (node, prefix, clock_scope) e) - (BEnumCons(E_EQ, gn, EItem bool_true))) - (f_and (BNot (f_of_expr td (node, prefix, clock_scope) e)) - (BEnumCons(E_EQ, gn, EItem bool_false))) + f_ternary + (f_of_expr td (node, prefix, clock_scope) e) + (BEnumCons(E_EQ, gn, EItem bool_true)) + (BEnumCons(E_NE, gn, EItem bool_true)) in f_and (expr_eq e) guarantee_eq | AST_activate (b, _) -> @@ -358,11 +358,10 @@ let rec f_of_scope active td (node, prefix, eqs) (clock_scope, rst_exprs as cs) let cs2, clock_eq = gen_clock td b_scope true rst_exprs in f_and clock_eq (f_of_scope true td b_scope cs2 assume_guarantees) | AST_activate_if(c, a, b) -> - f_or - (f_and (f_of_expr td (node, prefix, clock_scope) c) - (f_and (do_tree_act a) (do_tree_inact b))) - (f_and (BNot(f_of_expr td (node, prefix, clock_scope) c)) - (f_and (do_tree_act b) (do_tree_inact a))) + f_ternary + (f_of_expr td (node, prefix, clock_scope) c) + (f_and (do_tree_act a) (do_tree_inact b)) + (f_and (do_tree_act b) (do_tree_inact a)) and do_tree_inact = function | AST_activate_body b -> let b_scope = node, b.act_id^".", b.body in @@ -378,9 +377,10 @@ let rec f_of_scope active td (node, prefix, eqs) (clock_scope, rst_exprs as cs) let nstv = node^"/"^aid^".next_state" in let stv = node^"/"^aid^".state" in let st_choice_eq = - f_or - (f_and (reset_cond rst_exprs) (f_e_eq (EIdent stv) (EItem init_st.st_name))) - (f_and (no_reset_cond rst_exprs) (f_e_eq (EIdent stv) (EIdent lnstv))) + f_ternary + (reset_cond rst_exprs) + (f_e_eq (EIdent stv) (EItem init_st.st_name)) + (f_e_eq (EIdent stv) (EIdent lnstv)) in let rst_states = uniq_sorted @@ List.sort compare @@ List.flatten @@ -427,12 +427,12 @@ 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_or - (f_and (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)))) - (f_and (BNot (f_of_expr td (node, prefix, clock_scope) c)) (aux 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) in let trans_code = must_reset_c cnr (fun _ -> false) in let trans_code = f_and trans_code (aux st.until) in @@ -441,10 +441,10 @@ let rec f_of_scope active td (node, prefix, eqs) (clock_scope, rst_exprs as cs) if List.length states = 1 then act_eq else - f_or - (f_and (BEnumCons(E_EQ, stv, EItem st.st_name)) act_eq) - (f_and (BEnumCons(E_NE, stv, EItem st.st_name)) - (st_eq_inact (st, l))) + f_ternary + (BEnumCons(E_EQ, stv, EItem st.st_name)) + act_eq + (st_eq_inact (st, l)) in f_and st_choice_eq (f_and_list (List.map st_eq_act states)) @@ -497,8 +497,8 @@ let f_of_prog_incl_init rp assume_guarantees = consts = I.consts rp; } in - let init_cond = BEnumCons(E_EQ, "L/must_reset", bool_true) in - let no_next_init_cond = BEnumCons(E_EQ, "/must_reset", bool_false) in + let init_cond = BEnumCons(E_EQ, "L/must_reset", EItem bool_true) in + let no_next_init_cond = BEnumCons(E_NE, "/must_reset", EItem bool_true) in let clock_scope, clock_eq = gen_clock td rp.root_scope true [init_cond] in @@ -573,6 +573,8 @@ let rec extract_last_vars = function | BAnd(a, b) | BOr (a, b) -> extract_last_vars a @ extract_last_vars b | BNot(e) -> extract_last_vars e + | BTernary(c, a, b) -> extract_last_vars c @ + extract_last_vars a @ extract_last_vars b | _ -> [] and elv_ne = function diff --git a/main.ml b/main.ml index d91d139..e114554 100644 --- a/main.ml +++ b/main.ml @@ -30,8 +30,8 @@ let ai_itv_edd = ref false let ai_rel_edd = ref false let ai_root = ref "test" let ai_widen_delay = ref 5 -let ai_no_time_scopes = ref "" -let ai_init_scopes = ref "" +let ai_no_time_scopes = ref "all" +let ai_init_scopes = ref "all" let ai_disj_v = ref "" let ai_vci = ref false let ai_vvci = ref false -- cgit v1.2.3