summaryrefslogtreecommitdiff
path: root/interpret
diff options
context:
space:
mode:
Diffstat (limited to 'interpret')
-rw-r--r--interpret/interpret.ml38
1 files changed, 30 insertions, 8 deletions
diff --git a/interpret/interpret.ml b/interpret/interpret.ml
index dd0ffb0..8bdf650 100644
--- a/interpret/interpret.ml
+++ b/interpret/interpret.ml
@@ -243,7 +243,9 @@ end = struct
let do_eq (e, _) = match e with
| AST_assign(_, e) | AST_assume(_, e) | AST_guarantee(_, e) -> do_exp e
| AST_automaton (aid, states, _) ->
- let (init_state, _) = List.find (fun (st, _) -> st.initial) states in
+ let (init_state, _) =
+ try List.find (fun (st, _) -> st.initial) states
+ with Not_found -> error "No initial state for automaton!" in
Hashtbl.replace env.vars (node^"/"^aid^".state") (VState init_state.st_name);
List.iter
(fun (st, _) -> reset_scope env (node, aid^"."^st.st_name^".", st.body))
@@ -317,7 +319,10 @@ end = struct
Hashtbl.replace env.vars (node^"/"^id) (VCalc (needed t)))
vars
| AST_automaton(aid, states, vars) ->
- let asn = match VarMap.find (node^"/"^aid^".state") env.st.save with
+ let asn =
+ match try VarMap.find (node^"/"^aid^".state") env.st.save
+ with Not_found -> assert false
+ with
| VState s -> s
| _ -> assert false
in
@@ -354,22 +359,35 @@ end = struct
do_expr c; do_tree a; do_tree b
in do_tree t
| AST_automaton(aid, states, vars) ->
+ let do_st (st, _) =
+ do_weak_transitions env (node, aid^"."^st.st_name^".", st.body);
+ List.iter (fun (c, _, _) -> do_expr c) st.until
+ in
+ List.iter do_st states;
+
let svn = node^"/"^aid^".state" in
- let stv = VarMap.find svn env.st.save in
+ let stv =
+ try VarMap.find svn env.st.save
+ with Not_found -> assert false
+ in
let new_st =
if is_scope_active env (node, prefix, eqs) then begin
let asn = match stv with
| VState s -> s
| _ -> assert false
in
- let (st, _) = List.find (fun (st, _) -> st.st_name = asn) states in
+ let (st, _) =
+ try List.find (fun (st, _) -> st.st_name = asn) states
+ with Not_found -> assert false in
try
let (_, (next_st,_), rst) = List.find
(fun (c, _, _) -> eval_expr env (node, aid^"."^st.st_name^".") c = [VBool true])
st.until
in
if rst then begin
- let (st, _) = List.find (fun (st, _) -> st.st_name = next_st) states in
+ let (st, _) =
+ try List.find (fun (st, _) -> st.st_name = next_st) states
+ with Not_found -> error "Invalid transition?" in
reset_scope env (node, aid^"."^next_st^".", st.body)
end;
VState(next_st)
@@ -378,7 +396,7 @@ end = struct
end else
stv
in
- Hashtbl.replace env.vars svn new_st
+ Hashtbl.replace env.vars svn new_st;
in
List.iter do_eq eqs
@@ -392,7 +410,9 @@ end = struct
try as_bool (Hashtbl.find env.vars (node^"/"^prefix^"init"))
with
| Not_found ->
- let pre_init = as_bool (VarMap.find (node^"/"^prefix^"init") env.st.save)
+ let pre_init =
+ try as_bool (VarMap.find (node^"/"^prefix^"init") env.st.save)
+ with Not_found -> assert false
in pre_init && (not (is_scope_active env (node, prefix, eqs)))
| Bad_datatype ->
Format.eprintf "%s@."
@@ -430,7 +450,9 @@ end = struct
save_expr save e
| AST_automaton(aid, states, _) ->
let svn = node^"/"^aid^".state" in
- let st = Hashtbl.find env.vars svn in
+ let st =
+ try Hashtbl.find env.vars svn
+ with Not_found -> assert false in
let save = VarMap.add (node^"/"^aid^".state") st save in
List.fold_left (fun save (st, _) ->
let save =