diff options
Diffstat (limited to 'abstract')
| -rw-r--r-- | abstract/abs_interp_edd.ml | 19 | ||||
| -rw-r--r-- | abstract/formula.ml | 6 | ||||
| -rw-r--r-- | abstract/transform.ml | 57 |
3 files changed, 52 insertions, 30 deletions
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml index b139f9e..56b366e 100644 --- a/abstract/abs_interp_edd.ml +++ b/abstract/abs_interp_edd.ml @@ -588,7 +588,6 @@ end = struct (* program expressions *) init_cl : conslist; cl : conslist; - cl_g : conslist; guarantees : (id * bool_expr) list; } @@ -773,18 +772,24 @@ end = struct init_env : cmdline_opt -> rooted_prog -> env *) 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 f = Transform.f_of_prog_incl_init rp false in + + let f = simplify_k (get_root_true f) f in + Format.printf "Complete formula:@.%a@.@." Formula_printer.print_expr f; + + (* HERE POSSIBILITY OF SIMPLIFYING EQUATIONS SUCH AS x = y OR x = v *) + (* IF SUCH AN EQUATION APPEARS IN get_root_true f THEN IT IS ALWAYS TRUE *) + + let init_f = simplify_k [BEnumCons(E_EQ, "L/must_reset", EItem bool_true)] f in + let f = simplify_k [BEnumCons(E_NE, "L/must_reset", EItem bool_true)] f 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; let cl = Formula.conslist_of_f f in - let cl_g = Formula.conslist_of_f f_g in let init_cl = Formula.conslist_of_f init_f in Format.printf "Cycle conslist:@.%a@.@." Formula_printer.print_conslist cl; @@ -795,10 +800,10 @@ end = struct guarantees; Format.printf "@."; - let ve = mk_varenv rp f_g cl_g in + let ve = mk_varenv rp f cl in - { rp; opt; ve; init_cl; cl; cl_g; guarantees; } + { rp; opt; ve; init_cl; cl; guarantees; } diff --git a/abstract/formula.ml b/abstract/formula.ml index 1882c85..4c2c397 100644 --- a/abstract/formula.ml +++ b/abstract/formula.ml @@ -76,7 +76,8 @@ 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 + 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) @@ -109,7 +110,8 @@ and eliminate_not_negate = function | AST_GE -> AST_LT in BRel(r', a, b, is_real) - | BTernary _ -> assert false + | BTernary (c, a, b) -> + eliminate_not_negate(BOr(BAnd(c, a), BAnd(BNot c, b))) | BAnd(a, b) -> BOr(eliminate_not_negate a, eliminate_not_negate b) | BOr(a, b) -> diff --git a/abstract/transform.ml b/abstract/transform.ml index 9bce192..0144637 100644 --- a/abstract/transform.ml +++ b/abstract/transform.ml @@ -209,6 +209,13 @@ let clock_scope_here (node, prefix, _) = let gen_clock td (node, prefix, _) active rst_exprs = let clock_scope = node^"/"^prefix in + let act_eq = + if clock_scope = "/" + then BConst true + else if active + then BEnumCons(E_EQ, clock_scope^"act", EItem bool_true) + else BEnumCons(E_NE, clock_scope^"act", EItem bool_true) + in let clock_eq = let rst_code = f_and @@ -219,28 +226,36 @@ let gen_clock td (node, prefix, _) active rst_exprs = then f_e_eq (EIdent(clock_scope^"init")) (EItem bool_true) else BConst true) in + let last_act_eq = + (f_and + (if not (td.rp.no_time_scope clock_scope) + then BRel(AST_EQ, NIdent(clock_scope^"time"), + NBinary(AST_PLUS, NIntConst 1, NIdent("L"^clock_scope^"time"), false), + false) + else BConst true) + (if td.rp.init_scope clock_scope + then BEnumCons (E_NE, clock_scope^"init", EItem bool_true) + else BConst true)) + in + let last_inact_eq = + (f_and + (if not (td.rp.no_time_scope clock_scope) + then BRel(AST_EQ, + NIdent(clock_scope^"time"), + NIdent("L"^clock_scope^"time"), false) + else BConst true) + (if td.rp.init_scope clock_scope + then f_e_eq (EIdent(clock_scope^"init")) + (EIdent ("L"^clock_scope^"init")) + else BConst true)) + in let no_rst_code = - if active then - f_and - (if not (td.rp.no_time_scope clock_scope) - then BRel(AST_EQ, NIdent(clock_scope^"time"), - NBinary(AST_PLUS, NIntConst 1, NIdent("L"^clock_scope^"time"), false), - false) - else BConst true) - (if td.rp.init_scope clock_scope - then BEnumCons (E_NE, clock_scope^"init", EItem bool_true) - else BConst true) + if clock_scope = "/" + then last_act_eq else - f_and - (if not (td.rp.no_time_scope clock_scope) - then BRel(AST_EQ, - NIdent(clock_scope^"time"), - NIdent("L"^clock_scope^"time"), false) - else BConst true) - (if td.rp.init_scope clock_scope - then f_e_eq (EIdent(clock_scope^"init")) - (EIdent ("L"^clock_scope^"init")) - else BConst true) + f_ternary + (BEnumCons(E_EQ, "L"^clock_scope^"act", EItem bool_true)) + last_act_eq last_inact_eq in if rst_code = BConst true && no_rst_code = BConst true then BConst true @@ -250,7 +265,7 @@ let gen_clock td (node, prefix, _) active rst_exprs = rst_code no_rst_code in - (clock_scope, rst_exprs), clock_eq + (clock_scope, rst_exprs), f_and act_eq clock_eq let rec f_of_scope active td (node, prefix, eqs) (clock_scope, rst_exprs as cs) assume_guarantees = let expr_eq e = |