diff options
| -rw-r--r-- | abstract/transform.ml | 22 | ||||
| -rw-r--r-- | frontend/ast.ml | 4 | ||||
| -rw-r--r-- | frontend/parser.mly | 1 | ||||
| -rw-r--r-- | frontend/typing.ml | 17 |
4 files changed, 35 insertions, 9 deletions
diff --git a/abstract/transform.ml b/abstract/transform.ml index 7ae54ad..dcb4049 100644 --- a/abstract/transform.ml +++ b/abstract/transform.ml @@ -120,7 +120,7 @@ let rec f_of_neexpr td (node, prefix, clock_scope) where expr = | _ when type_expr td.rp node expr = [bool_type] -> f_or (f_and (f_of_expr td (node, prefix, clock_scope) expr) - (where [EE (EItem bool_true)])) + (where [EE (EItem bool_true)])) (f_and (f_of_expr td (node, prefix, clock_scope) (AST_not(expr), snd expr)) (where [EE (EItem bool_false)])) | _ -> le type_error "Expected numerical/enumerated value" @@ -135,11 +135,12 @@ 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 match fst expr with | AST_bool_const b -> where (BConst b) - | AST_binary_bool(AST_AND, a, b) -> f_and (sub where a) (sub where b) - | AST_binary_bool(AST_OR, a, b) -> f_or (sub where a) (sub where b) - | AST_not(a) -> BNot(sub where a) + | AST_binary_bool(AST_AND, a, b) -> where (f_and (sub_id a) (sub_id b)) + | AST_binary_bool(AST_OR, a, b) -> where (f_or (sub_id a) (sub_id b)) + | AST_not(a) -> where (BNot (sub_id a)) | AST_binary_rel(rel, a, b) -> where (f_of_neexpr td (node, prefix, clock_scope) @@ -175,9 +176,7 @@ and f_of_bexpr td (node, prefix, clock_scope) where expr = | _ when type_expr td.rp node expr = [bool_type] -> let ff = function | [EE x] -> - f_or - (f_and (f_e_eq x (EItem bool_true)) (where (BConst true))) - (f_and (f_e_eq x (EItem bool_false)) (where (BConst false))) + where (f_e_eq x (EItem bool_true)) | _ -> assert false in f_of_neexpr td (node, prefix, clock_scope) ff expr @@ -387,7 +386,14 @@ and f_of_prog rp assume_guarantees = let clock_scope, clock_eq = gen_clock td rp.root_scope true in - f_and clock_eq (f_of_scope true td td.rp.root_scope clock_scope assume_guarantees) + let scope_f = + f_of_scope + true + td td.rp.root_scope + clock_scope + assume_guarantees in + f_and clock_eq scope_f + (* Translate init state into a formula diff --git a/frontend/ast.ml b/frontend/ast.ml index d55626d..c561cef 100644 --- a/frontend/ast.ml +++ b/frontend/ast.ml @@ -69,6 +69,10 @@ 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 e8a6ecf..672bb9a 100644 --- a/frontend/parser.mly +++ b/frontend/parser.mly @@ -126,6 +126,7 @@ 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 46458f2..2859230 100644 --- a/frontend/typing.ml +++ b/frontend/typing.ml @@ -186,6 +186,18 @@ 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 + (List.map (fun (st, _) -> + List.map (fun (_, (id, _), _) -> (st.st_name, 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 = List.flatten @@ -193,7 +205,10 @@ 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 - svars @ tvars @ clock_vars rp st_scope @ + (if st.i_rst || st.o_rst then + [false, node^"/"^aid^"."^st.st_name^".next_reset", bool_type] + else []) + @ svars @ tvars @ clock_vars rp st_scope @ extract_all_vars rp st_scope (tvars@n_vars) in let st_ids = List.map (fun (st, _) -> st.st_name) states in |