diff options
Diffstat (limited to 'abstract/transform.ml')
| -rw-r--r-- | abstract/transform.ml | 304 |
1 files changed, 184 insertions, 120 deletions
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] + | _ -> []) |