Delete TODO to use git Issues instead

TODO

@@ -1,8 +0,0 @@
-# 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
-
-# ...

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
 
@@ -77,3 +77,4 @@ type t_ck = base_ck list
 and base_ck = 
     | Base
     | On of base_ck * t_expression
+    | Unknown

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
 
@@ -275,7 +275,7 @@ let cp_equations fmt (eqs, hloc, h) =
 
 (** [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

@@ -95,7 +95,7 @@ let cp_state_frees fmt (iprog, sts) =
         then
           Format.fprintf fmt "\tif (st->aux_states[%d]) {\n\
             \t\tfree_state_%s((t_state_%s*)(st->aux_states[%d]));\n\
-            \t\tfree (st->aux_state[%d]);\n\t}\n%a"
+            \t\tfree (st->aux_states[%d]);\n\t}\n%a"
             idx callee_name callee_name idx
             idx cp_free_aux (i+1, caller_name)
         else Format.fprintf fmt "\tif (st->aux_states[%d])\n\
@@ -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,22 @@ 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)
+  | _, _ -> () (*This should never happen*)
+
 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

@@ -25,8 +25,6 @@ let exec_passes ast verbose debug passes f =
     | [] ->  f ast
     | (n, p) :: passes ->
         verbose (Format.asprintf "Executing pass %s:\n" n);
-        try
-        begin
           match p verbose debug ast with
           | None -> (exit_error ("Error while in the pass "^n^".\n"); exit 0)
           | Some ast -> (
@@ -34,8 +32,6 @@ let exec_passes ast verbose debug passes f =
               (Format.asprintf
                 "Current AST (after %s):\n%a\n" n Lustre_pp.pp_ast ast);
             aux ast passes)
-        end with
-        | _ -> failwith ("The pass "^n^" should have caught me!")
   in
   aux ast passes
 
@@ -44,10 +40,12 @@ 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_merge"; "linearization_when";
       "linearization_pre"; "linearization_tuples"; "linearization_app";
       "ensure_assign_val";
-      "equations_ordering"] in
+      "equations_ordering";
+      "clock_unification"] in
   let sanity_passes = ["sanity_pass_assignment_unicity"; "check_typing"] in
   let usage_msg =
     "Usage: main [-passes p1,...,pn] [-ast] [-verbose] [-debug] \
@@ -85,6 +83,8 @@ let _ =
   List.iter (fun (s, k) -> Hashtbl.add passes_table s k)
     [
       ("remove_if", Passes.pass_if_removal);
+      ("linearization_merge", Passes.pass_merge_lin);
+      ("linearization_when", Passes.pass_when_lin);
       ("linearization_tuples", Passes.pass_linearization_tuples);
       ("linearization_app", Passes.pass_linearization_app);
       ("linearization_pre", Passes.pass_linearization_pre);
@@ -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

@@ -6,6 +6,183 @@ open Utils
 
 
 
+(** [pass_when_lin] linearizes the when construct so that it only appears as
+  * main construction of right members of equations. *)
+let pass_when_lin verbose debug =
+  (* prefix of the fresh variables to use and counter to make them unique. *)
+  let varname_prefix = "_whenlin" in
+  let count = ref 0 in
+  (** Auxiliary function that linearizes an expression. *)
+  let rec aux_expr vars expr toplevel conds =
+    match expr with
+    | EVar _ | EConst _ -> [], vars, expr
+    | EMonOp (t, op, e) ->
+      let eqs, vars, e = aux_expr vars e false conds in
+      eqs, vars, EMonOp (t, op, e)
+    | EBinOp (t, op, e, e') ->
+      let eqs, vars, e = aux_expr vars e false conds in
+      let eqs', vars, e' = aux_expr vars e' false conds in
+      eqs'@eqs, vars, EBinOp (t, op, e, e')
+    | EComp (t, op, e, e') ->
+      let eqs, vars, e = aux_expr vars e false conds in
+      let eqs', vars, e' = aux_expr vars e' false conds in
+      eqs'@eqs, vars, EComp (t, op, e, e')
+    | EReset (t, e, e') ->
+      let eqs, vars, e = aux_expr vars e false conds in
+      let eqs', vars, e' = aux_expr vars e' false conds in
+      eqs'@eqs, vars, EReset (t, e, e')
+    | ETuple (t, l) ->
+      let eqs, vars, l = List.fold_right
+        (fun e (eqs, vars, l) ->
+          let eqs', vars, e = aux_expr vars e false conds in
+          eqs' @ eqs, vars, (e :: l))
+        l ([], vars, []) in
+      eqs, vars, ETuple (t, l)
+    | EApp (t, n, e) ->
+      let eqs, vars, e = aux_expr vars e false conds in
+      eqs, vars, EApp (t, n, e)
+    | ETriOp (t, op, e, e', e'') ->
+      let eqs, vars, e = aux_expr vars e false conds in
+      let eqs', vars, e' = aux_expr vars e' false conds in
+      let eqs'', vars, e'' = aux_expr vars e'' false conds in
+      eqs''@eqs'@eqs, vars, ETriOp (t, op, e, e', e'')
+    | EWhen (t, e, e') ->
+      let eqs, vars, e = aux_expr vars e false conds in
+      let eqs', vars, e' = aux_expr vars e' false (e :: conds) in
+      let e =
+        List.fold_left
+          (fun e e' -> EBinOp ([TBool], BOp_and, e,e'))
+          e conds
+      in
+      if toplevel
+        then
+          eqs'@eqs, vars, EWhen (t, e, e')
+        else
+          begin
+            if List.length t = 1
+              then
+                begin
+                let newvar = Format.sprintf "%s%d" varname_prefix !count in
+                let newvar =
+                  match List.hd t with
+                  | TInt -> IVar newvar
+                  | TBool -> BVar newvar
+                  | TReal -> RVar newvar
+                  in
+                let () = incr count in
+                let vars = (t @ (fst vars), newvar :: (snd vars)) in
+                ((t, [newvar]), EWhen (t, e, e')) :: eqs'@eqs, vars, EVar (t, newvar)
+                end
+              else
+                  raise (PassExn "When should only happen on unary expressions.")
+          end
+  in
+  (** For each node: *)
+  let aux_when_lin node =
+    (** Loop on equations to get additional equations and variables. *)
+    let eqs, vars =
+      List.fold_left
+        (fun (eqs, vars) (patt, expr) ->
+          let eqs', vars, expr = aux_expr vars expr true [] in
+          (patt, expr) :: eqs' @ eqs, vars)
+        ([], node.n_local_vars) node.n_equations
+      in
+    Some { node with n_local_vars = vars; n_equations = eqs }
+  in
+  node_pass aux_when_lin
+
+
+
+(** [pass_merge_lin] linearizes the merges so that they only appear as main
+  * construct of right sides of equations.
+  * This simplifies their handling in next passes and in the C printer. *)
+let pass_merge_lin verbose debug =
+  (* prefix of the fresh variables to use and counter to make them unique. *)
+  let varname_prefix = "_mergelin" in
+  let count = ref 0 in
+  (** Auxiliary function that linearizes an expression. *)
+  let rec aux_expr vars expr toplevel =
+    match expr with
+    | EVar _ | EConst _ -> [], vars, expr
+    | EMonOp (t, op, e) ->
+      let eqs, vars, e = aux_expr vars e false in
+      eqs, vars, EMonOp (t, op, e)
+    | EBinOp (t, op, e, e') ->
+      let eqs, vars, e = aux_expr vars e false in
+      let eqs', vars, e' = aux_expr vars e' false in
+      eqs'@eqs, vars, EBinOp (t, op, e, e')
+    | EComp (t, op, e, e') ->
+      let eqs, vars, e = aux_expr vars e false in
+      let eqs', vars, e' = aux_expr vars e' false in
+      eqs'@eqs, vars, EComp (t, op, e, e')
+    | EReset (t, e, e') ->
+      let eqs, vars, e = aux_expr vars e false in
+      let eqs', vars, e' = aux_expr vars e' false in
+      eqs'@eqs, vars, EReset (t, e, e')
+    | ETuple (t, l) ->
+      let eqs, vars, l = List.fold_right
+        (fun e (eqs, vars, l) ->
+          let eqs', vars, e = aux_expr vars e false in
+          eqs' @ eqs, vars, (e :: l))
+        l ([], vars, []) in
+      eqs, vars, ETuple (t, l)
+    | EApp (t, n, e) ->
+      let eqs, vars, e = aux_expr vars e false in
+      eqs, vars, EApp (t, n, e)
+    | ETriOp (_, TOp_if, _, _, _) ->
+        raise (PassExn "There should no longer be any condition.")
+    | EWhen (t, e, e') ->
+      let eqs, vars, e = aux_expr vars e false in
+      let eqs', vars, e' = aux_expr vars e' false in
+      eqs @ eqs', vars, EWhen (t, e, e')
+    | ETriOp (t, TOp_merge, c, e, e') ->
+      begin
+        if toplevel
+          then
+            begin
+            let eqs, vars, c = aux_expr vars c false in
+            let eqs', vars, e = aux_expr vars e false in
+            let eqs'', vars, e' = aux_expr vars e' false in
+            eqs@eqs'@eqs'', vars, ETriOp (t, TOp_merge, c, e, e')
+            end
+          else
+            begin
+            if List.length t = 1
+              then
+                let newvar = Format.sprintf "%s%d" varname_prefix !count in
+                let newvar =
+                  match List.hd t with
+                  | TInt -> IVar newvar
+                  | TBool -> BVar newvar
+                  | TReal -> RVar newvar
+                  in
+                let () = incr count in
+                let vars = (t @ (fst vars), newvar :: (snd vars)) in
+                let eqs, vars, c = aux_expr vars c false in
+                let eqs', vars, e = aux_expr vars e false in
+                let eqs'', vars, e' = aux_expr vars e' false in
+                ((t, [newvar]), ETriOp (t, TOp_merge, c, e, e')) :: eqs @ eqs' @ eqs'', vars, EVar (t, newvar)
+              else
+                raise (PassExn "Merges should only happen on unary expressions.")
+            end
+      end
+  in
+  (** For each node: *)
+  let aux_merge_lin node =
+    (** Loop on equations to get additional equations and variables. *)
+    let eqs, vars =
+      List.fold_left
+        (fun (eqs, vars) (patt, expr) ->
+          let eqs', vars, expr = aux_expr vars expr true in
+          (patt, expr) :: eqs' @ eqs, vars)
+        ([], node.n_local_vars) node.n_equations
+      in
+    Some { node with n_local_vars = vars; n_equations = eqs }
+  in
+  node_pass aux_merge_lin
+
+
+
 (** [pass_if_removal] replaces the `if` construct with `when` and `merge` ones.
   *
   *     [x1, ..., xn = if c then e_l else e_r;]
@@ -147,6 +324,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 +393,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
@@ -242,7 +421,7 @@ let pass_linearization_pre verbose debug =
                           | [TInt]  -> IVar nvar
                           | [TBool] -> BVar nvar
                           | [TReal] -> RVar nvar
-                          | _ -> failwith "Should not happened." in
+                          | _ -> failwith "Should not happened. (pass_linearization_pre)" in
               let neq_patt: t_varlist = (t, [nvar]) in
               let neq_expr: t_expression = e in
               let vars = varlist_concat (t, [nvar]) vars in
@@ -623,28 +802,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
+                  (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)
+              (List.filter
+                (fun eq -> List.for_all (fun e -> eq <> e) (h :: t)) remaining_equations)
       end
   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 +851,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
@@ -727,7 +926,7 @@ let pass_typing verbose debug ast =
           else None
   in aux ast
 
-let check_automata_validity verbos debug = 
+let check_automata_validity verbose debug = 
   let check_automaton_branch_vars automaton = 
     let (init, states) = automaton in
     let left_side = Hashtbl.create 10 in
@@ -752,78 +951,22 @@ let check_automata_validity verbos debug =
     end
   in
   let aux node = 
+    try
     List.iter check_automaton_branch_vars node.n_automata;
     Some node
+    with
+    | PassExn err -> (verbose err; None)
   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 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,157 +979,273 @@ let automaton_translation debug automaton =
     | [TReal] -> EConst(ty, CReal(0.0))
     | _ -> ETuple(ty, List.map defaults ty)
   in
+  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
       
-  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
-      )
+  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 = 
+        try
+            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 = []}
+        with
+        |PassExn err -> (verbose err; None)
+    in
+  node_pass aux
 
 let clock_unification_pass verbose debug ast = 
 
-  let failure str = raise (PassExn ("Failed to unify clocks: "^str)) in
-    
   let known_clocks = Hashtbl.create 100 in
+  let used = Hashtbl.create 100 in (*keep track of variables that appear on right side of equation*)
+  let changed = ref false in
 
-  let find_clock_var var = 
-      match Hashtbl.find_opt known_clocks var with
-      | None -> 
-        begin
-          match var with
-          | BVar(name)
-          | IVar(name)
-          | RVar(name) -> raise (PassExn ("Cannot find clock of variable "^name) )
-        end
-      | Some c -> c
+  let rec count_not e acc = match e with
+    | EVar([TBool], var) -> acc, e
+    | EConst([TBool], cons) -> acc, e
+    | EMonOp([TBool], MOp_not, e) -> count_not e (acc + 1)
+    | _ -> acc, e
   in
 
-  let rec compute_clock_exp exp = match exp with
-  | EConst(_, _) -> [Base]
-  | EVar(_, var) -> find_clock_var var
-  | EMonOp(_, MOp_pre, _) -> [Base]
-  | EMonOp(_, _, e) -> compute_clock_exp e
+  let verify_when e1 e2 =
+      let n1, var1 = count_not e1 0
+      and n2, var2 = count_not e2 0 in
+      if n1 mod 2 <> n2 mod 2 || var1 <> var2 then
+          raise (PassExn "verify_when failure")
+  in
+
+  let get_var_name var = match var with
+  | RVar(name)
+  | BVar(name)
+  | IVar(name) -> name
+  in
+
+  let rec clk_to_string clk = match clk with
+  | Base -> "Base"
+  | Unknown -> "Unknown"
+  | On(clk, exp) -> 
+          let n, var = count_not exp 0 in
+          let s = if n mod 2 = 1 then "not " else "" in
+          let v = match var with |EVar(_, var) -> get_var_name var | EConst(_, CBool(false)) -> "false" |_ -> "true" in
+          (clk_to_string clk) ^ " on " ^ s ^ v
+  in
+
+  let add_clock var clock = 
+      match Hashtbl.find known_clocks var with
+      | Unknown -> changed := true; (debug ("Found clock for "^(get_var_name var)^": "^(clk_to_string clock))); Hashtbl.replace known_clocks var clock
+      | c when c = clock -> ()
+      | c -> raise (PassExn ("Clock conflict "^(get_var_name var) ^" "^(clk_to_string c) ^ " " ^ (clk_to_string clock)))
+  in
+
+  let rec update_clock exp clk = match exp with
+  | EConst(_, _) -> ()
+  | EVar(_, var) -> add_clock var clk; Hashtbl.replace used var var
+  | EMonOp(_, _, e) -> update_clock e clk
 
   | EComp(_, _, e1, e2)
   | EReset(_, e1, e2)
-  | EBinOp(_, _, e1, e2) -> 
-    begin
-      let c1 = compute_clock_exp e1
-      and c2 = compute_clock_exp e2 in
-      if c1 <> c2 then
-        failure "Binop"
-      else
-        c1
-    end
-  | EWhen(_, e1, e2) -> 
-      begin
-        match compute_clock_exp e1 with
-        | [c1] -> [On (c1, e2)]
-        | _ -> failure "When"
-      end
+  | EBinOp(_, _, e1, e2) -> update_clock e1 clk; update_clock e2 clk
   | ETriOp(_, TOp_merge, e1, e2, e3) ->
-    begin
-      let c1 = compute_clock_exp e1
-      and c2 = compute_clock_exp e2
-      and c3 = compute_clock_exp e3 in
-      match c1, c2, c3 with
-      | [c1], [On(cl2, e2)], [On(cl3, e3)] ->
-          begin
-            if cl2 <> c1 || cl3 <> c1 then
-              failure "Triop clocks"
-            else match e2, e3 with
-            | EMonOp(_, MOp_not, e), _ when e = e3 -> [c1]
-            | _, EMonOp(_, MOp_not, e) when e = e2 -> [c1]
-            | _ -> failure "Triop condition"
-          end
-      | _ -> failure ("Merge format")
-    end
+          update_clock e1 clk;
+          update_clock e2 (On(clk, e1));
+          update_clock e3 (On(clk, EMonOp([TBool], MOp_not, e1)))
   | ETriOp(_, TOp_if, e1, e2, e3) ->
-      let (* Unused: c1 = compute_clock_exp e1
-      and*) c2 = compute_clock_exp e2
-      and c3 = compute_clock_exp e3 in
-      if c2 <> c3 then
-        failure "If clocks"
-      else c2
-
-  | ETuple(_, explist) -> List.concat_map compute_clock_exp explist
-  | EApp(_, node, e) -> 
-      let rec aux_app clk_list = match clk_list with
-      | [] -> raise (PassExn "Node called with no argument provided")
-      | [cl] -> cl
-      | t::q -> if t = (aux_app q) then t else failure "App diff clocks"
-      and mult_clk cl out_list = match out_list with
-      | [] -> []
-      | t::q -> cl::(mult_clk cl q)
-      in
-      mult_clk (aux_app (compute_clock_exp e)) (snd node.n_outputs)
+          (* The 3 expressions should have the same clock *)
+          begin
+          update_clock e1 clk;
+          update_clock e2 clk;
+          update_clock e3 clk
+          end
+  | ETuple(_, explist) -> List.iter (fun e -> update_clock e clk) explist
+  | EApp(_, node, e) -> update_clock e clk
+  | EWhen(_, e1, e2) -> 
+      match clk with
+      | On(clk2, e) -> verify_when e e2; update_clock e1 clk2
+      | _ -> raise (PassExn "Clock unification failure: when")
       in
 
-  let rec compute_eq_clock eq = 
-    let rec step vars clks = match vars, clks with
-    | [], [] -> ()
-    | [], c::q -> raise (PassExn "Mismatch between clock size")
-    | v::t, c::q -> Hashtbl.replace known_clocks v [c]; step t q
-    | l, [] -> raise (PassExn "Mismatch between clock size")
+  let rec propagate_clock eqs =
+    let rec step ((ty, vars), exp)= match vars with
+    | [] -> ()
+    | v::t -> let clk = Hashtbl.find known_clocks v in
+      begin
+      if clk <> Unknown then update_clock exp clk
+      else ();
+      step ((ty, t), exp)
+      end
     in
-    let (_, vars), exp = eq in
-    let clk = compute_clock_exp exp in
-    step vars clk
+    List.iter step eqs
   in
   
+  let rec iter_til_stable eqs = 
+    changed := false;
+    propagate_clock eqs;
+    if !changed then
+        iter_til_stable eqs
+  in
+
+  let check_unification node =
+    let (_, node_inputs) = node.n_inputs in
+    let rec check_vars_aux acc = match acc with
+    | [(v, c)] -> if c = Unknown && (Hashtbl.mem used v) then raise (PassExn ("Clock unification failure: Unkwown clock for "^(get_var_name v))) else c
+    | (v, t)::q -> let c = check_vars_aux q in
+        if c <> t then raise (PassExn "Clock unification failure: Non homogeneous equation") else c
+    | [] -> raise (PassExn "Clock unification failure: empty equation")
+    in
+    let rec check_vars ((ty, vars), exp) acc = match vars with
+    | [] -> let _ = check_vars_aux acc in ()
+    | v::t -> check_vars ((ty, t), exp) ((v, Hashtbl.find known_clocks v)::acc)
+    in
+    let rec check_inputs inputs = match inputs with
+    | [] -> ()
+    | i::q -> let c = Hashtbl.find known_clocks i in
+        match c with
+        | On(_, e) -> let _, var = count_not e 0 in 
+            begin
+            match var with
+            | EConst(_, _) -> ()
+            | EVar(_, var) -> if not (List.mem var node_inputs) then raise (PassExn "Clock unification failure: input clock depends on non input clock")
+                else check_inputs q
+            | _ -> failwith "Should not happen. (clock_unification)"
+            end
+        | _ -> check_inputs q
+    in
+    (*Check that all variables used have a clock
+       and that inputs clocks do not depend on local vars or outputs*)
+    List.iter (fun eq -> check_vars eq []) node.n_equations;
+    check_inputs node_inputs;
+  in
+
+
   let compute_clock_node n = 
     begin
       Hashtbl.clear known_clocks;
-      List.iter (fun v -> Hashtbl.replace known_clocks v [Base]) (
-        snd n.n_inputs); (* Initializing inputs to base clock *)
-      List.iter compute_eq_clock n.n_equations;
-      if not (List.for_all (fun v -> (Hashtbl.find known_clocks v) = [Base]) (
-        snd n.n_outputs)) then failure "Outputs" (*Checking that the node's output are on base clock *)
-      else
+      List.iter (fun v -> Hashtbl.replace known_clocks v Unknown) (
+        snd n.n_inputs); (* Initializing inputs to Unknown clock *)
+      List.iter (fun v -> Hashtbl.replace known_clocks v Unknown) (
+        snd n.n_local_vars); (* Initializing local variables to Unknown clock *)
+      List.iter (fun v -> Hashtbl.replace known_clocks v Base) (
+        snd n.n_outputs); (* Initializing outputs to base clock *)
+          iter_til_stable n.n_equations;
+          (* catch potential errors and test for unification *)
+          check_unification n;
           Some n
     end
   in node_pass compute_clock_node 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)

src/test.node

@@ -16,3 +16,10 @@ let
   tmp = aux (a+b, i);
 tel
 
+node test (u, v: int; c: bool) returns (o: int);
+var x, y: int; b: bool;
+let
+	x = merge c u v;
+	o = 2 * x;
+tel
+

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 main (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/when_merge.node

@@ -0,0 +1,13 @@
+node test (i: real) returns (o: real);
+var x, y: real;
+let
+    x = (1.0 / i) when (i <> 0.0);
+    y = 0.0 when (not (i <> 0.0));
+    o = merge (i <> 0.0) x y;
+tel
+
+node main (i: real) returns (o: real);
+let
+    -- The idea is to pass `0.0` as the input to acknowledge that the division by zero isn't computed.
+    o = test(i);
+tel