diff options
Diffstat (limited to 'abstract/transform.ml')
| -rw-r--r-- | abstract/transform.ml | 22 |
1 files changed, 14 insertions, 8 deletions
diff --git a/abstract/transform.ml b/abstract/transform.ml index 7ae54ad..dcb4049 100644 --- a/abstract/transform.ml +++ b/abstract/transform.ml @@ -120,7 +120,7 @@ let rec f_of_neexpr td (node, prefix, clock_scope) where expr = | _ 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)])) + (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)])) | _ -> le type_error "Expected numerical/enumerated value" @@ -135,11 +135,12 @@ let rec f_of_neexpr td (node, prefix, clock_scope) where expr = *) and f_of_bexpr td (node, prefix, clock_scope) where expr = let sub = f_of_bexpr td (node, prefix, clock_scope) in + let sub_id = sub (fun x -> x) in match fst expr with | AST_bool_const b -> where (BConst b) - | AST_binary_bool(AST_AND, a, b) -> f_and (sub where a) (sub where b) - | AST_binary_bool(AST_OR, a, b) -> f_or (sub where a) (sub where b) - | AST_not(a) -> BNot(sub where a) + | AST_binary_bool(AST_AND, a, b) -> where (f_and (sub_id a) (sub_id b)) + | AST_binary_bool(AST_OR, a, b) -> where (f_or (sub_id a) (sub_id b)) + | AST_not(a) -> where (BNot (sub_id a)) | AST_binary_rel(rel, a, b) -> where (f_of_neexpr td (node, prefix, clock_scope) @@ -175,9 +176,7 @@ and f_of_bexpr td (node, prefix, clock_scope) where expr = | _ when type_expr td.rp node expr = [bool_type] -> let ff = function | [EE x] -> - f_or - (f_and (f_e_eq x (EItem bool_true)) (where (BConst true))) - (f_and (f_e_eq x (EItem bool_false)) (where (BConst false))) + where (f_e_eq x (EItem bool_true)) | _ -> assert false in f_of_neexpr td (node, prefix, clock_scope) ff expr @@ -387,7 +386,14 @@ and f_of_prog rp assume_guarantees = let clock_scope, clock_eq = gen_clock td rp.root_scope true in - f_and clock_eq (f_of_scope true td td.rp.root_scope clock_scope assume_guarantees) + let scope_f = + f_of_scope + true + td td.rp.root_scope + clock_scope + assume_guarantees in + f_and clock_eq scope_f + (* Translate init state into a formula |