diff options
Diffstat (limited to 'abstract/transform.ml')
| -rw-r--r-- | abstract/transform.ml | 44 |
1 files changed, 21 insertions, 23 deletions
diff --git a/abstract/transform.ml b/abstract/transform.ml index 6fa1277..b6781a8 100644 --- a/abstract/transform.ml +++ b/abstract/transform.ml @@ -136,7 +136,7 @@ and f_of_bexpr td (node, prefix) where expr = | AST_EQ -> E_EQ | AST_NE -> E_NE | _ -> type_error "Invalid operator on enumerated values." - in BEnumCons(eop, x, y) + in f_e_op eop x y | _ -> invalid_arity "Binary operator") (AST_tuple [a; b], snd expr)) (* Temporal *) @@ -233,12 +233,18 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees = BConst true in f_and (expr_eq e) assume_eq - | AST_guarantee (_, e) -> + | AST_guarantee ((id, _), e) -> + let gn = node^"/g_"^id in let guarantee_eq = if active && assume_guarantees then - f_of_expr td (node, prefix) e + f_and (f_of_expr td (node, prefix) e) + (BEnumCons(E_EQ, gn, EItem bool_true)) else - BConst true + f_or + (f_and (f_of_expr td (node, prefix) e) + (BEnumCons(E_EQ, gn, EItem bool_true))) + (f_and (BNot (f_of_expr td (node, prefix) e)) + (BEnumCons(E_EQ, gn, EItem bool_false))) in f_and (expr_eq e) guarantee_eq | AST_activate (b, _) -> @@ -265,8 +271,8 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees = in f_and (cond_eq b) (if active then do_tree_act b else do_tree_inact b) | AST_automaton (aid, states, _) -> - let stv = EIdent (node^"/"^aid^".state") in - let nstv = EIdent ("N"^node^"/"^aid^".state") in + let stv = node^"/"^aid^".state" in + let nstv = "N"^node^"/"^aid^".state" in let st_eq_inact (st, _) = f_and (f_of_scope false td @@ -304,13 +310,9 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees = then BRel(AST_EQ, NIdent("N"^node^"/"^prefix^"time"), NBinary(AST_PLUS, NIntConst 1, NIdent(node^"/"^prefix^"time"))) else BConst true) - (f_and - (if List.mem (node^"/") td.rp.act_scope - then f_e_eq (EIdent(node^"/"^prefix^"act")) (EItem bool_true) - else BConst true) - (if List.mem (node^"/") td.rp.init_scope - then f_e_eq (EIdent("N"^node^"/"^prefix^"init")) (EItem bool_false) - else BConst true)) + (if List.mem (node^"/") td.rp.init_scope + then f_e_eq (EIdent("N"^node^"/"^prefix^"init")) (EItem bool_false) + else BConst true) else f_and (if not (List.mem (node^"/") td.rp.no_time_scope) @@ -318,14 +320,10 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees = NIdent("N"^node^"/"^prefix^"time"), NIdent(node^"/"^prefix^"time")) else BConst true) - (f_and - (if List.mem (node^"/") td.rp.act_scope - then f_e_eq (EIdent(node^"/"^prefix^"act")) (EItem bool_false) - else BConst true) - (if List.mem (node^"/") td.rp.init_scope - then f_e_eq (EIdent("N"^node^"/"^prefix^"init")) - (EIdent (node^"/"^prefix^"init")) - else BConst true)) + (if List.mem (node^"/") td.rp.init_scope + then f_e_eq (EIdent("N"^node^"/"^prefix^"init")) + (EIdent (node^"/"^prefix^"init")) + else BConst true) in List.fold_left f_and time_incr_eq @@ -364,7 +362,7 @@ let rec init_f_of_scope rp (node, prefix, eqs) = cond_eq b | AST_automaton (aid, states, _) -> let (st, _) = List.find (fun (st, _) -> st.initial) states in - let init_eq = BEnumCons(E_EQ, EIdent(node^"/"^aid^".state"), EItem st.st_name) in + let init_eq = BEnumCons(E_EQ, node^"/"^aid^".state", EItem st.st_name) in let state_eq (st, _) = let sc_f = init_f_of_scope rp (node, aid^"."^st.st_name^".", st.body) @@ -421,7 +419,7 @@ let rec g_of_scope td (node, prefix, eqs) cond = | AST_automaton (aid, states, _) -> let st_g (st, _) = g_of_scope td (node, aid^"."^st.st_name^".", st.body) - (f_and cond (BEnumCons(E_EQ, EIdent(node^"/"^aid^".state"), EItem st.st_name))) + (f_and cond (BEnumCons(E_EQ, node^"/"^aid^".state", EItem st.st_name))) in List.flatten (List.map st_g states) in |