Merge branch 'e-last'

Conflicts:
	abstract/abs_interp.ml
	tests/source/counters.scade

4 files changed, 19 insertions, 30 deletions

diff --git a/frontend/ast.ml b/frontend/ast.ml
index c561cef..d55626d 100644
--- a/frontend/ast.ml
+++ b/frontend/ast.ml
@@ -69,10 +69,6 @@ and  state = {
     st_locals : var_def list;
     body      : eqn ext list;
     until     : transition list;
-    (* these two rst info are determined after parsing, in typing.ml when
-        the variable list is extracted *)
-    mutable i_rst : bool;       (* resettable by S -> S transition *)
-    mutable o_rst : bool;       (* resettable by S' -> S transition *)
 }
 and transition = (expr ext) * (id ext) * bool   (* bool : does it reset ? *)
 
diff --git a/frontend/lexer.mll b/frontend/lexer.mll
index ef40aa7..837ee75 100644
--- a/frontend/lexer.mll
+++ b/frontend/lexer.mll
@@ -88,6 +88,7 @@ rule token = parse
   | const_real   as c { REALVAL c }
   (* spaces, comments *)
   | "(*" { comment lexbuf; token lexbuf }
+  | "/*" { cppcomment lexbuf; token lexbuf }
   | "--" [^ '\n' '\r']* { token lexbuf }
   | newline { new_line lexbuf; token lexbuf }
   | space { token lexbuf }
@@ -98,3 +99,8 @@ and comment = parse
   | "*)" { () }
   | [^ '\n' '\r'] { comment lexbuf }
   | newline { new_line lexbuf; comment lexbuf }
+
+and cppcomment = parse
+  | "*/" { () }
+  | [^ '\n' '\r'] { cppcomment lexbuf }
+  | newline { new_line lexbuf; cppcomment lexbuf }
diff --git a/frontend/parser.mly b/frontend/parser.mly
index 672bb9a..e8a6ecf 100644
--- a/frontend/parser.mly
+++ b/frontend/parser.mly
@@ -126,7 +126,6 @@ state:
     st_locals = v;
     body = b;
     until = until;
-    i_rst = false; o_rst = false; (* calculated later *)
 } }
 
 trans(TT):
diff --git a/frontend/typing.ml b/frontend/typing.ml
index 2859230..883e8e0 100644
--- a/frontend/typing.ml
+++ b/frontend/typing.ml
@@ -129,15 +129,12 @@ let clock_vars rp (node, prefix, _) =
     let v =
       if not (rp.no_time_scope (node^"/"^prefix))
       then
-        [
-          false, node^"/"^prefix^"time", TInt;
-          false, "N"^node^"/"^prefix^"time", TInt]
+        [false, node^"/"^prefix^"time", TInt]
       else [] in
     let v =
       if rp.init_scope (node^"/"^prefix)
         then
-          (false, node^"/"^prefix^"init", bool_type)::
-          (false, "N"^node^"/"^prefix^"init", bool_type)::v
+          (false, node^"/"^prefix^"init", bool_type)::v
         else v in
     v
 
@@ -145,9 +142,7 @@ let clock_vars rp (node, prefix, _) =
     extract_all_vars : rooted_prog -> scope -> var list
 
     Extracts all variables with names given according to
-    naming convention used here and in transform.ml :
-    - pre variables are not prefixed by scope
-    - next values for variables are prefixed by capital N
+    naming convention used here and in transform.ml
 *)
 let rec extract_all_vars rp (node, prefix, eqs) n_vars =
     let vars_of_expr e =
@@ -162,12 +157,9 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars =
         (List.map
           (fun (id, expr) ->
               let id = node^"/"^id in
-              let vd =
-                List.mapi
-                  (fun i t -> false, id^"."^(string_of_int i), t)
-                  (type_expr_vl rp.p n_vars rp.const_vars node expr)
-              in
-              vd @ (List.map (fun (a, x, c) -> (a, "N"^x, c)) vd))
+              List.mapi
+                (fun i t -> false, id^"."^(string_of_int i), t)
+                (type_expr_vl rp.p n_vars rp.const_vars node expr))
           (extract_pre e))
     in
     let vars_of_eq e = match fst e with
@@ -186,17 +178,12 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars =
             vars_of_expr c @ do_branch a @ do_branch b
         in do_branch b
       | AST_automaton (aid, states, ret) ->
-        (* Determine which states can be reset *)
-        let rst_trans = List.flatten
+        let rst_states = List.flatten
             (List.map (fun (st, _) ->
-                List.map (fun (_, (id, _), _) -> (st.st_name, id))
+                List.map (fun (_, (id, _), _) -> id)
                 (List.filter (fun (_, _, rst) -> rst) st.until))
               states)
         in
-        List.iter (fun (st, _) ->
-            st.i_rst <- List.mem (st.st_name, st.st_name) rst_trans;
-            st.o_rst <- List.exists (fun (a, b) -> b = st.st_name && a <> b) rst_trans)
-          states;
 
         let do_state (st, _) =
           let tvars =
@@ -205,15 +192,15 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars =
           in
           let st_scope = (node, aid^"."^st.st_name^".", st.body) in
           let svars = vars_in_node node st.st_locals in
-          (if st.i_rst || st.o_rst then
-            [false, node^"/"^aid^"."^st.st_name^".next_reset", bool_type]
+          (if List.mem st.st_name rst_states then
+            [false, node^"/"^aid^"."^st.st_name^".must_reset", bool_type]
           else [])
           @ 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)::
-        (false, "N"^node^"/"^aid^".state", TEnum st_ids)::
+        (false, node^"/"^aid^".next_state", TEnum st_ids)::
         (List.flatten (List.map do_state states))
     in
     let v = List.flatten (List.map vars_of_eq eqs) in
@@ -247,6 +234,7 @@ let root_prog p root no_time_scope init_scope =
     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 }
+    { rp with all_vars = root_clock_vars @
+            root_vars @ extract_all_vars rp root_scope root_vars }