diff options
Diffstat (limited to 'abstract/transform.ml')
| -rw-r--r-- | abstract/transform.ml | 63 |
1 files changed, 50 insertions, 13 deletions
diff --git a/abstract/transform.ml b/abstract/transform.ml index 708456e..64fd8d8 100644 --- a/abstract/transform.ml +++ b/abstract/transform.ml @@ -70,11 +70,19 @@ let rec f_of_neexpr td (node, prefix) where expr = | TEnum _ -> EE(EIdent x)) typ) | AST_arrow(a, b) -> - f_or - (f_and (BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0)) - (sub where a)) - (f_and (BRel(AST_GE, NIdent(node^"/"^prefix^"time"), NIntConst 1)) - (sub where b)) + if List.mem (node^"/") td.rp.init_scope + then + f_or + (f_and (f_e_eq (EIdent (node^"/"^prefix^"init")) (EItem bool_true)) + (sub where a)) + (f_and (f_e_eq (EIdent (node^"/"^prefix^"init")) (EItem bool_false)) + (sub where b)) + else + f_or + (f_and (BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0)) + (sub where a)) + (f_and (BRel(AST_GE, NIdent(node^"/"^prefix^"time"), NIntConst 1)) + (sub where b)) (* other *) | AST_if(c, a, b) -> f_or @@ -261,12 +269,33 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees = in let time_incr_eq = if active then - BRel(AST_EQ, NIdent("N"^node^"/"^prefix^"time"), - NBinary(AST_PLUS, NIntConst 1, NIdent(node^"/"^prefix^"time"))) + f_and + (if not (List.mem (node^"/") td.rp.no_time_scope) + 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)) else - BRel(AST_EQ, - NIdent("N"^node^"/"^prefix^"time"), - NIdent(node^"/"^prefix^"time")) + f_and + (if not (List.mem (node^"/") td.rp.no_time_scope) + then BRel(AST_EQ, + 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)) in List.fold_left f_and time_incr_eq @@ -306,9 +335,17 @@ let rec init_f_of_scope rp (node, prefix, eqs) = | AST_automaton _ -> not_implemented "f_of_scope do_eq automaton" in let time_eq = - BRel(AST_EQ, - NIdent(node^"/"^prefix^"time"), - NIntConst 0) + f_and + (if not (List.mem (node^"/") rp.no_time_scope) + then + BRel(AST_EQ, + NIdent(node^"/"^prefix^"time"), + NIntConst 0) + else BConst true) + (if List.mem (node^"/") rp.init_scope + then + f_e_eq (EIdent(node^"/"^prefix^"init")) (EItem bool_true) + else BConst true) in List.fold_left f_and time_eq (List.map do_eq eqs) |