diff options
Diffstat (limited to 'abstract/transform.ml')
| -rw-r--r-- | abstract/transform.ml | 57 |
1 files changed, 49 insertions, 8 deletions
diff --git a/abstract/transform.ml b/abstract/transform.ml index e6886b8..40390dd 100644 --- a/abstract/transform.ml +++ b/abstract/transform.ml @@ -67,7 +67,7 @@ let rec f_of_nexpr td (node, prefix) where expr = BAnd(BNot(f_of_bexpr td (node, prefix) c), sub where b)) | AST_instance ((f, _), args, nid) -> let (n, _) = find_node_decl td.p f in - where (List.map (fun (_, (id, _), _) -> NIdent (node^"/"^nid^"/"^id)) n.ret) + where (List.map (fun (_, id, _) -> NIdent (node^"/"^nid^"/"^id)) n.ret) (* boolean values treated as integers *) | _ -> @@ -101,10 +101,10 @@ and f_of_bexpr td (node, prefix) expr = and f_of_scope active td (node, prefix, eqs) = let expr_eq e eq = - let instance_eq (id, eqs, args) = + let instance_eq (_, id, eqs, args) = let eq = f_of_scope active td (node^"/"^id, "", eqs) in if active then - List.fold_left (fun eq ((_,(argname,_),_), expr) -> + List.fold_left (fun eq ((_,argname,_), expr) -> let eq_arg = f_of_nexpr td (node, prefix) (function | [v] -> BRel(AST_EQ, NIdent(node^"/"^id^"/"^argname), v) | _ -> invalid_arity "in argument") @@ -146,11 +146,15 @@ and f_of_scope active td (node, prefix, eqs) = in expr_eq e assign_eq | AST_assume (_, e) -> - if active then - f_of_bexpr td (node, prefix) e - else - BConst true - | AST_guarantee _ -> BConst true + let assume_eq = + if active then + f_of_bexpr td (node, prefix) e + else + BConst true + in + expr_eq e assume_eq + | AST_guarantee (_, e) -> + expr_eq e (BConst true) | AST_activate (b, _) -> let rec cond_eq = function | AST_activate_body b -> BConst true @@ -199,3 +203,40 @@ and f_of_prog p root = f_of_scope true td td.root_scope + + + + + + +let rec init_f_of_scope p (node, prefix, eqs) = + let expr_eq e = + let instance_eq (_, id, eqs, args) = + init_f_of_scope p (node^"/"^id, "", eqs) + in + List.fold_left (fun x i -> f_and (instance_eq i) x) + (BConst true) (extract_instances p e) + in + let do_eq eq = match fst eq with + | AST_assign(_, e) | AST_assume(_, e) | AST_guarantee(_, e) -> + expr_eq e + | AST_activate (b, _) -> + let rec cond_eq = function + | AST_activate_body b -> + init_f_of_scope p (node, b.act_id^"_", b.body) + | AST_activate_if(c, a, b) -> + f_and (expr_eq c) + (f_and (cond_eq a) (cond_eq b)) + in + cond_eq b + | AST_automaton _ -> not_implemented "f_of_scope do_eq automaton" + in + let time_eq = + BRel(AST_EQ, + NIdent(node^"/"^prefix^"time"), + NIntConst 0) + in + List.fold_left f_and time_eq (List.map do_eq eqs) + +and init_f_of_prog p root = + init_f_of_scope p (get_root_scope p root) |