summaryrefslogtreecommitdiff
path: root/abstract/transform.ml
diff options
context:
space:
mode:
Diffstat (limited to 'abstract/transform.ml')
-rw-r--r--abstract/transform.ml69
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)