summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-07-04 09:37:22 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-07-04 09:37:22 +0200
commit8c8765721b5cb2907182a63c562677447df8caea (patch)
tree5d917e0e941c39307618704c95f82ee880b5572c
parentf808eeaf3016f828d71b0f87afb89bb79a869035 (diff)
downloadscade-analyzer-8c8765721b5cb2907182a63c562677447df8caea.tar.gz
scade-analyzer-8c8765721b5cb2907182a63c562677447df8caea.zip
Simplifications && preparation for restart.
-rw-r--r--abstract/transform.ml22
-rw-r--r--frontend/ast.ml4
-rw-r--r--frontend/parser.mly1
-rw-r--r--frontend/typing.ml17
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