summaryrefslogtreecommitdiff
path: root/abstract/transform.ml
diff options
context:
space:
mode:
Diffstat (limited to 'abstract/transform.ml')
-rw-r--r--abstract/transform.ml122
1 files changed, 62 insertions, 60 deletions
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-10 03:38:20 +0000