Many things, sorry for the mess.

- Implement two new enumeration domains (they don't bring us much) :
    multi valuation for variables ;
    multi valuation for variables and pairs of variables (not really sure it works)
- Make it so that the number of init/time variables is reduced
      (do not create new init/time variables on node instanciation, only
      inside activate blocks and automaton states)
- Some work on EDD (it is currently broken and does not compile)

1 files changed, 30 insertions, 23 deletions

diff --git a/frontend/typing.ml b/frontend/typing.ml
index 0f19b93..167caea 100644
--- a/frontend/typing.ml
+++ b/frontend/typing.ml
@@ -117,7 +117,26 @@ let node_vars p f nid =
     vars_in_node nid (decls_of_node n)
 
 (*
-    extract_all_vars : prog -> scope -> var list
+    clock_vars : rooted_prog -> scope -> var list
+*)
+let clock_vars rp (node, prefix, _) =
+    let v =
+      if not (rp.no_time_scope (node^"/"))
+      then
+        [
+          false, node^"/"^prefix^"time", TInt;
+          false, "N"^node^"/"^prefix^"time", TInt]
+      else [] in
+    let v =
+      if rp.init_scope (node^"/")
+        then
+          (false, node^"/"^prefix^"init", bool_type)::
+          (false, "N"^node^"/"^prefix^"init", bool_type)::v
+        else v in
+    v
+
+(*
+    extract_all_vars : rooted_prog -> scope -> var list
 
     Extracts all variables with names given according to
     naming convention used here and in transform.ml :
@@ -154,10 +173,9 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars =
         let rec do_branch = function
           | AST_activate_body b ->
             let bvars = vars_in_node node b.act_locals in
-            bvars @
-              extract_all_vars rp
-                (node, b.act_id^".", b.body)
-                (bvars@n_vars)
+            let b_scope = node, b.act_id^".", b.body in
+            bvars @ clock_vars rp b_scope @
+              extract_all_vars rp b_scope (bvars@n_vars)
           | AST_activate_if(c, a, b) ->
             vars_of_expr c @ do_branch a @ do_branch b
         in do_branch b
@@ -167,11 +185,10 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars =
             List.flatten
               (List.map (fun (e, _, _) -> vars_of_expr e) st.until)
           in
+          let st_scope = (node, aid^"."^st.st_name^".", st.body) 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)
+          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
         (false, node^"/"^aid^".state", TEnum st_ids)::
@@ -179,18 +196,6 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars =
         (List.flatten (List.map do_state states))
     in
     let v = List.flatten (List.map vars_of_eq eqs) in
-    let v =
-      if not (rp.no_time_scope (node^"/"))
-      then
-        (false, node^"/"^prefix^"time", TInt)::
-        (false, "N"^node^"/"^prefix^"time", TInt)::v
-      else v in
-    let v =
-      if rp.init_scope (node^"/")
-        then
-          (false, node^"/"^prefix^"init", bool_type)::
-          (false, "N"^node^"/"^prefix^"init", bool_type)::v
-        else v in
     v
 
 
@@ -208,7 +213,6 @@ let root_prog p root no_time_scope init_scope =
         (extract_const_decls p)
     in
 
-    let root_vars = vars_in_node "" (decls_of_node root_node) in
 
     let rp = {
       p; root_scope; root_node;
@@ -219,6 +223,9 @@ let root_prog p root no_time_scope init_scope =
       const_vars;
       all_vars = [] } in
 
-    { rp with all_vars = root_vars @ extract_all_vars rp root_scope root_vars }
+    let root_vars = vars_in_node "" (decls_of_node root_node) in
+    let root_clock_vars = clock_vars rp root_scope in
+
+    { rp with all_vars = root_clock_vars @ root_vars @ extract_all_vars rp root_scope root_vars }