diff options
Diffstat (limited to 'interpret/interpret.ml')
| -rw-r--r-- | interpret/interpret.ml | 38 |
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 = |