From 1445a2be1e1bd81efa552230a0f11672aa20a92c Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Fri, 4 Jul 2014 11:48:05 +0200 Subject: First implementation of resetting transitions. --- abstract/formula.ml | 28 +++++++++++------- abstract/transform.ml | 79 ++++++++++++++++++++++++++++++++++++++++----------- 2 files changed, 80 insertions(+), 27 deletions(-) (limited to 'abstract') diff --git a/abstract/formula.ml b/abstract/formula.ml index 9c0ff71..0045489 100644 --- a/abstract/formula.ml +++ b/abstract/formula.ml @@ -50,20 +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 - | BNot (BConst true), _ | _, BNot (BConst true) -> 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 1cbc27d..17fd064 100644 --- a/abstract/transform.ml +++ b/abstract/transform.ml @@ -208,17 +208,17 @@ let clock_scope_here (node, prefix, _) = let gen_clock td (node, prefix, _) active rst_exprs = let clock_scope = node^"/"^prefix in let clock_eq = - f_or - (f_and (reset_cond rst_exprs) - (f_and + 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))) - (f_and (no_reset_cond rst_exprs) - (if active then + 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"), @@ -238,7 +238,14 @@ let gen_clock td (node, prefix, _) active rst_exprs = (if td.rp.init_scope clock_scope then f_e_eq (EIdent(clock_scope^"init")) (EIdent ("L"^clock_scope^"init")) - else BConst true))) + 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, rst_exprs), clock_eq @@ -374,6 +381,13 @@ let rec f_of_scope active td (node, prefix, eqs) (clock_scope, rst_exprs as cs) (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 rst_exprs in @@ -386,28 +400,61 @@ let rec f_of_scope active td (node, prefix, eqs) (clock_scope, rst_exprs as cs) let st_eq_act (st, l) = let act_eq = let st_scope = node, aid^"."^st.st_name^".", st.body 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 st_choice_eq (f_and_list (List.map st_eq_act states)) else f_and st_choice_eq - (f_and_list (List.map st_eq_inact states)) + (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) -- cgit v1.2.3