diff options
Diffstat (limited to 'abstract')
| -rw-r--r-- | abstract/abs_interp.ml | 19 | ||||
| -rw-r--r-- | abstract/formula.ml | 2 | ||||
| -rw-r--r-- | abstract/transform.ml | 108 |
3 files changed, 88 insertions, 41 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 = { |