Fix a typo in a comment in src/passes.ml

TODO

@@ -1,8 +1,5 @@
 # Parseur
 
- - tests divers et variés
- - support pour un point-virgule optionel en fin de nœud
- - ajout des flottants (= réels)
- - ajout de pre, ->, fby, automates
+ - ajustement des automates
 
 # ...

beamer/code/example_automaton.lus

@@ -1,12 +1,12 @@
 node auto (i: int) returns (o : int);
-var x, y:int;
+var x, y: int;
 let
 	automaton
 	| Incr -> do (o,x) = (0 fby o + 1, 2); until o < 5 then Decr
 	| Decr -> do (o,x) = diagonal_int(0 fby o); until o > 3 then Incr
 tel
 
-node auto (i: int) returns (o: int);
+node auto (i: int) returns (o : int);
 var x, y: int;
 let
 	_s1 = 1 -> (if _s = 1 and o < 5 then 2 else if _s = 2 and o > then 1 else 1);
@@ -14,7 +14,7 @@ let
 tel
 
 node auto (i: int) returns (o : int);
-var x, y:int;
+var x, y: int;
 let
 	automaton
 	| Incr -> do (o,x) = (0 fby o + 1, 2); until o < 5 then Decr

src/ast.ml

@@ -55,7 +55,7 @@ and t_equation = t_varlist * t_expression
 
 and t_eqlist = t_equation list
 
-and t_state = | State of ident * t_eqlist * t_expression * ident
+and t_state = | State of ident * t_eqlist * (t_expression list) * (ident list)
 
 and t_automaton = t_state * t_state list
 

src/ast_to_c.ml

@@ -215,11 +215,11 @@ let cp_prevars fmt (node, h) =
           match Hashtbl.find_opt node_st.nt_map (v, false) with
           | Some (src_array, src_idx) ->
             let (dst_array, dst_idx) = Hashtbl.find node_st.nt_map (v, true) in
-            Format.fprintf fmt "\tstate->%s[%d] = state->%s[%d];\n"
+            Format.fprintf fmt "\t_state->%s[%d] = _state->%s[%d];\n"
               dst_array dst_idx src_array src_idx
           | None -> 
             let (dst_array, dst_idx) = Hashtbl.find node_st.nt_map (v, true) in
-            Format.fprintf fmt "\tstate->%s[%d] = %s;\n"
+            Format.fprintf fmt "\t_state->%s[%d] = %s;\n"
               dst_array dst_idx v
           )
         (List.map Utils.name_of_var l)
@@ -236,11 +236,11 @@ let cp_init_aux_nodes fmt (node, h) =
     | None -> () (** All auxiliary nodes have been initialized *)
     | Some n ->
       begin
-      Format.fprintf fmt "%a\t\tif(!state->is_reset) {\n\
-          \t\t\tstate->aux_states[%d] = calloc (1, sizeof (%s));\n\
+      Format.fprintf fmt "%a\t\tif(!_state->is_reset) {\n\
+          \t\t\t_state->aux_states[%d] = calloc (1, sizeof (%s));\n\
           \t\t}\n\
-          \t\t((%s*)(state->aux_states[%d]))->is_init = true;\n\
-          \t\t((%s*)(state->aux_states[%d]))->is_reset = state->is_reset;\n"
+          \t\t((%s*)(_state->aux_states[%d]))->is_init = true;\n\
+          \t\t((%s*)(_state->aux_states[%d]))->is_reset = _state->is_reset;\n"
         aux (node, nst, i-1)
         (i-1) (Format.asprintf "t_state_%s" n.n_name)
         (Format.asprintf "t_state_%s" n.n_name) (i-1)
@@ -252,7 +252,7 @@ let cp_init_aux_nodes fmt (node, h) =
     then ()
     else begin
       Format.fprintf fmt "\t/* Initialize the auxiliary nodes */\n\
-          \tif (state->is_init) {\n%a\t}\n\n\n"
+          \tif (_state->is_init) {\n%a\t}\n\n\n"
         aux (node, nst, nst.nt_count_app)
     end
 
@@ -270,12 +270,12 @@ let cp_equations fmt (eqs, hloc, h) =
     List.map (fun eq -> equation_to_expression (hloc, h, eq)) eqs in
   let main_block = remove_ifnot main_block in
   let main_block = merge_neighbour_ifs main_block in
-  Format.fprintf fmt "\t/*Main code :*/\n%a"
+  Format.fprintf fmt "\t/*Main code:*/\n%a"
     cp_block (main_block, hloc.nt_map)
 
 (** [cp_node] prints a single node *)
 let cp_node fmt (node, h) =
-  Format.fprintf fmt "%a\n{\n%a%a\n\n\tstate->is_init = false;\n%a}\n"
+  Format.fprintf fmt "%a\n{\n%a%a\n\n\t_state->is_init = false;\n%a}\n"
     cp_prototype (node, h)
     cp_init_aux_nodes (node, h)
     cp_equations (node.in_equations, Hashtbl.find h node.in_name, h)
@@ -310,12 +310,12 @@ let dump_var_locations fmt (st: node_states) =
 
 
 (** main function that prints a C-code from a term of type [t_nodelist]. *)
-let ast_to_c verbose debug prog =
+let ast_to_c fmt verbose debug prog =
   verbose "Computation of the node_states";
   let prog_st_types = make_state_types prog in
   debug (Format.asprintf "%a" dump_var_locations prog_st_types);
   let iprog: i_nodelist = ast_to_intermediate_ast prog prog_st_types in
-  Format.printf "%a\n\n%a\n\n%a\n\n/* Nodes: */\n%a%a\n"
+  Format.fprintf fmt "%a\n\n#define BUFFER_SIZE 1024\n\n%a\n\n%a\n\n/* Nodes: */\n%a%a\n"
     cp_includes (Config.c_includes)
     cp_state_types prog_st_types
     cp_state_frees (iprog, prog_st_types)

src/cprint.ml

@@ -124,7 +124,7 @@ let cp_state_frees fmt (iprog, sts) =
 
 
 let cp_var' fmt = function
-  | CVStored (arr, idx) -> Format.fprintf fmt "state->%s[%d]" arr idx
+  | CVStored (arr, idx) -> Format.fprintf fmt "_state->%s[%d]" arr idx
   | CVInput s -> Format.fprintf fmt "%s" s
 
 let cp_var fmt = function
@@ -170,7 +170,7 @@ let cp_prototype fmt (node, h): unit =
   | None -> failwith "This should not happened!"
   | Some nst ->
       begin
-        Format.fprintf fmt "void fn_%s (%s *state, %a)"
+        Format.fprintf fmt "void fn_%s (%s *_state, %a)"
           node.in_name
           nst.nt_name
           cp_varlist node.in_inputs
@@ -211,7 +211,7 @@ let rec cp_value fmt (value, (hloc: (ident * bool, string * int) Hashtbl.t)) =
   in
   match value with
   | CVariable (CVInput s) -> Format.fprintf fmt "%s" s
-  | CVariable (CVStored (arr, idx)) -> Format.fprintf fmt "state->%s[%d]" arr idx
+  | CVariable (CVStored (arr, idx)) -> Format.fprintf fmt "_state->%s[%d]" arr idx
   | CConst (CInt i) -> Format.fprintf fmt "%d" i
   | CConst (CBool b) -> Format.fprintf fmt "%s" (Bool.to_string b)
   | CConst (CReal r) -> Format.fprintf fmt "%f" r
@@ -227,9 +227,9 @@ let rec cp_value fmt (value, (hloc: (ident * bool, string * int) Hashtbl.t)) =
                       end
                     | CVInput n -> n) in
       let (arr, idx) = Hashtbl.find hloc (varname, true) in
-      Format.fprintf fmt "state->%s[%d]" arr idx
+      Format.fprintf fmt "_state->%s[%d]" arr idx
   | CBinOp (BOp_arrow, v, v') ->
-      Format.fprintf fmt "(state->is_init ? (%a) : (%a))"
+      Format.fprintf fmt "(_state->is_init ? (%a) : (%a))"
         cp_value (v, hloc) cp_value (v', hloc)
   | CBinOp (op, v, v') ->
       Format.fprintf fmt "(%a) %s (%a)"
@@ -256,7 +256,7 @@ and cp_expression fmt (expr, hloc) =
   match expr with
   | CAssign (CVStored (arr, idx), value) ->
     begin
-      Format.fprintf fmt "%sstate->%s[%d] = %a;\n"
+      Format.fprintf fmt "%s_state->%s[%d] = %a;\n"
         prefix arr idx cp_value (value, hloc)
     end
   | CAssign (CVInput _, _) -> failwith "never assign an input."
@@ -270,14 +270,14 @@ and cp_expression fmt (expr, hloc) =
       let h_out = aux_node_st.nt_output_map in
       Format.fprintf fmt "%sfn_%s(%s, %a);\n"
         prefix fn
-        (Format.asprintf "state->aux_states[%d]" (nb-1))
+        (Format.asprintf "_state->aux_states[%d]" (nb-1))
         cp_varlist' argl;
       let _ = List.fold_left
         (fun i var ->
           match var with
           | CVStored (arr, idx) ->
             let (arr', idx') = Hashtbl.find h_out i in
-            Format.fprintf fmt "%sstate->%s[%d] = ((%s*)(state->aux_states[%d]))->%s[%d];\n"
+            Format.fprintf fmt "%s_state->%s[%d] = ((%s*)(_state->aux_states[%d]))->%s[%d];\n"
               prefix arr idx
               aux_node_st.nt_name (nb-1)
               arr' idx';
@@ -288,8 +288,8 @@ and cp_expression fmt (expr, hloc) =
   | CReset (node_name, i, v, b) ->
     begin
       Format.fprintf fmt "\tif (%a) {\n\
-        \t\t((t_state_%s*)(state->aux_states[%d]))->is_init = true;\n\
-        \t\t((t_state_%s*)(state->aux_states[%d]))->is_reset = true;\n\
+        \t\t((t_state_%s*)(_state->aux_states[%d]))->is_init = true;\n\
+        \t\t((t_state_%s*)(_state->aux_states[%d]))->is_reset = true;\n\
         \t}\n\
         %a\n"
         cp_value (v, hloc)
@@ -389,7 +389,7 @@ let cp_main_fn fmt (prog, sts) =
           else Format.fprintf fmt "%s%a")
         (match h with
         | IVar _ -> "%d"
-        | BVar _ -> "%c"
+        | BVar _ -> "%hd"
         | RVar _ -> "%f")
         cp_printf_str (true, t)
     in
@@ -397,7 +397,7 @@ let cp_main_fn fmt (prog, sts) =
       match Hashtbl.find_opt h i with
       | None -> ()
       | Some (s, i) ->
-        Format.fprintf fmt ", state.%s[%d]%a"
+        Format.fprintf fmt ", _state.%s[%d]%a"
           s i cp_printf_arg (h, i+1)
     in
     Format.fprintf fmt "\"%a\\n\"%a"
@@ -417,23 +417,31 @@ let cp_main_fn fmt (prog, sts) =
     let main_st = Hashtbl.find  sts "main" in
     if main_st.nt_count_app = 0
       then ()
-      else Format.fprintf fmt "\tfree_state_main(&state);\n"
+      else Format.fprintf fmt "\tfree_state_main(&_state);\n"
   in
   match List.find_opt (fun n -> n.n_name = "main") prog with
   | None -> ()
   | Some node ->
     Format.fprintf fmt "int main (int argc, char **argv)\n\
       {\n%a\n\
-        \tchar _buffer[1024];\n\
-        \tt_state_main state;\n\
-        \tstate.is_init = true;\n\
-        \tstate.is_reset = false;\n\
+        \tchar buffer[BUFFER_SIZE];\n\
+        \tt_state_main _state;\n\
+        \t_state.is_init = true;\n\
+        \t_state.is_reset = false;\n\
         \twhile(true) {\n\
-          \t\tscanf(\"%%s\", _buffer);\n\
-          \t\tif(!strcmp(_buffer, \"exit\")) { break; }\n\
-          \t\tsscanf(_buffer, %a);\n%a\
-          \t\tfn_main(&state, %a);\n\
+          \t\tprintf(\"input: \");\n\
+          \t\tfor(unsigned short idx = 0; idx < BUFFER_SIZE; idx++) {\n\
+          \t\t\tif(idx == (BUFFER_SIZE - 1) || (buffer[idx] = getchar()) == '\\n') {\n\
+          \t\t\t\tbuffer[idx] = '\\0';\n\
+          \t\t\t\tbreak;\n\
+          \t\t\t}\n\
+          \t\t}\n\
+          \t\tif(!strcmp(buffer, \"exit\")) { break; }\n\
+          \t\tsscanf(buffer, %a);\n%a\
+          \t\tfn_main(&_state, %a);\n\
+          \t\tprintf(\"output: \");\n\
           \t\tprintf(%a);\n\
+          \t\tprintf(\"\\n\");\n\
         \t}\n\
         %a\treturn EXIT_SUCCESS;\n\
       }\n"

src/lustre_pp.ml

@@ -153,14 +153,21 @@ let rec pp_automata fmt: t_automaton list -> unit = function
       pp_translist trans
       pp_automata tail
 
+and pp_nexts fmt: t_expression list * string list -> unit = function
+  | [], [] -> ()
+  | e::exprs, n::nexts -> 
+      Format.fprintf fmt "if %a then %s else %a"
+      pp_expression e
+      n
+      pp_nexts (exprs, nexts)
+
 and pp_translist fmt: t_state list -> unit = function
   | [] -> ()
   | State(name, eqs, cond, next)::q ->
-      Format.fprintf fmt "\t\t\t|%s -> do\n%a\n\t\t\tdone until %a \t\t\tthen %s\n%a"
+      Format.fprintf fmt "\t\t\t|%s -> do\n%a\n\t\t\tdone until %a \n%a"
       name
       pp_equations eqs
-      pp_expression cond
-      next
+      pp_nexts (cond, next)
       pp_translist q
 
 let pp_node fmt node =

src/main.ml

@@ -44,7 +44,7 @@ let exec_passes ast verbose debug passes f =
 let _ =
   (** Usage and argument parsing. *)
   let default_passes =
-    ["linearization_reset"; "remove_if";
+      ["linearization_reset"; "automata_translation"; "remove_if";
       "linearization_pre"; "linearization_tuples"; "linearization_app";
       "ensure_assign_val";
       "equations_ordering"] in
@@ -157,6 +157,13 @@ let _ =
     else (
       if !nopopt
         then (fun _ -> ())
-        else Ast_to_c.ast_to_c print_verbose print_debug)
+        else
+        (
+            let oc = open_out !output_file in
+            let fmt = Format.make_formatter
+                  (Stdlib.output_substring oc)
+                  (fun () -> Stdlib.flush oc) in
+            Ast_to_c.ast_to_c fmt print_verbose print_debug);
+        )
   end
 

src/parser.mly

@@ -436,9 +436,10 @@ ident_comma_list:
 
 transition:
   | CASE IDENT BO_arrow DO equations DONE { 
-      State($2, $5, EConst([TBool], CBool(true)), $2) }
-  | CASE IDENT BO_arrow DO equations UNTIL expr THEN IDENT {
-      State($2, $5, $7, $9)}
+      State($2, $5, [EConst([TBool], CBool(true))], [$2]) }
+  | CASE IDENT BO_arrow DO equations UNTIL next_list {
+      let (exprs, outs) = $7 in
+      State($2, $5, exprs, outs)}
 ;
 
 transition_list:
@@ -446,3 +447,8 @@ transition_list:
   | transition transition_list { $1 :: $2 }
   | /* empty */ {raise(MyParsingError("Empty automaton", current_location()))}
 ;
+
+next_list:
+  | expr THEN IDENT { [$1], [$3] }
+  | next_list ELSE IF expr THEN IDENT { let (exprs, outs) = $1 in $4::exprs, $6::outs }
+;

src/passes.ml

@@ -147,6 +147,7 @@ let pass_if_removal verbose debug =
   node_pass aux_if_removal
 
 
+
 (** [pass_linearization_reset] makes sure that all reset constructs in the program
   * are applied to functions.
   * This is required, since the reset construct is translated into resetting the
@@ -215,6 +216,7 @@ let pass_linearization_reset verbose debug =
   node_pass node_lin
 
 
+
 (** [pass_linearization_pre] makes sure that all pre constructs in the program
   * are applied to variables.
   * This is required, since the pre construct is translated into a variable in
@@ -623,28 +625,45 @@ let rec tpl debug ((pat, exp): t_equation) =
   | ETuple (_, []) -> []
   | _ -> [(pat, exp)]
 
+
+
+(** [pass_eq_reordering] orders the equation such that an equation should not
+  * appear before all equations defining the variables it depends on are. *)
 let pass_eq_reordering verbose debug ast =
+  (** [pick_equations] takes a list of equations and initialized variables.
+    * it either returns:
+    *  - a list of equations in a correct order
+    *  - nothing *)
   let rec pick_equations init_vars eqs remaining_equations =
     match remaining_equations with
-    | [] -> Some eqs
+    | [] -> (* There are no equations left to order: we are done. *) Some eqs
     | _ ->
       begin
+        (** The filter below provides the equations whose dependencies have
+          * already been defined *)
         match List.filter
                 (fun (patt, expr) ->
                   List.for_all
                     (fun v -> List.mem v init_vars)
                     (vars_of_expr expr))
                 remaining_equations with
-        | [] -> raise (PassExn "[equation ordering] The equations cannot be ordered.")
-        | h :: t ->
-            let init_vars =
+        | [] -> (** There are remaining equations to order, but none whose all
+                  * dependencies have already been defined yet.*)
+          raise (PassExn "[equation ordering] The equations cannot be ordered.")
+        | h :: t -> (** [h :: t] is a list of equations whose dependencies have
+                      * all already been defined. *)
+            let init_vars = (* new set of initialized variables *)
               List.fold_left
                 (fun acc vs ->
-                  acc @ (vars_of_patt (fst vs))) init_vars (h :: t) in
-            pick_equations init_vars (eqs@(h :: t))
-              (List.filter (fun eq -> List.for_all (fun e -> eq <> e) (h :: t)) remaining_equations)
+                  (vars_of_patt (fst vs)) @ acc) init_vars (h :: t) in
+            (** The filter below removes the equation  of [h :: t] to those to
+              * the list of equations to be ordered *)
+            pick_equations init_vars (eqs @ (h :: t))
+              (List.filter
+                (fun eq -> List.for_all (fun e -> eq <> e) (h :: t)) remaining_equations)
       end
-    in
+  in
+  (* main function of the (node-)pass. *)
   let node_eq_reorganising  (node: t_node): t_node option =
     let init_vars = List.map name_of_var (snd node.n_inputs) in
     try
@@ -655,8 +674,11 @@ let pass_eq_reordering verbose debug ast =
       end
     with PassExn err -> (verbose err; None)
   in
+  (** iterate the pass over the nodes of the program. *)
   node_pass node_eq_reorganising ast
 
+
+
 let pass_typing verbose debug ast =
   let htbl = Hashtbl.create (List.length ast) in
   let () = debug "[typing verification]" in
@@ -757,73 +779,14 @@ let check_automata_validity verbos debug =
   in
   node_pass aux
 
-let automaton_translation debug automaton = 
-  let gathered = Hashtbl.create 10 in
-  let state_to_int = Hashtbl.create 10 in
-  let add_to_table var exp state = 
-    if Hashtbl.mem gathered var then
-      let res = Hashtbl.find gathered var in
-      Hashtbl.replace gathered var ((state, exp)::res);
-    else
-      Hashtbl.replace gathered var ([(state, exp)])
-  in
-  let rec init_state_translation states c = match states with
-  | [] -> ()
-  | State(name, _, _, _)::q -> 
-      Hashtbl.replace state_to_int name c; (init_state_translation q (c+1))
-  in
-
-  let rec find_state name = 
-    match Hashtbl.find_opt state_to_int name with
-    | None -> failwith "Unknown state in automaton"
-    | Some v -> v
-  in
-
-  let rec equation_pass state : t_eqlist -> unit = function
-    | [] -> ()
-    | (vars, exp)::q -> begin
-      add_to_table vars exp state;
-      equation_pass state q
-    end
-  in
-
-  let flatten_state state = match state with
-  | State(name, eq, cond, next) -> 
-    (* Flattening is not possible
-       for example a branch where x,y = 1, 2 will be unpacked
-       when in another branch x, y = f(z) will not be unpacked
-    *)
-    (*
-    let new_equations = List.flatten
-      begin
-      List.map
-        (tpl debug)
-        eq
-      end in
-    *)
-    equation_pass name eq;
-    State(name, eq, cond, next)
-  in
-
-  let rec transition_eq states s = 
-    match states with
-    | [] -> EVar([TInt], IVar(s))
-    | State(name, eqs, cond, next)::q ->
-        let name = find_state name
-        and next = find_state next in
-        ETriOp([TInt], TOp_if, 
-          EBinOp([TBool], BOp_and, 
-            EComp([TBool], COp_eq,
-              EVar([TInt], IVar(s)),
-              EConst([TInt], CInt(name))
-            ),
-            cond
-          ),
-          EConst([TInt], CInt(next)),
-          transition_eq q s
-        )
-    in
+let automaton_translation debug automaton =
 
+  let id = create_automaton_id () in
+  let automat_name = create_automaton_name id in
+  let new_vars = Hashtbl.create Config.maxvar in
+  let var_seen = Hashtbl.create Config.maxvar in
+  let var_merged = Hashtbl.create Config.maxvar in
+  let state_to_int = Hashtbl.create Config.maxvar in
   let default_constant ty =
     let defaults ty = match ty with
     | TInt  -> EConst([ty], CInt(0))
@@ -836,56 +799,134 @@ let automaton_translation debug automaton =
     | [TReal] -> EConst(ty, CReal(0.0))
     | _ -> ETuple(ty, List.map defaults ty)
   in
-
-  let rec translate_var s v explist ty = match explist with
-  | [] -> default_constant ty
-  | (state, exp)::q -> 
-      ETriOp(Utils.type_exp exp, TOp_if,
-        EComp([TBool], COp_eq, 
-          EVar([TInt], IVar(s)),
-          EConst([TInt], CInt(Hashtbl.find state_to_int state))
-        ),
-        exp,
-        translate_var s v q ty
-      )
+  let get_branch_var var branch = 
+      Format.asprintf "_%s_%s_%d" var branch id in
+  let create_var_name var branch ty = 
+      let s = get_branch_var var branch in
+      Hashtbl.replace new_vars s (var, branch, ty);
+      Hashtbl.add var_seen var (s, branch, ty);
+      s
+  in
+  let get_branch_bool branch = 
+    Format.asprintf "_b_%s_%d" branch id in
+  let create_branch_name branch = 
+      let s = get_branch_bool branch in
+      Hashtbl.replace new_vars s ("", branch, TBool);
+      s
+  in
+  let create_merge_var varname branch ty = 
+      let s = Format.asprintf "_%s_%s_merge_%d" varname branch id in
+      Hashtbl.replace new_vars s (varname, branch, ty);
+      s
+  in
+  let create_next_var branch = 
+      let s = Format.asprintf "_next_%s_%d" branch id in
+      Hashtbl.replace new_vars s ("", branch, TInt);
+      s
+  in
+  let create_type_var_name var branch = match var with
+  | BVar(name) -> create_var_name name branch TBool
+  | IVar(name) -> create_var_name name branch TInt
+  | RVar(name) -> create_var_name name branch TReal
+  in
+  let to_var varname ty = match ty with
+  | TInt  -> IVar(varname)
+  | TBool -> BVar(varname)
+  | TReal -> RVar(varname)
+  in
+  let rec init_state_translation states c = match states with
+  | [] -> ()
+  | State(name, _, _, _)::q -> 
+      Hashtbl.replace state_to_int name c; (init_state_translation q (c+1))
+  in
+  let rec find_state name = 
+    match Hashtbl.find_opt state_to_int name with
+    | None -> failwith "Unknown state in automaton"
+    | Some v -> v
+  in
+  let translate_eqlist eqlist branch = 
+      let aux eq = 
+          let ((ty, vlist), expr ) = eq in 
+            ((ty, List.map2 (fun l ty -> to_var (create_type_var_name l branch) ty ) vlist ty ), 
+                EWhen(type_exp expr, expr, EVar([TBool], to_var (get_branch_bool branch) TBool ))) 
+      in
+      List.map aux eqlist
+  in
+  let rec next_construct exprs nexts = match exprs, nexts with
+  | [], [] -> EConst([TInt], CInt(1))
+  | e::exprs, n::nexts -> ETriOp([TInt], TOp_if, e, EConst([TInt], CInt(find_state n)), next_construct exprs nexts)
+  | _, _ -> failwith "Automata translation: next construct: should not happen"
+  in
+  let state_translation state = 
+      match state with
+      | State( name, equations, expr, next ) ->
+        let b = create_branch_name name in
+        let eqs = translate_eqlist equations name in
+        let bool_expr = EComp([TBool], COp_eq, EVar([TInt], to_var automat_name TInt), EConst([TInt], CInt(find_state name))) in
+        let next_expr = EWhen([TInt], next_construct expr next, EVar([TBool], to_var (get_branch_bool name) TBool)) in
+        (([TBool], [to_var b TBool]), bool_expr)::(([TInt], [to_var (create_next_var name) TInt]), next_expr)::eqs
+  in
+  let rec iter_states states = 
+      match states with
+      | [] -> []
+      | s::q -> (state_translation s) @ (iter_states q)
+  in
+  let combine_one_var varname ty = 
+      let default = default_constant [ty] in
+      let rec merge_branches previous branchlist = match branchlist with
+      | [] -> Hashtbl.replace var_merged varname true ; [(([ty], [to_var varname ty]), previous)]
+      | (var, branch, ty2)::q -> 
+              let merge_var = create_merge_var varname branch ty in
+              (([ty], [to_var merge_var ty]), 
+        ETriOp([ty], TOp_merge, EVar([TBool], to_var (get_branch_bool branch) TBool), EVar([ty], to_var var ty), 
+            EWhen([ty], previous, EMonOp([TBool], MOp_not, EVar([TBool], to_var (get_branch_bool branch) TBool))))) 
+              :: ( merge_branches (EVar([ty], to_var merge_var ty2)) q )
+      in
+      let l = Hashtbl.find_all var_seen varname in
+      merge_branches default l
+      
+  in
+  let combine_var varname = 
+      if Hashtbl.mem var_merged varname then [] 
+      else let (_, _, ty) = Hashtbl.find var_seen varname in combine_one_var varname ty
+  in
+  let rec merge_state states = match states with
+  | [] -> EConst([TInt], CInt(1))
+  | State(name, _, _, _)::q -> 
+          let end_state = merge_state q in
+          let bool_var = EVar([TBool], to_var (get_branch_bool name) TBool) in
+          ETriOp([TInt], TOp_merge, bool_var, EVar([TInt], to_var (create_next_var name) TInt),
+            EWhen([TInt], end_state, EMonOp([TBool], MOp_not, bool_var)))
+  in
+  let extract_new_var (varname, (_, _, ty)) = to_var varname ty in
+  let rec build_type varlist = match varlist with
+  |IVar(_)::q -> TInt::build_type q
+  |BVar(_)::q -> TBool::build_type q
+  |RVar(_)::q -> TReal::build_type q
+  |[] -> []
   in
 
-  let flatten_automaton automaton = 
-    let (init, states) = automaton in
-    (flatten_state init, List.map flatten_state states)
-  in
-  let (init, states) = flatten_automaton automaton in
-  let s = create_automaton_name () in
+  let init, states = automaton in
   init_state_translation states 1;
-  let exp_transition = EBinOp([TInt], BOp_arrow, EConst([TInt], CInt(1)), EMonOp([TInt], MOp_pre, transition_eq states s)) in
-  let new_equations = [(([TInt], [IVar(s)]), exp_transition)] in
-  Hashtbl.fold (fun var explist acc -> (var, translate_var s var explist (fst var))::acc) gathered new_equations, IVar(s)
-
-
-let automata_trans_pass debug (node:t_node) : t_node option=
-
-  let rec aux automaton = match automaton with
-  | [] -> [], [], []
-  | a::q -> 
-      let eq, var = automaton_translation debug a
-      and tail_eq, tail_var, tail_type = aux q in
-      eq@tail_eq, var::tail_var, TInt::tail_type
-  in
-
-  let eqs, vars, new_ty = aux node.n_automata in
-  let ty, loc_vars = node.n_local_vars in
-  Some
-    {
-      n_name = node.n_name;
-      n_inputs = node.n_inputs;
-      n_outputs = node.n_outputs;
-      n_local_vars = (new_ty@ty, vars@loc_vars);
-      n_equations = eqs@node.n_equations;
-      n_automata = []; (* not needed anymore *)
-    }
+  let transition_eq = (([TInt], [IVar(automat_name)]), EBinOp([TInt], BOp_arrow, EConst([TInt], CInt(1)), EMonOp([TInt], MOp_pre, merge_state states))) in
+  let state_eqs = (iter_states states) in
+  let new_eqs = state_eqs @ (List.flatten (List.map combine_var (List.of_seq (Hashtbl.to_seq_keys var_seen)))) in
+  let new_vars = List.map extract_new_var (List.of_seq (Hashtbl.to_seq new_vars)) in
+  (transition_eq)::new_eqs, (TInt::(build_type new_vars), IVar(automat_name)::new_vars)
 
 let automata_translation_pass verbose debug = 
-  node_pass (automata_trans_pass debug)
+    let rec iter_automata autolist = match autolist with
+    | [] -> [], ([], [])
+    | a::q -> let (eqs, (ty, vars)) = automaton_translation debug a in
+                let (eqs_end, (ty_end, vars_end)) = iter_automata q in
+                eqs@eqs_end, (ty@ty_end, vars@vars_end)
+    in
+    let aux node = 
+        let eqs, (ty, vars) = iter_automata node.n_automata in
+        let (ty_old, vars_old) = node.n_local_vars in
+        Some { node with n_local_vars = (ty@ty_old, vars@vars_old); n_equations = node.n_equations@eqs; n_automata = []}
+    in
+  node_pass aux
 
 let clock_unification_pass verbose debug ast = 
 

src/passes_utils.ml

@@ -33,6 +33,9 @@ let expression_pass f: t_nodelist -> t_nodelist option =
 exception PassExn of string
 
 let counter = ref 0
-let create_automaton_name : unit -> string = fun () ->
+let create_automaton_id : unit -> int = fun () ->
     counter := !counter + 1;
-    Format.asprintf "_s%d" (!counter)
+    !counter
+
+let create_automaton_name id = 
+    Format.asprintf "_s%d" (id)

tests/arrow.node

@@ -0,0 +1,4 @@
+node main (i: int) returns (o: int);
+let
+    o = 1 -> 2 -> 3;
+tel

tests/automaton.node

@@ -0,0 +1,22 @@
+node diagonal_int (i: int) returns (o1, o2 : int);
+let
+    (o1, o2) = (i, i);
+tel
+
+node undiag_test (i: int) returns (o : bool);
+var l1, l2: int; l3: int;
+let
+    l3 = (pre (1)) -> 0;
+    (l1, l2) = diagonal_int(i);
+    o = (not (not (l1 = l2))) and (l1 = l2) and true;
+tel
+
+node auto (i: int) returns (o : int);
+var x, y:int;
+let
+    automaton
+    | Incr -> do (o,x) = (0 fby o + 1, 2); until x > 0 then Decr else if x = o then Done
+    | Decr -> do (o,x) = diagonal_int(0 fby o); until x < o then Incr
+	| Done -> do o = pre o; done
+tel
+

tests/counting.node

@@ -0,0 +1,16 @@
+-- count the number of top between two tick
+node counting (tick:bool; top:bool)
+returns (o: int);
+var v, o1: int;
+let o = if tick then v else 0 -> (pre o) + v;
+    v = if top then 1 else 0
+tel;
+
+node main (i: int)
+returns (o: int);
+let
+    -- 0 means no `tick` and no `top`
+    -- 1 means `tick`
+    -- 2 means `top`
+    o = counting(i = 1, i = 2)
+tel;

tests/pre.node

@@ -1,4 +1,4 @@
-node n2 (i: int) returns (o: bool);
+node main (i: int) returns (o: bool);
 let
     o = pre (true and pre( i = pre(pre(i))));
 tel

tests/reset.node

@@ -0,0 +1,15 @@
+-- counter of `top`s until `reset` condition holds
+node counting (tick: bool) returns (o: int);
+var v: int;
+let
+  o = v -> (pre o) + v;
+  v = if tick then 1 else 0
+tel
+
+node main (i: int) returns (o: int);
+let
+  -- 0 means no `top` and no `reset`
+  -- 1 means `top`
+  -- 2 means `reset`
+  o = reset counting(i = 1) every (i = 2);
+tel

tests/test.node

@@ -1,21 +0,0 @@
-node diagonal_int (i: int) returns (o1, o2 : int);
-let
-	(o1, o2) = (i, i);
-tel
-
-node undiag_test (i: int) returns (o : bool);
-var l1, l2: int; l3: int;
-let
-	l3 = (pre (1)) -> 0;
-	(l1, l2) = diagonal_int(i);
-	o = (not (not (l1 = l2))) and (l1 = l2) and true;
-tel
-
-node auto (i: int) returns (o : int);
-var x, y:int;
-let
-	automaton
-	| Incr -> do (o,x) = (0 fby o + 1, 2); done
-	| Decr -> do (o,x) = diagonal_int(0 fby o); done
-tel
-

tests/tuple.node

@@ -1,6 +1,6 @@
 node diagonal_int (i: int) returns (o1, o2 : int);
 let
-	(o1, o2) = (i, i);
+    (o1, o2) = (i, i);
 tel
 
 node main (i: int) returns (o1, o2, o3, o4: int);

tests/when_merge.node

@@ -0,0 +1,14 @@
+node test (i: int) returns (o: int);
+var x, y: int;
+let
+    x = (1 / i) when (i <> 0);
+    y = 0 when (not (i <> 0));
+    o = merge (i <> 0) x y;
+tel
+
+node main (i: int) returns (o: int);
+var garbage: int;
+let
+    garbage = test(0);
+    o = test(1);
+tel