diff options
Diffstat (limited to 'abstract/transform.ml')
| -rw-r--r-- | abstract/transform.ml | 69 |
1 files changed, 59 insertions, 10 deletions
diff --git a/abstract/transform.ml b/abstract/transform.ml index 87da1bd..25e4b43 100644 --- a/abstract/transform.ml +++ b/abstract/transform.ml @@ -18,7 +18,6 @@ type transform_data = { (* future : the automata state *) } - (* f_of_nexpr : transform_data -> (string, string) -> (num_expr list -> 'a) -> expr -> 'a *) @@ -122,10 +121,13 @@ and f_of_expr td (node, prefix) expr = f_of_bexpr td (node, prefix) (fun x -> x) expr -and f_of_scope active td (node, prefix, eqs) = +(* + Translate program into one big formula +*) +let rec f_of_scope active td (node, prefix, eqs) assume_guarantees = let expr_eq e eq = let instance_eq (_, id, eqs, args) = - let eq = f_of_scope active td (node^"/"^id, "", eqs) in + let eq = f_of_scope active td (node^"/"^id, "", eqs) assume_guarantees in if active then List.fold_left (fun eq ((_,argname,_), expr) -> let eq_arg = f_of_nexpr td (node, prefix) (function @@ -177,7 +179,13 @@ and f_of_scope active td (node, prefix, eqs) = in expr_eq e assume_eq | AST_guarantee (_, e) -> - expr_eq e (BConst true) + let guarantee_eq = + if active && assume_guarantees then + f_of_expr td (node, prefix) e + else + BConst true + in + expr_eq e guarantee_eq | AST_activate (b, _) -> let rec cond_eq = function | AST_activate_body b -> BConst true @@ -187,7 +195,7 @@ and f_of_scope active td (node, prefix, eqs) = in let rec do_tree_act = function | AST_activate_body b -> - f_of_scope true td (node, b.act_id^".", b.body) + f_of_scope true td (node, b.act_id^".", b.body) assume_guarantees | AST_activate_if(c, a, b) -> f_or (f_and (f_of_expr td (node, prefix) c) @@ -196,7 +204,7 @@ and f_of_scope active td (node, prefix, eqs) = (f_and (do_tree_act b) (do_tree_inact a))) and do_tree_inact = function | AST_activate_body b -> - f_of_scope false td (node, b.act_id^".", b.body) + f_of_scope false td (node, b.act_id^".", b.body) assume_guarantees | AST_activate_if(_, a, b) -> f_and (do_tree_inact a) (do_tree_inact b) in @@ -216,17 +224,18 @@ and f_of_scope active td (node, prefix, eqs) = time_incr_eq (List.map do_eq eqs) -and f_of_prog p root = +and f_of_prog p root assume_guarantees = let td = { root_scope = get_root_scope p root; p = p; consts = I.consts p root; } in - f_of_scope true td td.root_scope - - + f_of_scope true td td.root_scope assume_guarantees +(* + Translate init state into a formula +*) let rec init_f_of_scope p (node, prefix, eqs) = let expr_eq e = let instance_eq (_, id, eqs, args) = @@ -258,3 +267,43 @@ let rec init_f_of_scope p (node, prefix, eqs) = and init_f_of_prog p root = init_f_of_scope p (get_root_scope p root) + +(* + Get expressions for guarantee violation +*) +let rec g_of_scope td (node, prefix, eqs) cond = + let expr_g e = + let instance_g (_, id, eqs, args) = + g_of_scope td (node^"/"^id, "", eqs) cond + in + List.fold_left (fun x i -> (instance_g i) @ x) + [] (extract_instances td.p e) + in + let do_eq eq = match fst eq with + | AST_assign(_, e) | AST_assume(_, e) -> + expr_g e + | AST_guarantee((id, _), e) -> + (id, f_and cond (f_of_expr td (node, prefix) (AST_not(e), snd e))) + :: (expr_g e) + | AST_activate (b, _) -> + let rec cond_g cond = function + | AST_activate_body b -> + g_of_scope td (node, b.act_id^".", b.body) cond + | AST_activate_if(c, a, b) -> + (cond_g (f_and cond (f_of_expr td (node, prefix) c)) a) @ + (cond_g (f_and cond (f_of_expr td (node, prefix) (AST_not(c), snd c))) b) @ + (expr_g c) + in + cond_g cond b + | AST_automaton _ -> not_implemented "g_of_scope automaton" + in + List.fold_left (@) [] (List.map do_eq eqs) + +and guarantees_of_prog p root = + let td = { + root_scope = get_root_scope p root; + p = p; + consts = I.consts p root; + } in + + g_of_scope td (get_root_scope p root) (BConst true) |