diff options
Diffstat (limited to 'abstract')
| -rw-r--r-- | abstract/abs_interp.ml | 194 | ||||
| -rw-r--r-- | abstract/abs_interp_edd.ml | 90 | ||||
| -rw-r--r-- | abstract/formula.ml | 27 | ||||
| -rw-r--r-- | abstract/transform.ml | 304 |
4 files changed, 347 insertions, 268 deletions
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml index f6ce0ab..cb5ae9c 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 @@ -170,6 +165,7 @@ end = struct rp : rooted_prog; opt : cmdline_opt; + all_vars : (bool * id * typ) list; enum_vars : (id * ED.item list) list; num_vars : (id * bool) list; @@ -181,7 +177,8 @@ end = struct (* abstract interpretation *) cycle : (id * id * typ) list; (* s'(x) = s(y) *) forget : (id * typ) list; (* s'(x) not specified *) - d_vars : id list; (* disjunction variables *) + d_vars : id list; (* disjunction variables when calculating *) + acc_d_vars : id list; (* disjunction variables in accumulator *) top : case_v; env : (case, case_v) Hashtbl.t; mutable delta : case list; @@ -191,7 +188,7 @@ end = struct (* print_st : Formatter.t -> st -> unit *) - let print_st fmt st = print_aux fmt st.d_vars st.env + let print_st fmt st = print_aux fmt st.acc_d_vars st.env (* add_case : st -> case_v -> unit @@ -223,29 +220,70 @@ end = struct | [en] -> aux en (v::vals) q | _ -> assert false) (ED.project enum p) - in aux enum [] st.d_vars + in aux enum [] st.acc_d_vars + + (* + dd_apply_cl : dd_v -> conslist -> dd_v + *) + let rec apply_cl_get_all_cases (enum, num) (ec, nc, r) = + match r with + | CLTrue -> + let enums = List.fold_left + (fun enums ec -> List.flatten + (List.map (fun e -> ED.apply_cons e ec) enums)) + [enum] ec in + let num = ND.apply_cl num nc in + List.map (fun ec -> ec, num) enums + | CLFalse -> [] + | CLAnd(a, b) -> + let envs = apply_cl_get_all_cases (enum, num) (ec, nc, a) in + List.flatten + (List.map (fun e -> apply_cl_get_all_cases e (ec, nc, b)) envs) + | CLOr((eca, nca, ra), (ecb, ncb, rb)) -> + apply_cl_get_all_cases (enum, num) (ec@eca, nc@nca, ra) @ + apply_cl_get_all_cases (enum, num) (ec@ecb, nc@ncb, rb) + + (* + pass_cycle : st -> case_v -> case_v + *) + let pass_cycle st (enum, num) = + let assign_e, assign_n = List.fold_left + (fun (ae, an) (a, b, t) -> match t with + | TEnum _ -> (a, b)::ae, an + | TInt | TReal -> ae, (a, NIdent b)::an) + ([], []) st.cycle in + + let enum = ED.assign enum assign_e in + let num = ND.assign num assign_n in + + List.fold_left + (fun (enum, num) (var, t) -> + let e, n = match t with + | TEnum _ -> ED.forgetvar enum var, num + | TReal | TInt -> enum, ND.forgetvar num var + in e, n) + (enum, num) st.forget + let dd_pass_cycle st (v : dd_v) = + let vv = dd_bot st.acc_d_vars in + Hashtbl.iter (fun _ x -> dd_add_case vv (pass_cycle st x)) v.data; + vv (* init_state : int -> rooted_prog -> st *) let init_state opt rp = - Format.printf "Vars: @[<hov>%a@]@.@." - (print_list Ast_printer.print_typed_var ", ") - rp.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 + 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; - let init_cl = conslist_of_f init_f in + Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f; + let init_cl = conslist_of_f init_f in + 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 guarantees = Transform.guarantees_of_prog rp in Format.printf "Guarantees:@."; List.iter (fun (id, f) -> @@ -253,69 +291,58 @@ 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; + (* add variables from LASTs *) + 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 ", ") + 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) + ([], []) all_vars in (* 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) + [] all_vars in + let forget = List.map (fun (_, id, ty) -> (id, ty)) rp.all_vars in (* calculate disjunction variables *) - (* first approximation : use all enum variables appearing in init formula *) - let rec calculate_dvars (ec, _, r) = - let a = List.map (fun (_, id, _) -> id) ec in - let rec aux = function - | CLTrue | CLFalse -> [] - | CLAnd(u, v) -> - aux u @ aux v - | CLOr(u, v) -> - calculate_dvars u @ calculate_dvars v - in a @ aux r - in - let d_vars_0 = calculate_dvars init_cl in - let d_vars_1 = List.filter - (fun id -> opt.disjunct id && not (List.mem id d_vars_0) && id.[0] <> 'N') + (* actually, don't calculate them, rely on user input *) + let d_vars = List.filter (fun k -> k <> "/init" && opt.disjunct k) (List.map (fun (id, _) -> id) enum_vars) in - let d_vars = d_vars_0 @ d_vars_1 in + let acc_d_vars = List.filter (fun i -> i.[0] = 'L') d_vars in (* setup abstract data *) let top = ED.top enum_vars, ND.top num_vars in let delta = [] in let widen = Hashtbl.create 12 in - (* calculate initial state and environment *) - let init_s = dd_bot d_vars in - - let init_ec, _, _ = init_cl in - let init_ed = List.fold_left - (fun ed cons -> - List.flatten (List.map (fun x -> ED.apply_cons x cons) ed)) - [ED.top enum_vars] (init_ec) in - List.iter (fun ed -> dd_add_case init_s (ed, ND.top num_vars)) init_ed; - let env_dd = apply_cl init_s init_cl in - let env = env_dd.data in - let st = - { rp; opt; enum_vars; num_vars; + { rp; opt; enum_vars; num_vars; all_vars; cl; cl_g; guarantees; - cycle; forget; d_vars; top; - env; delta; widen } in + cycle; forget; acc_d_vars; d_vars; top; + env = Hashtbl.create 12; delta; widen } in + + (* calculate initial state and environment *) + List.iter (fun ed -> add_case st (pass_cycle st ed)) + (apply_cl_get_all_cases top init_cl); Hashtbl.iter (fun case _ -> st.delta <- case::st.delta) st.env; @@ -323,30 +350,6 @@ end = struct (* - pass_cycle : st -> case_v -> case_v - *) - let pass_cycle st (enum, num) = - let assign_e, assign_n = List.fold_left - (fun (ae, an) (a, b, t) -> match t with - | TEnum _ -> (a, b)::ae, an - | TInt | TReal -> ae, (a, NIdent b)::an) - ([], []) st.cycle in - - let enum = ED.assign enum assign_e in - let num = ND.assign num assign_n in - - List.fold_left - (fun (enum, num) (var, t) -> match t with - | TEnum _ -> ED.forgetvar enum var, num - | TReal | TInt -> enum, ND.forgetvar num var) - (enum, num) st.forget - - let dd_pass_cycle st (v : dd_v) = - let vv = dd_bot v.d_vars in - Hashtbl.iter (fun _ x -> dd_add_case vv (pass_cycle st x)) v.data; - vv - - (* cycle : st -> cl -> dd_v -> dd_v *) let cycle st cl env = @@ -362,10 +365,10 @@ end = struct let set_target_case st env case = List.fold_left2 (fun env id v -> - if List.exists (fun (id2, _) -> id2 = "N"^id) st.enum_vars then - dd_apply_econs env (E_EQ, "N"^id, EItem v) + if List.exists (fun (id2, _) -> id2 = "L"^id) st.enum_vars then + dd_apply_econs env (E_EQ, id, EItem v) else env) - env st.d_vars case + env st.acc_d_vars case (* do_prog : rooted_prog -> unit @@ -387,7 +390,7 @@ end = struct (print_list Formula_printer.print_id ", ") case; let start = try Hashtbl.find st.env case with Not_found -> assert false in - let start_dd = dd_singleton st.d_vars start in + let start_dd = dd_singleton st.acc_d_vars start in let f i = let i = dd_singleton st.d_vars i in let i' = set_target_case st i case in @@ -422,7 +425,6 @@ end = struct Hashtbl.iter (fun _ q -> add_case st q) j.data) !cases; - if st.opt.verbose_ci then Format.printf "-> @[<hov>%a@]@." print_st st; diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml index 6220a0a..8ea0012 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_cl : conslist; 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,15 @@ end = struct init_env : cmdline_opt -> rooted_prog -> env *) let init_env opt rp = - Format.printf "Vars: @[<hov>%a@]@.@." - (print_list Ast_printer.print_typed_var ", ") - rp.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, 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 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 + let cl = Formula.conslist_of_f f in + let cl_g = Formula.conslist_of_f f_g in + let init_cl = Formula.conslist_of_f init_f in + Format.printf "Cycle conslist:@.%a@.@." Formula_printer.print_conslist cl; let guarantees = Transform.guarantees_of_prog rp in Format.printf "Guarantees:@."; @@ -945,20 +942,32 @@ end = struct Format.printf " %s: %a@." id Formula_printer.print_expr f) guarantees; Format.printf "@."; + + (* add variables from LASTs *) + 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 - 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 "Vars: @[<hov>%a@]@.@." + (print_list Ast_printer.print_typed_var ", ") + 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) + ([], []) all_vars in - 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 @@ -969,6 +978,9 @@ end = struct (List.filter (fun n -> is_suffix n "init") evars)) in let lv_f = lv_f @ (List.map (fun v -> (3.0, ["#BEGIN"; v])) (List.filter (fun n -> is_suffix n "state") evars)) in + let lv_f = lv_f @ + (List.map (fun v -> (0.7, [v; "L"^v])) + (List.filter (fun n -> List.mem ("L"^n) evars) evars)) in let evars_ord = if true then time "FORCE" (fun () -> force_ordering evars lv_f) @@ -995,25 +1007,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_cl; cl; cl_g; guarantees; + cycle; forget } @@ -1094,7 +1098,9 @@ end = struct end in - let init_acc = edd_star_new (edd_bot e.data.ve) e.data in + Format.printf "Calculating initial state...@."; + let init_acc = edd_star_new (edd_bot e.ve) + (pass_cycle e (edd_apply_cl (edd_top e.ve) e.init_cl)) in (* Dump final state *) let acc = ch_it 0 init_acc in @@ -1124,13 +1130,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 +1152,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..0045489 100644 --- a/abstract/formula.ml +++ b/abstract/formula.ml @@ -50,19 +50,26 @@ type bool_expr = | BOr of bool_expr * bool_expr | BNot of bool_expr -let f_and a b = match a, b with - | BConst false, _ | _, BConst false -> BConst false - | BConst true, b -> b - | a, BConst true -> a - | a, b -> BAnd(a, b) +let is_false = function + | BConst false | BNot(BConst true) -> true + | _ -> false +let is_true = function + | BConst true | BNot(BConst false) -> true + | _ -> false + +let f_and a b = + if is_false a || is_false b then BConst false + else if is_true a then b + else if is_true b then a + else 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 - | a, BConst false -> a - | a, b -> BOr(a, b) +let f_or a b = + if is_true a || is_true b then BConst true + else if is_false a then b + else if is_false b then a + else BOr(a, b) let f_e_op op a b = match a, b with | EItem i, EItem j -> BConst (if op = E_EQ then i = j else i <> j) diff --git a/abstract/transform.ml b/abstract/transform.ml index dcb4049..480705f 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) @@ -136,6 +143,7 @@ let rec f_of_neexpr td (node, prefix, clock_scope) where expr = and f_of_bexpr td (node, prefix, clock_scope) where expr = let sub = f_of_bexpr td (node, prefix, clock_scope) in let sub_id = sub (fun x -> x) in + let le = loc_error (snd expr) in match fst expr with | AST_bool_const b -> where (BConst b) | AST_binary_bool(AST_AND, a, b) -> where (f_and (sub_id a) (sub_id b)) @@ -152,7 +160,8 @@ and f_of_bexpr td (node, prefix, clock_scope) where expr = | AST_NE -> E_NE | _ -> type_error "Invalid operator on enumerated values." in f_e_op eop x y - | _ -> invalid_arity "Binary operator") + | [NE _; EE _] | [EE _; NE _] -> le type_error "Invalid arguments for binary operator." + | _ -> le invalid_arity "Binary operator") (AST_tuple [a; b], snd expr)) (* Temporal *) | AST_arrow(a, b) -> @@ -180,7 +189,7 @@ and f_of_bexpr td (node, prefix, clock_scope) where expr = | _ -> assert false in f_of_neexpr td (node, prefix, clock_scope) ff expr - | _ -> type_error "Expected boolean value." + | _ -> le type_error "Expected boolean value." and f_of_expr td (node, prefix, clock_scope) expr = f_of_bexpr td (node, prefix, clock_scope) (fun x -> x) expr @@ -190,40 +199,63 @@ 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) + let rst_code = + 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) + in + let no_rst_code = + 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 + if rst_code = BConst true && no_rst_code = BConst true + then BConst true + else + f_or + (f_and (reset_cond rst_exprs) rst_code) + (f_and (no_reset_cond rst_exprs) no_rst_code) 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 +279,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 +289,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 +355,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,47 +366,97 @@ 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 rst_states = uniq_sorted @@ List.sort compare @@ List.flatten + (List.map (fun (st, _) -> + List.map (fun (_, (id, _), _) -> id) + (List.filter (fun (_, _, rst) -> rst) st.until)) + states) + 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 rst_exprs = + if List.mem st.st_name rst_states then + (f_e_eq (EIdent("L"^node^"/"^aid^"."^st.st_name^".must_reset")) + (EItem bool_true))::rst_exprs + else rst_exprs + 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 cr, cnr = List.partition + (fun i -> List.exists (fun (_, (v, _), x) -> x && v = i) st.until) + rst_states in + let must_reset_c l f = + f_and_list + (List.map + (fun i -> f_e_eq (EIdent (node^"/"^aid^"."^i^".must_reset")) + (EItem (if f i then bool_true else bool_false))) + l) + in let rec aux = function - | [] -> BEnumCons(E_EQ, nstv, EItem st.st_name) + | [] -> + f_and + (must_reset_c cr (fun _ -> false)) + (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, clock_scope) c) - (BEnumCons(E_EQ, nstv, EItem target))) + (f_and + (BEnumCons(E_EQ, nstv, EItem target)) + (must_reset_c cr (fun i -> rst && i = target)))) (f_and (BNot (f_of_expr td (node, prefix, clock_scope) c)) (aux q)) - in f_and st_eq (aux st.until) + in + let trans_code = must_reset_c cnr (fun _ -> false) in + let trans_code = f_and trans_code (aux st.until) in + f_and st_eq trans_code 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))) + if List.length states = 1 then + act_eq + else + 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) + 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 + (f_and_list + (List.map + (fun s -> let n = node^"/"^aid^"."^s^".must_reset" in + f_e_eq (EIdent n) (EIdent ("L"^n))) + rst_states)) + (f_and_list (List.map st_eq_inact states))) in f_and_list (List.map do_eq eqs) @@ -384,77 +466,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 +539,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] + | _ -> []) |