diff options
Diffstat (limited to 'abstract')
| -rw-r--r-- | abstract/abs_interp.ml | 7 | ||||
| -rw-r--r-- | abstract/abs_interp_edd.ml | 73 | ||||
| -rw-r--r-- | abstract/formula.ml | 3 | ||||
| -rw-r--r-- | abstract/transform.ml | 235 |
4 files changed, 164 insertions, 154 deletions
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml index c3db657..26b788b 100644 --- a/abstract/abs_interp.ml +++ b/abstract/abs_interp.ml @@ -2,17 +2,12 @@ open Ast open Ast_util open Formula open Typing +open Cmdline open Util open Num_domain open Enum_domain -type cmdline_opt = { - widen_delay : int; - disjunct : (id -> bool); - verbose_ci : bool; - vverbose_ci : bool; -} module I (ED : ENUM_ENVIRONMENT_DOMAIN) (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml index 6220a0a..c1fb905 100644 --- a/abstract/abs_interp_edd.ml +++ b/abstract/abs_interp_edd.ml @@ -2,10 +2,10 @@ open Ast open Ast_util open Formula open Typing +open Cmdline open Util open Num_domain -open Abs_interp @@ -592,9 +592,12 @@ end = struct rp : rooted_prog; opt : cmdline_opt; + last_vars : (bool * id * typ) list; + all_vars : (bool * id * typ) list; ve : varenv; (* program expressions *) + init_f : bool_expr; cl : conslist; cl_g : conslist; guarantees : (id * bool_expr) list; @@ -602,7 +605,6 @@ end = struct (* abstract interpretation *) cycle : (id * id * typ) list; (* s'(x) = s(y) *) forget : (id * typ) list; (* s'(x) not specified *) - mutable data : edd_v; } @@ -924,20 +926,33 @@ end = struct init_env : cmdline_opt -> rooted_prog -> env *) let init_env opt rp = + let init_f, f = Transform.f_of_prog rp false in + let _, f_g = Transform.f_of_prog rp true in + Format.printf "Init formula:@.%a@.@." Formula_printer.print_expr init_f; + Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f; + + let cl = Formula.conslist_of_f f in + let cl_g = Formula.conslist_of_f f_g in + Format.printf "Cycle conslist:@.%a@.@." Formula_printer.print_conslist cl; + + let last_vars = uniq_sorted (List.sort compare (Transform.extract_last_vars f_g)) in + let last_vars = List.map + (fun id -> + let (_, _, ty) = List.find (fun (_, u, _) -> id = "L"^u) rp.all_vars + in false, id, ty) + last_vars in + let all_vars = last_vars @ rp.all_vars in + Format.printf "Vars: @[<hov>%a@]@.@." (print_list Ast_printer.print_typed_var ", ") - rp.all_vars; + all_vars; let num_vars, enum_vars = List.fold_left (fun (nv, ev) (_, id, t) -> match t with | TEnum ch -> nv, (id, ch)::ev | TInt -> (id, false)::nv, ev | TReal -> (id, true)::nv, ev) - ([], []) rp.all_vars in - - let init_f = Transform.init_f_of_prog rp in - Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f; - let init_cl = conslist_of_f init_f in + ([], []) all_vars in let guarantees = Transform.guarantees_of_prog rp in Format.printf "Guarantees:@."; @@ -946,19 +961,10 @@ end = struct 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; - - let cl = Formula.conslist_of_f f in - let cl_g = Formula.conslist_of_f f_g in - Format.printf "Cycle conslist:@.%a@.@." Formula_printer.print_conslist cl; - (* calculate order for enumerated variables *) let evars = List.map fst enum_vars in - let lv = extract_linked_evars_root init_cl - @ extract_linked_evars_root cl_g in + let lv = extract_linked_evars_root cl_g in let lv = uniq_sorted (List.sort Pervasives.compare (List.map ord_couple lv)) in @@ -995,25 +1001,17 @@ end = struct (* calculate cycle variables and forget variables *) let cycle = List.fold_left (fun q (_, id, ty) -> - if id.[0] = 'N' then - (String.sub id 1 (String.length id - 1), id, ty)::q + if id.[0] = 'L' then + (id, String.sub id 1 (String.length id - 1), ty)::q else q) - [] rp.all_vars - in - let forget = List.map (fun (_, id, ty) -> (id, ty)) - (List.filter - (fun (_, id, _) -> - not (List.exists (fun (_, id2, _) -> id2 = "N"^id) rp.all_vars)) - rp.all_vars) + [] last_vars in + let forget = List.map (fun (_, id, ty) -> (id, ty)) rp.all_vars in - (* calculate initial environment *) - let data = edd_apply_cl (edd_top ve) init_cl in - Format.printf "Init: @[<hov>%a@]@." edd_print data; - { rp; opt; ve; - cl; cl_g; guarantees; - cycle; forget; data } + { rp; opt; ve; last_vars; all_vars; + init_f; cl; cl_g; guarantees; + cycle; forget } @@ -1094,7 +1092,8 @@ end = struct end in - let init_acc = edd_star_new (edd_bot e.data.ve) e.data in + let init_acc = edd_star_new (edd_bot e.ve) + (pass_cycle e (edd_apply_cl (edd_top e.ve) (conslist_of_f e.init_f))) in (* Dump final state *) let acc = ch_it 0 init_acc in @@ -1124,13 +1123,13 @@ end = struct end; (* Examine probes *) - if List.exists (fun (p, _, _) -> p) e.rp.all_vars then begin + if List.exists (fun (p, _, _) -> p) e.all_vars then begin let final_flat = edd_forget_vars final (List.fold_left (fun l (_, id, ty) -> match ty with | TInt | TReal -> l | TEnum _ -> id::l) - [] e.rp.all_vars) in + [] e.all_vars) in let final_flat = match final_flat.root with | DTop -> ND.top e.ve.nvars | DBot -> ND.bottom e.ve.nvars @@ -1146,7 +1145,7 @@ end = struct ND.print_itv (ND.project final_flat id) | TEnum _ -> Format.printf "%a : enum variable@." Formula_printer.print_id id) - e.rp.all_vars; + e.all_vars; Format.printf "@]@." end diff --git a/abstract/formula.ml b/abstract/formula.ml index 01f6655..9c0ff71 100644 --- a/abstract/formula.ml +++ b/abstract/formula.ml @@ -51,7 +51,8 @@ type bool_expr = | BNot of bool_expr let f_and a b = match a, b with - | BConst false, _ | _, BConst false -> BConst false + | BConst false, _ | _, BConst false + | BNot (BConst true), _ | _, BNot (BConst true) -> BConst false | BConst true, b -> b | a, BConst true -> a | a, b -> BAnd(a, b) diff --git a/abstract/transform.ml b/abstract/transform.ml index dcb4049..1cbc27d 100644 --- a/abstract/transform.ml +++ b/abstract/transform.ml @@ -7,7 +7,14 @@ open Typing open Interpret (* used for constant evaluation ! *) -(* Transform SCADE program to logical formula. *) +(* Transform SCADE program to logical formula. + + Convention : to access the last value of a variable, + access the variable with the same name prefixed by "L". + A pre-processing pass will extract the variables that are + referenced in such a way so that they are taken into + account when calculating the memory. +*) (* node * prefix * equations *) type scope = id * id * eqn ext list @@ -72,7 +79,7 @@ let rec f_of_neexpr td (node, prefix, clock_scope) where expr = let typ = type_expr td.rp node expr in where (List.mapi - (fun i t -> let x = id^"."^(string_of_int i) in + (fun i t -> let x = "L"^id^"."^(string_of_int i) in match t with | TInt -> NE(NIdent x, false) | TReal -> NE(NIdent x, true) @@ -190,40 +197,56 @@ and f_of_expr td (node, prefix, clock_scope) expr = Translate program into one big formula *) +let reset_cond rst_exprs = + List.fold_left f_or (BConst false) rst_exprs +let no_reset_cond rst_exprs = + List.fold_left (fun ff c -> f_and ff (BNot c)) (BConst true) rst_exprs + let clock_scope_here (node, prefix, _) = node^"/"^prefix -let gen_clock td (node, prefix, _) active = +let gen_clock td (node, prefix, _) active rst_exprs = let clock_scope = node^"/"^prefix in let clock_eq = - if active then - f_and - (if not (td.rp.no_time_scope clock_scope) - then BRel(AST_EQ, NIdent("N"^clock_scope^"time"), - NBinary(AST_PLUS, NIntConst 1, NIdent(clock_scope^"time"), false), - false) - else BConst true) - (if td.rp.init_scope clock_scope - then f_e_eq (EIdent("N"^clock_scope^"init")) (EItem bool_false) - else BConst true) - else - f_and - (if not (td.rp.no_time_scope clock_scope) - then BRel(AST_EQ, - NIdent("N"^clock_scope^"time"), - NIdent(clock_scope^"time"), false) - else BConst true) - (if td.rp.init_scope clock_scope - then f_e_eq (EIdent("N"^clock_scope^"init")) - (EIdent (clock_scope^"init")) - else BConst true) + f_or + (f_and (reset_cond rst_exprs) + (f_and + (if not (td.rp.no_time_scope clock_scope) + then BRel(AST_EQ, NIdent(clock_scope^"time"), NIntConst 0, false) + else BConst true) + (if td.rp.init_scope clock_scope + then f_e_eq (EIdent(clock_scope^"init")) (EItem bool_true) + else BConst true))) + (f_and (no_reset_cond rst_exprs) + (if active then + f_and + (if not (td.rp.no_time_scope clock_scope) + then BRel(AST_EQ, NIdent(clock_scope^"time"), + NBinary(AST_PLUS, NIntConst 1, NIdent("L"^clock_scope^"time"), false), + false) + else BConst true) + (if td.rp.init_scope clock_scope + then f_e_eq (EIdent(clock_scope^"init")) (EItem bool_false) + else BConst true) + else + f_and + (if not (td.rp.no_time_scope clock_scope) + then BRel(AST_EQ, + NIdent(clock_scope^"time"), + NIdent("L"^clock_scope^"time"), false) + else BConst true) + (if td.rp.init_scope clock_scope + then f_e_eq (EIdent(clock_scope^"init")) + (EIdent ("L"^clock_scope^"init")) + else BConst true))) in - clock_scope, clock_eq + (clock_scope, rst_exprs), clock_eq -let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees = +let rec f_of_scope active td (node, prefix, eqs) (clock_scope, rst_exprs as cs) assume_guarantees = let expr_eq e = let instance_eq (_, id, eqs, args) = - let eq = f_of_scope active td (node^"/"^id, "", eqs) clock_scope assume_guarantees in + let eq = f_of_scope active td (node^"/"^id, "", eqs) + cs assume_guarantees in if active then let arg_eq ((_,argname,ty), expr) = f_of_neexpr td (node, prefix, clock_scope) (function @@ -247,7 +270,7 @@ let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees = f_of_neexpr td (node, prefix, clock_scope) (fun elist -> list_fold_op f_and (List.mapi - (fun i v -> let x = ("N"^id^"."^(string_of_int i)) in + (fun i v -> let x = (id^"."^(string_of_int i)) in match v with | NE (v, r) -> BRel(AST_EQ, NIdent x, v, r) | EE v -> f_e_eq (EIdent x) v) @@ -257,11 +280,11 @@ let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees = let typ = type_expr td.rp node expr in list_fold_op f_and (List.mapi - (fun i t -> let x = string_of_int i in + (fun i t -> let id_x = id ^ "." ^ string_of_int i in match t with - | TInt -> BRel(AST_EQ, NIdent("N"^id^"."^x), NIdent (id^"."^x), false) - | TReal -> BRel(AST_EQ, NIdent("N"^id^"."^x), NIdent (id^"."^x), true) - | TEnum _ -> f_e_eq (EIdent("N"^id^"."^x)) (EIdent (id^"."^x))) + | TInt -> BRel(AST_EQ, NIdent(id_x), NIdent ("L"^id_x), false) + | TReal -> BRel(AST_EQ, NIdent(id_x), NIdent ("L"^id_x), true) + | TEnum _ -> f_e_eq (EIdent(id_x)) (EIdent ("L"^id_x))) typ) in let eq_p = f_and_list (List.map pre_expr (extract_pre e)) in @@ -323,8 +346,8 @@ let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees = let rec do_tree_act = function | AST_activate_body b -> let b_scope = node, b.act_id^".", b.body in - let clock_scope, clock_eq = gen_clock td b_scope true in - f_and clock_eq (f_of_scope true td b_scope clock_scope assume_guarantees) + let cs2, clock_eq = gen_clock td b_scope true rst_exprs in + f_and clock_eq (f_of_scope true td b_scope cs2 assume_guarantees) | AST_activate_if(c, a, b) -> f_or (f_and (f_of_expr td (node, prefix, clock_scope) c) @@ -334,29 +357,37 @@ let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees = and do_tree_inact = function | AST_activate_body b -> let b_scope = node, b.act_id^".", b.body in - let clock_scope, clock_eq = gen_clock td b_scope false in - f_and clock_eq (f_of_scope false td b_scope clock_scope assume_guarantees) + let cs2, clock_eq = gen_clock td b_scope false rst_exprs in + f_and clock_eq (f_of_scope false td b_scope cs2 assume_guarantees) | AST_activate_if(_, a, b) -> 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 (aid, states, _) -> + let (init_st, _) = List.find (fun (st, _) -> st.initial) states in + let lnstv = "L"^node^"/"^aid^".next_state" in + let nstv = node^"/"^aid^".next_state" in let stv = node^"/"^aid^".state" in - let nstv = "N"^node^"/"^aid^".state" in + let st_choice_eq = + f_or + (f_and (reset_cond rst_exprs) (f_e_eq (EIdent stv) (EItem init_st.st_name))) + (f_and (no_reset_cond rst_exprs) (f_e_eq (EIdent stv) (EIdent lnstv))) + in + let st_eq_inact (st, _) = let st_scope = node, aid^"."^st.st_name^".", st.body in - let clock_scope, clock_eq = gen_clock td st_scope false in + let clock_scope, clock_eq = gen_clock td st_scope false rst_exprs in f_and clock_eq (f_and - (f_of_scope false td st_scope clock_scope assume_guarantees) + (f_of_scope false td st_scope cs 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_scope = node, aid^"."^st.st_name^".", st.body in - let clock_scope, clock_eq = gen_clock td st_scope true in - let st_eq = f_and clock_eq (f_of_scope true td st_scope clock_scope assume_guarantees) in + let cs2, clock_eq = gen_clock td st_scope true rst_exprs in + let st_eq = f_and clock_eq (f_of_scope true td st_scope cs2 assume_guarantees) in let rec aux = function | [] -> BEnumCons(E_EQ, nstv, EItem st.st_name) | (c, (target, l), rst)::q -> @@ -372,9 +403,11 @@ let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees = (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) + f_and st_choice_eq + (f_and_list (List.map st_eq_act states)) else - f_and_list (List.map st_eq_inact states) + f_and st_choice_eq + (f_and_list (List.map st_eq_inact states)) in f_and_list (List.map do_eq eqs) @@ -384,77 +417,32 @@ and f_of_prog rp assume_guarantees = consts = I.consts rp; } in - let clock_scope, clock_eq = gen_clock td rp.root_scope true in - - let scope_f = - f_of_scope - true - td td.rp.root_scope - clock_scope - assume_guarantees in - f_and clock_eq scope_f - + let prog_normal = + let clock_scope, clock_eq = gen_clock td rp.root_scope true [] in -(* - Translate init state into a formula -*) -let gen_clock_init rp (node, prefix, _) = - let clock_scope = node^"/"^prefix in - let time_eq = - f_and - (if not (rp.no_time_scope clock_scope) - then - BRel(AST_EQ, - NIdent(clock_scope^"time"), - NIntConst 0, false) - else BConst true) - (if rp.init_scope clock_scope - then - f_e_eq (EIdent(clock_scope^"init")) (EItem bool_true) - else BConst true) - in - clock_scope, time_eq + let scope_f = + f_of_scope + true + td td.rp.root_scope + clock_scope + assume_guarantees in + f_and clock_eq scope_f + in + let prog_init = + let clock_scope, clock_eq = + gen_clock td rp.root_scope true [BConst true] in -let rec init_f_of_scope rp (node, prefix, eqs) clock_scope = - let expr_eq e = - let instance_eq (_, id, eqs, args) = - init_f_of_scope rp (node^"/"^id, "", eqs) clock_scope + let scope_f = + f_of_scope + true + td td.rp.root_scope + clock_scope + assume_guarantees in + f_and clock_eq scope_f in - List.fold_left (fun x i -> f_and (instance_eq i) x) - (BConst true) (extract_instances rp.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 -> - let bscope = (node, b.act_id^".", b.body) in - let clock_scope, clock_eq = gen_clock_init rp bscope in - f_and clock_eq (init_f_of_scope rp bscope clock_scope) - | 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 (aid, states, _) -> - let (st, _) = List.find (fun (st, _) -> st.initial) states in - let init_eq = BEnumCons(E_EQ, node^"/"^aid^".state", EItem st.st_name) in - let state_eq (st, _) = - let sc_f = - let st_scope = (node, aid^"."^st.st_name^".", st.body) in - let clock_scope, clock_eq = gen_clock_init rp st_scope in - f_and clock_eq (init_f_of_scope rp st_scope clock_scope) - 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 - f_and_list (List.map do_eq eqs) + prog_init, prog_normal + -and init_f_of_prog rp = - let clock_scope, clock_eq = gen_clock_init rp rp.root_scope in - f_and clock_eq (init_f_of_scope rp rp.root_scope clock_scope) (* Get expressions for guarantee violation @@ -502,3 +490,30 @@ and guarantees_of_prog rp = g_of_scope td rp.root_scope (clock_scope_here rp.root_scope) (BConst true) + + +(* + Extract variables accessed by a LAST +*) + +let rec extract_last_vars = function + | BRel(_, a, b, _) -> + elv_ne a @ elv_ne b + | BEnumCons c -> + elv_ec c + | BAnd(a, b) | BOr (a, b) -> + extract_last_vars a @ extract_last_vars b + | BNot(e) -> extract_last_vars e + | _ -> [] + +and elv_ne = function + | NIdent i when i.[0] = 'L' -> [i] + | NBinary(_, a, b, _) -> elv_ne a @ elv_ne b + | NUnary (_, a, _) -> elv_ne a + | _ -> [] + +and elv_ec (_, v, q) = + (if v.[0] = 'L' then [v] else []) @ + (match q with + | EIdent i when i.[0] = 'L' -> [i] + | _ -> []) |