diff options
| -rw-r--r-- | abstract/formula.ml | 28 | ||||
| -rw-r--r-- | abstract/transform.ml | 79 | ||||
| -rw-r--r-- | frontend/ast.ml | 4 | ||||
| -rw-r--r-- | frontend/parser.mly | 1 | ||||
| -rw-r--r-- | frontend/typing.ml | 11 |
5 files changed, 83 insertions, 40 deletions
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) diff --git a/frontend/ast.ml b/frontend/ast.ml index c561cef..d55626d 100644 --- a/frontend/ast.ml +++ b/frontend/ast.ml @@ -69,10 +69,6 @@ and state = { st_locals : var_def list; body : eqn ext list; until : transition list; - (* these two rst info are determined after parsing, in typing.ml when - the variable list is extracted *) - mutable i_rst : bool; (* resettable by S -> S transition *) - mutable o_rst : bool; (* resettable by S' -> S transition *) } and transition = (expr ext) * (id ext) * bool (* bool : does it reset ? *) diff --git a/frontend/parser.mly b/frontend/parser.mly index 672bb9a..e8a6ecf 100644 --- a/frontend/parser.mly +++ b/frontend/parser.mly @@ -126,7 +126,6 @@ state: st_locals = v; body = b; until = until; - i_rst = false; o_rst = false; (* calculated later *) } } trans(TT): diff --git a/frontend/typing.ml b/frontend/typing.ml index d814bbe..883e8e0 100644 --- a/frontend/typing.ml +++ b/frontend/typing.ml @@ -178,17 +178,12 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars = vars_of_expr c @ do_branch a @ do_branch b in do_branch b | AST_automaton (aid, states, ret) -> - (* Determine which states can be reset *) - let rst_trans = List.flatten + let rst_states = List.flatten (List.map (fun (st, _) -> - List.map (fun (_, (id, _), _) -> (st.st_name, id)) + List.map (fun (_, (id, _), _) -> id) (List.filter (fun (_, _, rst) -> rst) st.until)) states) in - List.iter (fun (st, _) -> - st.i_rst <- List.mem (st.st_name, st.st_name) rst_trans; - st.o_rst <- List.exists (fun (a, b) -> b = st.st_name && a <> b) rst_trans) - states; let do_state (st, _) = let tvars = @@ -197,7 +192,7 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars = in let st_scope = (node, aid^"."^st.st_name^".", st.body) in let svars = vars_in_node node st.st_locals in - (if st.i_rst || st.o_rst then + (if List.mem st.st_name rst_states then [false, node^"/"^aid^"."^st.st_name^".must_reset", bool_type] else []) @ svars @ tvars @ clock_vars rp st_scope @ |