Add ABRO example ; correct interpret bug.

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 =