diff options
Diffstat (limited to 'abstract/transform.ml')
| -rw-r--r-- | abstract/transform.ml | 57 |
1 files changed, 36 insertions, 21 deletions
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 = |