summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--abstract/abs_interp.ml19
-rw-r--r--abstract/formula.ml2
-rw-r--r--abstract/transform.ml108
-rw-r--r--frontend/typing.ml17
4 files changed, 104 insertions, 42 deletions
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index e55f199..383a69c 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -29,29 +29,30 @@ end = struct
(* init state *)
let init_state widen_delay rp =
- let f = Formula.eliminate_not (Transform.f_of_prog rp false) in
- let f_g = Formula.eliminate_not (Transform.f_of_prog rp true) in
-
let env = List.fold_left
(fun env (_, id, ty) -> E.addvar env id ty)
E.init
rp.all_vars
in
- let init_f = Transform.init_f_of_prog rp in
- let guarantees = Transform.guarantees_of_prog rp in
+ Format.printf "Vars: @[<hov>%a@]@.@."
+ (Ast_printer.print_list Ast_printer.print_typed_var ", ")
+ rp.all_vars;
+ let init_f = Transform.init_f_of_prog rp in
Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f;
- Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f;
- Format.printf "Cycle formula with guarantees:@.%a@.@." Formula_printer.print_expr f_g;
-
- Format.printf "Vars: @[<hov>%a@]@.@." (Ast_printer.print_list Ast_printer.print_typed_var ", ") rp.all_vars;
+ let guarantees = Transform.guarantees_of_prog rp in
Format.printf "Guarantees:@.";
List.iter (fun (id, f) ->
Format.printf " %s: %a@." id Formula_printer.print_expr f)
guarantees;
Format.printf "@.";
+ let f = Formula.eliminate_not (Transform.f_of_prog rp false) in
+ let f_g = Formula.eliminate_not (Transform.f_of_prog rp true) in
+ Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f;
+ Format.printf "Cycle formula with guarantees:@.%a@.@." Formula_printer.print_expr f_g;
+
let env = E.set_disjunct env "/exit" DNever in
let env = E.apply_f env init_f in
diff --git a/abstract/formula.ml b/abstract/formula.ml
index ce83935..62acb28 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -54,6 +54,8 @@ let f_and a b = match a, b with
| a, BConst true -> a
| a, b -> BAnd(a, b)
+let f_and_list = List.fold_left f_and (BConst true)
+
let f_or a b = match a, b with
| BConst true, _ | _, BConst true -> BConst true
| BConst false, b -> b
diff --git a/abstract/transform.ml b/abstract/transform.ml
index 64fd8d8..6fa1277 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -166,24 +166,22 @@ and f_of_expr td (node, prefix) expr =
Translate program into one big formula
*)
let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
- let expr_eq e eq =
+ let expr_eq e =
let instance_eq (_, id, eqs, args) =
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_neexpr td (node, prefix) (function
- | [NE v] -> BRel(AST_EQ, NIdent(node^"/"^id^"/"^argname), v)
- | [EE v] -> f_e_eq (EIdent(node^"/"^id^"/"^argname)) v
- | _ -> invalid_arity "in argument")
- expr
- in f_and eq eq_arg)
- eq args
+ let arg_eq ((_,argname,_), expr) =
+ f_of_neexpr td (node, prefix) (function
+ | [NE v] -> BRel(AST_EQ, NIdent(node^"/"^id^"/"^argname), v)
+ | [EE v] -> f_e_eq (EIdent(node^"/"^id^"/"^argname)) v
+ | _ -> invalid_arity "in argument")
+ expr
+ in f_and eq (f_and_list (List.map arg_eq args))
else
eq
in
- let eq = List.fold_left (fun x i -> f_and (instance_eq i) x)
- eq (extract_instances td.rp.p e)
- in
+ let eq_i = f_and_list (List.map instance_eq (extract_instances td.rp.p e)) in
+
let pre_expr (id, expr) =
if active then
f_of_neexpr td (node, prefix) (fun elist ->
@@ -205,27 +203,28 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
| TEnum _ -> f_e_eq (EIdent("N"^id^"."^x)) (EIdent (id^"."^x)))
typ)
in
- List.fold_left (fun x i -> f_and (pre_expr i) x)
- eq (extract_pre e)
+ let eq_p = f_and_list (List.map pre_expr (extract_pre e)) in
+
+ f_and eq_i eq_p
in
let do_eq eq = match fst eq with
| AST_assign(ids, e) ->
let assign_eq =
if active then
- f_of_neexpr td (node, prefix)
- (fun vs ->
- let rels =
- List.map2 (fun (id, _) -> function
- | NE v -> BRel(AST_EQ, NIdent (node^"/"^id), v)
- | EE v -> f_e_eq (EIdent (node^"/"^id)) v)
- ids vs
- in
- list_fold_op f_and rels)
- e
+ let apply_f vs =
+ let rels =
+ List.map2 (fun (id, _) -> function
+ | NE v -> BRel(AST_EQ, NIdent (node^"/"^id), v)
+ | EE v -> f_e_eq (EIdent (node^"/"^id)) v)
+ ids vs
+ in
+ f_and_list rels
+ in
+ f_of_neexpr td (node, prefix) apply_f e
else
BConst true
in
- expr_eq e assign_eq
+ f_and (expr_eq e) assign_eq
| AST_assume (_, e) ->
let assume_eq =
if active then
@@ -233,7 +232,7 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
else
BConst true
in
- expr_eq e assume_eq
+ f_and (expr_eq e) assume_eq
| AST_guarantee (_, e) ->
let guarantee_eq =
if active && assume_guarantees then
@@ -241,12 +240,12 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
else
BConst true
in
- expr_eq e guarantee_eq
+ f_and (expr_eq e) guarantee_eq
| AST_activate (b, _) ->
let rec cond_eq = function
| AST_activate_body b -> BConst true
| AST_activate_if(c, a, b) ->
- f_and (expr_eq c (BConst true))
+ f_and (expr_eq c)
(f_and (cond_eq a) (cond_eq b))
in
let rec do_tree_act = function
@@ -265,7 +264,38 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
f_and (do_tree_inact a) (do_tree_inact b)
in
f_and (cond_eq b) (if active then do_tree_act b else do_tree_inact b)
- | AST_automaton _ -> not_implemented "f_of_scope do_eq automaton"
+ | AST_automaton (aid, states, _) ->
+ let stv = EIdent (node^"/"^aid^".state") in
+ let nstv = EIdent ("N"^node^"/"^aid^".state") in
+ let st_eq_inact (st, _) =
+ f_and
+ (f_of_scope false td
+ (node, aid^"."^st.st_name^".", st.body) assume_guarantees)
+ (f_and_list (List.map (fun (c, _, _) -> expr_eq c) st.until))
+ in
+ if active then
+ let st_eq_act (st, l) =
+ let act_eq =
+ let st_eq = f_of_scope true td
+ (node, aid^"."^st.st_name^".", st.body) assume_guarantees in
+ let rec aux = function
+ | [] -> BEnumCons(E_EQ, nstv, EItem st.st_name)
+ | (c, (target, l), rst)::q ->
+ if rst then loc_error l error "Resetting transitions not supported.";
+ f_or
+ (f_and (f_of_expr td (node, prefix) c)
+ (BEnumCons(E_EQ, nstv, EItem target)))
+ (f_and (BNot (f_of_expr td (node, prefix) c)) (aux q))
+ in f_and st_eq (aux st.until)
+ in
+ f_or
+ (f_and (BEnumCons(E_EQ, stv, EItem st.st_name)) act_eq)
+ (f_and (BEnumCons(E_NE, stv, EItem st.st_name))
+ (st_eq_inact (st, l)))
+ in
+ f_and_list (List.map st_eq_act states)
+ else
+ f_and_list (List.map st_eq_inact states)
in
let time_incr_eq =
if active then
@@ -332,7 +362,16 @@ let rec init_f_of_scope rp (node, prefix, eqs) =
(f_and (cond_eq a) (cond_eq b))
in
cond_eq b
- | AST_automaton _ -> not_implemented "f_of_scope do_eq automaton"
+ | AST_automaton (aid, states, _) ->
+ let (st, _) = List.find (fun (st, _) -> st.initial) states in
+ let init_eq = BEnumCons(E_EQ, EIdent(node^"/"^aid^".state"), EItem st.st_name) in
+ let state_eq (st, _) =
+ let sc_f =
+ init_f_of_scope rp (node, aid^"."^st.st_name^".", st.body)
+ in List.fold_left (fun f (c, _, _) -> f_and f (expr_eq c)) sc_f st.until
+ in
+ List.fold_left f_and init_eq
+ (List.map state_eq states)
in
let time_eq =
f_and
@@ -379,9 +418,14 @@ let rec g_of_scope td (node, prefix, eqs) cond =
(expr_g c)
in
cond_g cond b
- | AST_automaton _ -> not_implemented "g_of_scope automaton"
+ | AST_automaton (aid, states, _) ->
+ let st_g (st, _) =
+ g_of_scope td (node, aid^"."^st.st_name^".", st.body)
+ (f_and cond (BEnumCons(E_EQ, EIdent(node^"/"^aid^".state"), EItem st.st_name)))
+ in
+ List.flatten (List.map st_g states)
in
- List.fold_left (@) [] (List.map do_eq eqs)
+ List.flatten (List.map do_eq eqs)
and guarantees_of_prog rp =
let td = {
diff --git a/frontend/typing.ml b/frontend/typing.ml
index a4abfe0..564d91e 100644
--- a/frontend/typing.ml
+++ b/frontend/typing.ml
@@ -158,7 +158,22 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars =
| AST_activate_if(c, a, b) ->
vars_of_expr c @ do_branch a @ do_branch b
in do_branch b
- | AST_automaton _ -> not_implemented "extract_all vars automaton"
+ | AST_automaton (aid, states, ret) ->
+ let do_state (st, _) =
+ let tvars =
+ List.flatten
+ (List.map (fun (e, _, _) -> vars_of_expr e) st.until)
+ in
+ let svars = vars_in_node node st.st_locals in
+ svars @ tvars @
+ extract_all_vars rp
+ (node, aid^"."^st.st_name^".", st.body)
+ (tvars@n_vars)
+ in
+ let st_ids = List.map (fun (st, _) -> st.st_name) states in
+ (false, node^"/"^aid^".state", TEnum st_ids)::
+ (false, "N"^node^"/"^aid^".state", TEnum st_ids)::
+ (List.flatten (List.map do_state states))
in
let v = List.flatten (List.map vars_of_eq eqs) in
let v =