Everything proved !!

1 files changed, 16 insertions, 1 deletions

diff --git a/frontend/typing.ml b/frontend/typing.ml
index a4abfe0..564d91e 100644
--- a/frontend/typing.ml
+++ b/frontend/typing.ml
@@ -158,7 +158,22 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars =
           | AST_activate_if(c, a, b) ->
             vars_of_expr c @ do_branch a @ do_branch b
         in do_branch b
-      | AST_automaton _ -> not_implemented "extract_all vars automaton"
+      | AST_automaton (aid, states, ret) ->
+        let do_state (st, _) =
+          let tvars =
+            List.flatten
+              (List.map (fun (e, _, _) -> vars_of_expr e) st.until)
+          in
+          let svars = vars_in_node node st.st_locals in
+          svars @ tvars @
+            extract_all_vars rp
+              (node, aid^"."^st.st_name^".", st.body)
+              (tvars@n_vars)
+        in
+        let st_ids = List.map (fun (st, _) -> st.st_name) states in
+        (false, node^"/"^aid^".state", TEnum st_ids)::
+        (false, "N"^node^"/"^aid^".state", TEnum st_ids)::
+        (List.flatten (List.map do_state states))
     in
     let v = List.flatten (List.map vars_of_eq eqs) in
     let v =