summaryrefslogtreecommitdiff
path: root/abstract
diff options
context:
space:
mode:
Diffstat (limited to 'abstract')
-rw-r--r--abstract/abs_interp_edd.ml5
-rw-r--r--abstract/formula.ml68
-rw-r--r--abstract/formula_printer.ml8
-rw-r--r--abstract/transform.ml122
4 files changed, 142 insertions, 61 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 "@[<hv 2>(%a)@]" print_bool_expr b
else Format.fprintf fmt "@[<hv 2>%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
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-21 18:00:43 +0000