diff --git a/compiler/global/modules.ml b/compiler/global/modules.ml
index ac3f309..e728448 100644
--- a/compiler/global/modules.ml
+++ b/compiler/global/modules.ml
@@ -160,6 +160,10 @@ let initialize modul =
   List.iter open_module !default_used_modules
 
 
+let current () = g_env.current_mod
+let select modul = g_env.current_mod <- modul
+
+
 (** {3 Add functions prevent redefinitions} *)
 
 let _check_not_defined env f =
diff --git a/compiler/global/names.ml b/compiler/global/names.ml
index 8496922..da0256d 100644
--- a/compiler/global/names.ml
+++ b/compiler/global/names.ml
@@ -96,7 +96,7 @@ let rec modul_of_string_list = function
 let qualname_of_string s =
   let q_l_n = Misc.split_string s "." in
   match List.rev q_l_n with
-    | [] -> Misc.internal_error "Names"
+    | [] -> (* Misc.internal_error "Names" *)raise Exit
     | n::q_l -> { qual = modul_of_string_list q_l; name = n }
 
 let modul_of_string s =
diff --git a/compiler/heptagon/ctrln/ctrlNbacAsEpt.ml b/compiler/heptagon/ctrln/ctrlNbacAsEpt.ml
index 24c8e68..3ea3dc7 100644
--- a/compiler/heptagon/ctrln/ctrlNbacAsEpt.ml
+++ b/compiler/heptagon/ctrln/ctrlNbacAsEpt.ml
@@ -28,6 +28,7 @@
 (*                                                                     *)
 (***********************************************************************)
 
+open Signature
 open Types
 open Names
 open Idents
@@ -119,6 +120,17 @@ let eqrel: eqrel -> fun_name = function
   | `Eq -> Initial.mk_pervasives "="
   | `Ne -> Initial.mk_pervasives "<>"
 
+let totrel t : totrel -> fun_name = function
+  | `Lt when t = Initial.tfloat -> Initial.mk_pervasives "<"
+  | `Le when t = Initial.tfloat -> Initial.mk_pervasives "<="
+  | `Gt when t = Initial.tfloat -> Initial.mk_pervasives ">"
+  | `Ge when t = Initial.tfloat -> Initial.mk_pervasives ">="
+  | `Lt -> Initial.mk_pervasives "<"
+  | `Le -> Initial.mk_pervasives "<="
+  | `Gt -> Initial.mk_pervasives ">"
+  | `Ge -> Initial.mk_pervasives ">="
+  | #eqrel as r -> eqrel r
+
 let nuop t : nuop -> fun_name = function
   | `Opp when t = Initial.tfloat -> Initial.mk_pervasives "~-."
   | `Opp -> Initial.mk_pervasives "~-"
@@ -161,13 +173,13 @@ let translate_expr gd e =
     | `Buop (op, e) -> mkb (mk_uapp (Efun (buop op)) (tb e))
     | `Bnop (op, e, f, l) -> mkb_bapp ?flag (Efun (bnop op)) tb e f l
     | `Bcmp (re, e, f) -> mkb (mk_bapp (Efun (eqrel re)) (tb e) (tb f))
-    | `Ncmp _ -> assert false
     | `Ecmp (re, e, f) -> mkb (mk_bapp (Efun (eqrel re)) (te e) (te f))
     | `Pcmp (re, e, f) -> mkb (mk_bapp (Efun (eqrel re)) (tp e) (tp f))
+    | `Ncmp (re, e, f) -> mkb_ncmp re e f
     | `Pin (e, f, l) -> mkb_bapp_eq ?flag tp e f l
     | `Bin (e, f, l) -> mkb_bapp_eq ?flag tb e f l
     | `Ein (e, f, l) -> mkb_bapp_eq ?flag te e f l
-    | `BIin _ -> assert false
+    | `BIin _ -> raise (Untranslatable ("bounded Integer membership", flag))
     | #cond as c -> trcond ?flag tb tb c
     | #flag as e -> apply' tb e
   and te ?flag = ignore flag; function
@@ -183,11 +195,15 @@ let translate_expr gd e =
     | `Int i -> mkp Initial.tint (Econst (Initial.mk_static_int i))
     | `Real r -> mkp Initial.tfloat (Econst (Initial.mk_static_float r))
     | `Mpq r -> tn ?flag (`Real (Mpqf.to_float r))
-    | `Bint _ -> assert false
+    | `Bint (s, w, _) -> raise (Untranslatable (Format.asprintf "constant of \
+                                 type %a" print_typ (`Bint (s, w)), flag))
     | `Nuop (op, e) -> mk_nuapp ?flag op e
     | `Nnop (op, e, f, l) -> mk_nnapp ?flag op e f l
     | #cond as c -> trcond ?flag tb tn c
     | #flag as e -> apply' tn e
+  and mkb_ncmp ?flag re e f =
+    let { e_ty } as e = tn ?flag e and f = tn f in
+    mkb (mk_bapp (Efun (totrel e_ty re)) e f)
   and mk_nuapp ?flag op e =
     let { e_ty } as e = tn ?flag e in
     mkp e_ty (mk_uapp (Efun (nuop e_ty op)) e)
@@ -223,18 +239,26 @@ let decl_typs typdefs gd =
 
 (* --- *)
 
-let decl_var_acc gd v t acc =
-  let ident = ident_of_name (Symb.to_string v) in
+let decl_var' gd v id t =
   let vd = {
-    v_ident = ident;
-    v_type = translate_typ gd v t;
+    v_ident = id;
+    v_type = t;
     v_linearity = Linearity.Ltop;
     v_clock = Clocks.Cbase;
     v_last = Var;
     v_loc = Location.no_location;
   } in
-  gd.env <- Env.add ident vd gd.env;
-  gd.var_names <- SMap.add v ident gd.var_names;
+  gd.env <- Env.add id vd gd.env;
+  gd.var_names <- SMap.add v id gd.var_names;
+  vd
+
+let decl_ident gd id t =
+  let v = mk_symb (name id) in
+  decl_var' gd v id t
+
+let decl_symb_acc gd v t acc =
+  let ident = ident_of_name (Symb.to_string v) in
+  let vd = decl_var' gd v ident (translate_typ gd v t) in
   vd :: acc
 
 (* --- *)
@@ -250,7 +274,7 @@ let translate_equ_acc gd v e acc =
 (* --- *)
 
 let block_of_func gd { fni_local_vars; fni_all_specs } =
-  let locals = SMap.fold (decl_var_acc gd) fni_local_vars [] in
+  let locals = SMap.fold (decl_symb_acc gd) fni_local_vars [] in
   let equs = SMap.fold (translate_equ_acc gd) fni_all_specs [] in
   {
     b_local = locals;
@@ -269,26 +293,41 @@ let io_of_func gd { fni_io_vars } =
      List.rev_append (SMap.bindings fnig_output_vars) o)) ([], []) fni_io_vars
   in
   let i = List.sort (fun (a, _) (b, _) -> scmp b a) i in                 (* rev. *)
-  let i = List.fold_left (fun acc (v, t) -> decl_var_acc gd v t acc) [] i in
+  let i = List.fold_left (fun acc (v, t) -> decl_symb_acc gd v t acc) [] i in
   let o = List.sort (fun (a, _) (b, _) -> scmp b a) o in                 (* rev. *)
-  let o = List.fold_left (fun acc (v, t) -> decl_var_acc gd v t acc) [] o in
+  let o = List.fold_left (fun acc (v, t) -> decl_symb_acc gd v t acc) [] o in
   i, o
 
 (* --- *)
 
-let node_of_func gd func =
-  let n_name = gd.qname "func" in
-  enter_node n_name;
+(* /!\ Inputs omitted in the signature w.r.t the Controllable-Nbac model should
+   not appear anywhere in equations... *)
+let io_of_func_match gd { node_inputs; node_outputs } =
+  let decl_arg = function
+    | { a_name = Some n; a_type = ty } -> decl_ident gd (ident_of_name n) ty
+    | _ -> failwith "Missing argument names in signature"
+  in
+  let i = List.map decl_arg node_inputs in
+  let o = List.map decl_arg node_outputs in
+  i, o
+
+(* --- *)
+
+let node_of_func gd ?node_sig n_name func =
+  enter_node n_name;                                                   (* ??? *)
   let fi = gather_func_info func in
-  let n_input, n_output = io_of_func gd fi in
+  let n_input, n_output = match node_sig with
+    | None -> io_of_func gd fi
+    | Some s -> io_of_func_match gd s
+  in
   let block = block_of_func gd fi in
-  {
+  Pnode {
     n_name;
-    n_stateful = false;                                                (* ??? *)
-    n_unsafe = false;                                                  (* ??? *)
+    n_stateful = false;
+    n_unsafe = false;
     n_input;
     n_output;
-    n_contract = None;                                             (* <- TODO *)
+    n_contract = None;                                    (* <- TODO: assume? *)
     n_block = block;
     n_loc = Location.no_location;
     n_params = [];
@@ -297,14 +336,25 @@ let node_of_func gd func =
 
 (* --- *)
 
-let gen_func ~module_name func =
+let gen_func ?node_sig ~node_name func =
   let { fn_typs; fn_decls } = func_desc func in
-  let gd = mk_gen_data module_name (fn_decls:> ('f, 'f var_spec) decls) fn_typs in
-  let typs = decl_typs fn_typs gd in
-  let typs = List.rev_map (fun t -> Ptype t) typs in
-  let node = node_of_func gd func in
+  let modul = modul node_name in
+  let gd = mk_gen_data modul (fn_decls:> ('f, 'f var_spec) decls) fn_typs in
+  let typs = List.map (fun t -> Ptype t) (decl_typs fn_typs gd) in
+  let node = node_of_func gd ?node_sig node_name func in
+  node, typs
+
+(* --- *)
+
+let create_prog modul =
   {
-    p_modname = Module module_name;
+    p_modname = modul;
     p_opened = [];
-    p_desc = List.rev (Pnode node :: typs);
+    p_desc = [];
   }
+
+let add_to_prog e ({ p_desc } as p) =
+  (* TODO: check typ duplicates *)
+  { p with p_desc = List.rev (e :: List.rev p_desc); }
+
+(* --- *)
diff --git a/compiler/main/ctrl2ept.ml b/compiler/main/ctrl2ept.ml
index bcf59df..b425856 100644
--- a/compiler/main/ctrl2ept.ml
+++ b/compiler/main/ctrl2ept.ml
@@ -23,12 +23,12 @@ let abort ?filename n msgs =
 (** File extensions officially understood by the tool, with associated input
     types. *)
 let ityps_alist = [
-  (* "ctrln", `Ctrln; "cn", `Ctrln; *)
   "ctrlf", `Ctrlf; "cf", `Ctrlf;
-  (* "ctrlr", `Ctrlr; "cr", `Ctrlr; *)
+  "ctrls", `Ctrlf; "cs", `Ctrlf; (* No need to discriminate between weaved and
+                                    split functions (for now). *)
 ]
 
-(** Name of official input types as understood by the tool. *)
+(** name of official input types as understood by the tool. *)
 let ityps = List.map fst ityps_alist
 
 let set_input_type r t =
@@ -38,16 +38,31 @@ let set_input_type r t =
 let inputs = ref []
 let output = ref ""
 let input_type = ref None
+let node = ref ""
 
+exception Help
+let usage = "Usage: ctrl2ept [options] { [-i] <filename> | -n <node> } \
+                    [ -- { <filename> } ]"
+let print_vers () =
+  fprintf err_formatter "ctrl2ept, version %s (compiled on %s)@." version date;
+  exit 0
 let anon x = inputs := x :: !inputs
-let options =
+let it = Arg.Symbol (ityps, set_input_type input_type)
+let options = Arg.align
   [
-    "-v",Arg.Set verbose, doc_verbose;
-    "-version", Arg.Unit show_version, doc_version;
-    "-i", Arg.String anon, "<file> ";
-    "-input-type", Arg.Symbol (ityps, set_input_type input_type), "Input file type";
-    "--input-type", Arg.Symbol (ityps, set_input_type input_type), "";
-    "-o", Arg.Set_string output, "<file> ";
+    "-i", Arg.String anon, "<file> Input file (`-' means standard input)";
+    "-input-type", it, " Input file type";
+    "--input-type", it, "";
+    "-o", Arg.Set_string output, "<file> Select output file (`-' means \
+                                  standard output)";
+    "-n", Arg.Set_string node, "<node> Select base input node";
+    "--", Arg.Rest anon, " Treat all remaining arguments as input files";
+    "-where", Arg.Unit locate_stdlib, doc_locate_stdlib;
+    "-stdlib", Arg.String set_stdlib, doc_stdlib;
+    "-v",Arg.Set verbose, " Set verbose mode";
+    "-version", Arg.Unit print_vers, " Print the version of the compiler";
+    "--version", Arg.Unit print_vers, "";
+    "-h", Arg.Unit (fun _ -> raise Help), "";
   ]
 
 (* -------------------------------------------------------------------------- *)
@@ -63,7 +78,7 @@ type out =
 let mk_oc basename =
   {
     out_exec = (fun ext ->
-      let filename = asprintf "%s.%s" basename ext in
+      let filename = asprintf "%s%s" basename ext in
       let oc = open_out filename in
       info "Outputting into `%s'…" filename;
       oc, (fun () -> flush oc; close_out oc));
@@ -101,16 +116,100 @@ let parse_input ?filename (parse: ?filename:string -> _) =
 
 (* -------------------------------------------------------------------------- *)
 
-let handle_ctrlf ?filename mk_oc =
+exception Error of string
+
+(* let hack_filter_inputs = let open AST in function *)
+(*   | `Desc ({ fn_decls = decls } as f) -> *)
+(*       (\* TODO: we should actually _substitute_ these variables with ff in the *)
+(*          definitions; yet I think they are unlikely to appear anywhere in the *)
+(*          controller. *\) *)
+(*       let init_symb = Symb.of_string Ctrln_utils.init_cond_str *)
+(*       and sink_symb = Symb.of_string Ctrln_utils.sink_state_str in *)
+(*       let decls = SMap.remove init_symb decls in *)
+(*       let decls = SMap.remove sink_symb decls in *)
+(*       `Desc { f with fn_decls = decls } *)
+(*   | _ -> failwith "should be given an unchecked function!" *)
+
+let parse_n_gen_ept_node ?filename ?node_name ?node_sig () =
   let name, func = parse_input ?filename CtrlNbac.Parser.Unsafe.parse_func in
-  let name = match name with None -> "ctrlr" | Some n -> n ^"_ctrlr" in
-  let prog = CtrlNbacAsEpt.gen_func ~module_name:name func in
+  let node_name = match node_name with Some n -> n
+    | None -> match name with None -> assert false
+        | Some n -> Names.local_qn (n ^ "_ctrlr")
+  in
+  (* let name = match name with None -> "ctrlr" | Some n -> n ^"_ctrlr" in *)
+  (* let func = hack_filter_inputs func in *)
+  name, CtrlNbacAsEpt.gen_func ~node_name ?node_sig func
+
+let handle_ctrlf ?filename mk_oc =
+  let _, (node, typs) = parse_n_gen_ept_node ?filename () in
+  let prog = CtrlNbacAsEpt.create_prog Names.LocalModule in    (* don't care? *)
+  let prog = List.fold_right CtrlNbacAsEpt.add_to_prog typs prog in
+  let prog = CtrlNbacAsEpt.add_to_prog node prog in
   let oc, close = mk_oc.out_exec "ept" in
   Hept_printer.print oc prog;
   close ()
 
 (* -------------------------------------------------------------------------- *)
 
+let parse_nodename nn = try Names.qualname_of_string nn with
+  | Exit -> raise (Error (sprintf "Invalid node name: `%s'" nn))
+
+let output_prog prog modul =
+  Modules.select modul;
+  let filename = String.uncapitalize (Names.modul_to_string modul) ^ ".ept" in
+  let oc = open_out filename in
+  info "Outputting into `%s'…" filename;
+  Hept_printer.print oc prog;
+  close_out oc
+
+let input_function prog filename node_name node_sig =
+  info "Reading function from `%s'…" filename;
+  let res = parse_n_gen_ept_node ~filename ~node_name ~node_sig () in
+  let node, typs = snd res in
+  let prog = List.fold_right CtrlNbacAsEpt.add_to_prog typs prog in
+  let prog = CtrlNbacAsEpt.add_to_prog node prog in
+  prog
+
+let try_ctrlf nn prog =
+  let node_name = Ctrln_utils.controller_node nn in
+  if Modules.check_value node_name then
+    let filename = Ctrln_utils.ctrlf_for_node nn in
+    let node_sig = Modules.find_value node_name in
+    input_function prog filename node_name node_sig
+  else
+    raise (Error "Unable to load any controller function.")
+
+let try_ctrls nn prog =
+  let rec try_ctrls num prog =
+    let node_name = Ctrln_utils.controller_node ~num nn in
+    if Modules.check_value node_name then
+      let filename = Ctrln_utils.ctrls_for_node nn num in
+      let node_sig = Modules.find_value node_name in
+      let prog = input_function prog filename node_name node_sig in
+      try_ctrls (succ num) prog
+    else
+      prog
+  in
+  try_ctrls 0 prog
+
+let handle_node arg =
+  let nn = parse_nodename arg in
+
+  let mo = Names.modul nn in
+  if mo = Names.Pervasives || mo = Names.LocalModule then
+    raise (Error (sprintf "Invalid node specification: `%s'." arg));
+
+  Initial.initialize Names.Pervasives;
+  info "Loading module of controllers for node %s…" (Names.fullname nn);
+  let om = Ctrln_utils.controller_modul mo in
+  Modules.open_module om;
+  let prog = CtrlNbacAsEpt.create_prog om in
+  let prog = try_ctrls nn prog in
+  let prog = if prog.Heptagon.p_desc = [] then try_ctrlf nn prog else prog in
+  output_prog prog om
+
+(* -------------------------------------------------------------------------- *)
+
 let ityp_name_n_handle = function
   (* | `Ctrln -> "node", handle_ctrln *)
   | `Ctrlf -> "function", handle_ctrlf
@@ -137,11 +236,8 @@ let guesstyp_n_output filename =
     | Not_found ->
         raise (Arg.Bad (sprintf "Cannot guess input type of `%s'" filename))
 
-let handle_input_file ?ityp filename =
-  let ityp, mk_oc = match ityp with
-    | None -> guesstyp_n_output filename
-    | Some ityp -> ityp, snd (guesstyp_n_output filename)
-  in
+let handle_input_file filename =
+  let ityp, mk_oc = guesstyp_n_output filename in
   let itypname, handle = ityp_name_n_handle ityp in
   info "Reading %s from `%s'…" itypname filename;
   handle ~filename mk_oc
@@ -157,10 +253,12 @@ let handle_input_stream = function
 
 (** [main] function to be launched *)
 let main () =
-  Arg.parse options anon errmsg;
+  Arg.parse options anon usage;
   match List.rev !inputs with
+    | [] when !node <> "" -> handle_node !node
     | [] -> handle_input_stream !input_type
-    | lst -> List.iter (handle_input_file ?ityp:!input_type) lst
+    | lst -> (if !node <> "" then handle_node !node;
+             List.iter handle_input_file lst)
 
 (* -------------------------------------------------------------------------- *)
 (** Launch the [main] *)
@@ -168,5 +266,6 @@ let _ =
   try
     main ()
   with
+    | Help -> Arg.usage options usage
     | Errors.Error -> error "aborted."; exit 2
-    | Arg.Bad s | Sys_error s -> error "%s" s; exit 2
+    | Error s | Arg.Bad s | Sys_error s -> error "%s" s; exit 2
diff --git a/compiler/main/heptc.ml b/compiler/main/heptc.ml
index dd9a389..4763329 100644
--- a/compiler/main/heptc.ml
+++ b/compiler/main/heptc.ml
@@ -114,7 +114,9 @@ let compile source_f =
 
 (** [main] function to be launched *)
 let main () =
-  let read_qualname f = Arg.String (fun s -> f (Names.qualname_of_string s)) in
+  let read_qualname f =
+    Arg.String (fun s -> f (try Names.qualname_of_string s with
+      | Exit -> raise (Arg.Bad ("Invalid name: "^ s)))) in
   try
     Arg.parse
       [
diff --git a/compiler/minils/ctrln/ctrlNbacGen.ml b/compiler/minils/ctrln/ctrlNbacGen.ml
index 6224aff..11f6a66 100644
--- a/compiler/minils/ctrln/ctrlNbacGen.ml
+++ b/compiler/minils/ctrln/ctrlNbacGen.ml
@@ -34,6 +34,7 @@
 
 (* -------------------------------------------------------------------------- *)
 
+open Ctrln_utils
 open Signature
 open Types
 open Names
@@ -48,34 +49,56 @@ exception Untranslatable of string                    (* XXX not catched yet! *)
 
 (* --- *)
 
+let tt = mk_bcst' true
+let ff = mk_bcst' false
+
+(* --- *)
+
 (** Private record gathering temporary generation data *)
 type 'f gen_data =
     {
       typdefs: 'f typdefs;
       decls: 'f node_decls;
-      outputs: SSet.t;
+      base: (var_ident * ty) SMap.t;
+      local: (var_ident * ty) SMap.t;
+      contrs: (var_ident * ty) SMap.t;
+      output: IdentSet.t;
       init_cond: 'f bexp;
       init_state: 'f bexp;
       assertion: 'f bexp;
       invariant: 'f bexp;
       (* reachable: bexp; *)
+      remaining_contrs: SSet.t;      (* All controllable inputs that has not yet
+                                        been assigned to a U/C group. *)
+      local_contr_deps: SSet.t SMap.t;         (* All variables that depend on a
+                                                  controllable. *)
+      extra_inputs: SSet.t;
+      uc_groups: (SSet.t * SSet.t) list;
     }
 
 (* --- *)
 
-let tt = mk_bcst' true
-let ff = mk_bcst' false
-let init_cond_str = "__init__"                             (* XXX uniqueness? *)
-and sink_state_str = "__sink__"
-
-let ref_of_typ = function
-  | `Bool -> mk_bref
-  | `Enum _ -> mk_eref
-  | `Int | `Real -> mk_nref
+let mk_gen_data typdefs decls input local output init_cond =
+  {
+    typdefs;
+    decls;
+    base = input;
+    local;
+    contrs = SMap.empty;
+    output;
+    remaining_contrs = SSet.empty;
+    local_contr_deps = SMap.empty;
+    extra_inputs = SSet.empty;
+    uc_groups = [];
+    init_cond;
+    init_state = tt;
+    assertion = tt;
+    invariant = tt;
+  }
 
 (* --- *)
 
-let translate_constr { name } = mk_label & mk_symb name (* XXX use module name (?) *)
+let translate_constr { name } = mk_label & mk_symb name (* XXX use qual name? *)
 let translate_constrs cl = mk_etyp (List.map translate_constr cl)
 
 (* --- *)
@@ -91,18 +114,23 @@ let translate_typ typ = match Modules.unalias_type typ with
   | Tarray _ -> raise & Untranslatable ("array type")
   | Tinvalid -> failwith "Encountered an invalid type!"
 
+let ref_of_ty ty = match translate_typ ty with
+  | `Bool -> mk_bref
+  | `Enum _ -> mk_eref
+  | `Int | `Real -> mk_nref
+
 (* --- *)
 
 let simplify_static_exp se = (Static.simplify QualEnv.empty se).se_desc
 
 let translate_static_bexp se = match simplify_static_exp se with
-  | Sbool true | Sconstructor { qual=Pervasives; name="true" } -> tt
-  | Sbool false | Sconstructor { qual=Pervasives; name="false" } -> ff
+  | Sbool true | Sconstructor { qual = Pervasives; name = "true" } -> tt
+  | Sbool false | Sconstructor { qual = Pervasives; name = "false" } -> ff
   | _ -> failwith ("Boolean static expression expected!")
 
 let translate_static_eexp se = match simplify_static_exp se with
-  | Sconstructor { qual=Pervasives; name="true" as n }
-  | Sconstructor { qual=Pervasives; name="false" as n } ->
+  | Sconstructor { qual = Pervasives; name = "true" as n }
+  | Sconstructor { qual = Pervasives; name = "false" as n } ->
       failwith ("Enum static expression expected! (found `"^n^"')")
   | Sconstructor c -> `Enum (translate_constr c)
   | _ -> failwith ("Enum static expression expected!")
@@ -110,8 +138,8 @@ let translate_static_eexp se = match simplify_static_exp se with
 let translate_static_nexp se = match simplify_static_exp se with
   | Sint v -> `Int v
   | Sfloat v -> `Real v
-  | Sop ({ qual=Pervasives; name="~-" },[{ se_desc=Sint v }]) -> `Int (-v)
-  | Sop ({ qual=Pervasives; name="~-." },[{ se_desc=Sfloat v }]) -> `Real (-.v)
+  | Sop ({ qual = Pervasives; name="~-" },[{ se_desc = Sint v }]) -> `Int (-v)
+  | Sop ({ qual = Pervasives; name="~-." },[{ se_desc=Sfloat v }]) -> `Real (-.v)
   | _ -> failwith ("Numerical static expression expected!")
 
 (* --- *)
@@ -162,15 +190,14 @@ let translate_app ~pref op el =
   in
   match op, List.map (translate_ext ~pref) el with
     | Eequal, [e;f] -> mk_eq e f
-    | Efun { qual=Pervasives; name }, el -> pervasives (name, el)
-    (*  *)
+    | Efun { qual = Pervasives; name }, el -> pervasives (name, el)
     | Eifthenelse, [c;t;e] -> mk_cond c t e
     | _ -> failwith "Unsupported application!"
 
 (** [translate_exp gd e] translates the {e memoryless} expression [e] into its
     Controllable Nbac representation.  *)
-let rec translate_exp ~pref t ({ e_desc = desc; e_ty = ty }) =  (* XXX clock? *)
-  let typ = translate_typ ty in assert (t = typ); match desc with
+let rec translate_exp ~pref ({ e_desc = desc }) =               (* XXX clock? *)
+  match desc with
     | Eextvalue ext -> translate_ext ~pref ext
     | Eapp ({ a_op }, el, _) -> translate_app ~pref a_op el
     | Emerge (v, (_c, e) :: l) ->
@@ -181,7 +208,7 @@ let rec translate_exp ~pref t ({ e_desc = desc; e_ty = ty }) =  (* XXX clock? *)
             (translate_ext ~pref e) x)
           (translate_ext ~pref e)
           l
-    | Ewhen (exp, _, _) -> translate_exp ~pref t exp
+    | Ewhen (exp, _, _) -> translate_exp ~pref exp
     | Efby _ -> failwith "TODO: translate_exp (fby)"
     | Estruct _ -> failwith "TODO: translate_exp (struct)"
     | _ -> failwith "TODO: translate_exp"
@@ -198,7 +225,18 @@ let rec translate_clk ~pref on off = function
 
 (* --- *)
 
-let add_state_var gd v typ exp init =
+let acc_dependencies_on vars deps_on_vars i e = fold_exp_dependencies
+  (fun v s ->
+    if SSet.mem v vars then SSet.add v s
+    else try SSet.union s (SMap.find v deps_on_vars) with
+      | Not_found -> s)
+  e i
+
+(* --- *)
+
+let add_state_var' ~pref gd id ty exp init =
+  let v = pref & mk_symb & name id in
+  let typ = translate_typ ty in
   let mk_init = match typ, init with
     | _,       None   -> (fun b -> b)
     | `Bool,   Some i -> mk_and' (mk_beq' (mk_bref' v) (translate_static_bexp i))
@@ -207,119 +245,299 @@ let add_state_var gd v typ exp init =
   in
   { gd with
     decls = SMap.add v (typ, `State (exp, None), None) gd.decls;
-    init_state = mk_init gd.init_state; }
+    init_state = mk_init gd.init_state; }, v
 
-let add_output_var gd v typ exp = add_state_var gd v typ exp None
+let add_state_var ~pref gd id ty exp init =
+  let gd, v = add_state_var' ~pref gd id ty exp init in
+  { gd with base = SMap.add v (id, ty) gd.base; }
 
-let add_local_var gd v typ exp =
-  { gd with decls = SMap.add v (typ, `Local (exp, None), None) gd.decls; }
+let add_output_var ~pref gd id ty exp =
+  add_state_var' ~pref gd id ty exp None |> fst
+
+
+let add_local_var ~pref gd id ty exp =
+  let v = pref & mk_symb & name id in
+  let typ = translate_typ ty in
+  let ldeps = fold_exp_dependencies (fun v acc ->
+    if SSet.mem v gd.remaining_contrs then SSet.add v acc
+    else try SSet.union acc (SMap.find v gd.local_contr_deps) with
+      | Not_found -> acc)
+    exp
+    SSet.empty
+  in
+  let local_contr_deps = SMap.add v ldeps gd.local_contr_deps in
+  { gd with
+    decls = SMap.add v (typ, `Local (exp, None), None) gd.decls;
+    local_contr_deps; }
+
+let declare_additional_input ~pref gd id =
+  let l = mk_symb & name id in
+  try
+    let v = pref l in
+    let t = SMap.find l gd.local |> snd |> translate_typ in
+    { gd with
+      decls = SMap.add v (t, `Input one, None) gd.decls;
+      extra_inputs = SSet.add v gd.extra_inputs; }
+  with
+    | Not_found ->                                 (* output of the main node. *)
+        assert (IdentSet.mem id gd.output);
+        gd
 
 (* --- *)
 
-let translate_eq ~pref gd ({ eq_lhs = pat;
-                             eq_rhs = { e_desc = exp; e_ty = typ } as rhs;
-                             eq_base_ck = clk }) =
-  let typ = translate_typ typ in
+let close_uc_group gd defined_contrs =
+  let rem = SSet.diff gd.remaining_contrs defined_contrs in
+  let lcd = SMap.map (SSet.inter rem) gd.local_contr_deps in
+  let lcd = SMap.filter (fun _ d -> not (SSet.is_empty d)) lcd in
+  { gd with
+    remaining_contrs = rem;
+    extra_inputs = SSet.empty;
+    local_contr_deps = lcd;
+    uc_groups = (gd.extra_inputs, defined_contrs) :: gd.uc_groups; }
+
+(* --- *)
+
+let pat_ids pat =
+  let rec acc_pat acc = function
+    | Evarpat id -> ((* pref &  *)(* mk_symb & name  *)id) :: acc
+    | Etuplepat pats -> List.fold_left acc_pat acc pats
+  in
+  acc_pat [] pat |> List.rev
+
+let translate_abstract_app ~pref gd pat _f args =
+  let results = pat_ids (* ~pref *) pat in
+  let args = List.map (translate_ext ~pref) args in
+  let gd =
+    (* in case of dependencies on remainging controllable variables, switch to
+       next U/C group. *)
+    let depc = List.fold_left
+      (acc_dependencies_on gd.remaining_contrs gd.local_contr_deps)
+      SSet.empty args
+    in
+    if SSet.is_empty depc then gd else close_uc_group gd depc
+  in
+  (* declare extra inputs. *)
+  (List.fold_left (declare_additional_input ~pref) gd results, [])
+
+(* --- *)
+
+let translate_eq ~pref (gd, equs)
+    ({ eq_lhs = pat;
+       eq_rhs = { e_desc = exp; e_ty = ty } as rhs;
+       eq_base_ck = clk } as eq)
+    =
   match pat with
     | Evarpat id ->
-        begin
-          let v = pref & mk_symb & name id in
-          match exp with
-            | Efby (init, ev) ->
-                let ev = translate_ext ~pref ev in
-                let ev = translate_clk ~pref ev (ref_of_typ typ v) clk in
-                add_state_var gd v typ ev init
-            | _ when SSet.mem v gd.outputs ->
-                add_output_var gd v typ (translate_exp ~pref typ rhs)
-            | _ ->
-                add_local_var gd v typ (translate_exp ~pref typ rhs)
+        begin match exp with
+          | Efby (init, ev) ->
+              let v = pref & mk_symb & name id in
+              let ev = translate_ext ~pref ev in
+              let ev = translate_clk ~pref ev (ref_of_ty ty v) clk in
+              (add_state_var ~pref gd id ty ev init, eq :: equs)
+          | Eapp ({ a_op = (Enode f | Efun f) }, args, None)
+                when f.qual <> Pervasives ->
+              let gd, equs' = translate_abstract_app ~pref gd pat f args in
+              (gd, eq :: equs' @ equs)
+          | _ when IdentSet.mem id gd.output ->
+              (add_output_var ~pref gd id ty (translate_exp ~pref rhs),
+               eq :: equs)
+          | _ ->
+              (add_local_var ~pref gd id ty (translate_exp ~pref rhs),
+               eq :: equs)
+        end
+    | Etuplepat _ ->
+        begin match exp with
+          | Eapp ({ a_op = (Enode f | Efun f) }, args, None)
+                when f.qual <> Pervasives ->
+              let gd, equs' = translate_abstract_app ~pref gd pat f args in
+              (gd, eq :: equs' @ equs)
+          | _ -> failwith "TODO: Minils.Etuplepat construct!"
         end
-    | Etuplepat _ -> failwith "TODO: Minils.Etuplepat!"
 
-let translate_eqs ~pref = List.fold_left (translate_eq ~pref)
+let translate_eqs ~pref acc equs =
+  let gd, equs = List.fold_left (translate_eq ~pref) acc equs in
+  gd, List.rev equs
 
 (* --- *)
 
 let prefix_vars ~pref vars : symb -> symb =
-  let vars = List.fold_left
-    (fun acc { v_ident = id } ->                                (* XXX "_" only? *)
-      let v = mk_symb & name id in
-      SMap.add v (mk_symb ("_" ^ Symb.to_string v)) acc)
-    (SMap.empty) vars
-  in
+  let vars = List.fold_left begin fun acc { v_ident = id } ->
+    let v = mk_symb & name id in
+    SMap.add v (mk_symb ("c_" ^ Symb.to_string v)) acc
+  end (SMap.empty) vars in
   fun p -> pref (try SMap.find p vars with Not_found -> p)
 
+let declare_contr (decls, contrs, vds)
+    ({ v_ident = id; v_type = ty } as vd) rank =
+  let v = mk_symb & name id in
+  SMap.add v (translate_typ ty, `Contr (one, rank, None), None) decls,
+  SMap.add v (id, ty) contrs,
+  vd :: vds
+
 (** Contract translation *)
 let translate_contract ~pref gd
     ({ c_local;           c_eq = equs;
        c_assume = a;      c_enforce = g;
        c_assume_loc = a'; c_enforce_loc = g';
-       c_controllables = cl }) =
-  let declare_contr decls { v_ident = id; v_type = typ } rank =
-    let v = mk_symb & name id in
-    SMap.add v (translate_typ typ, `Contr (AST.one, rank, None), None) decls in
-  let declare_contrs decls cl =
+       c_controllables = cl } as contract) =
+  let declare_contrs acc cl =
     fst & List.fold_left
-      (fun (decls, rank) c -> (declare_contr decls c rank, AST.succ rank))
-      (decls, one) cl
+      (fun (acc, rank) c -> (declare_contr acc c rank, AST.succ rank))
+      (acc, one) cl
   in
 
   let pref = prefix_vars ~pref c_local in
-  let gd = { gd with decls = declare_contrs gd.decls cl } in
-  let gd = translate_eqs ~pref gd equs in
+  let decls, contrs, locals = declare_contrs (gd.decls, SMap.empty, []) cl in
+  let c = SMap.fold (fun v _ -> SSet.add v) contrs SSet.empty in
+  let gd = { gd with decls; contrs; remaining_contrs = c; } in
+  let gd, equs' = translate_eqs ~pref (gd, []) equs in
   let ak = as_bexp & mk_and (translate_ext ~pref a) (translate_ext ~pref a')
   and ok = as_bexp & mk_and (translate_ext ~pref g) (translate_ext ~pref g') in
 
   let gd, ok =
     if !Compiler_options.nosink
     then (gd, ok)
-    else let sink = pref & mk_symb sink_state_str in
-         let ok = `Bexp (mk_bcond' gd.init_cond tt ok) in
-         (add_state_var gd sink `Bool ok None, mk_bref' sink)
+    else let sink = gen_var "" sink_state_str in
+         let sink_expr = mk_bref' & pref & mk_symb & name sink in
+         let ok = `Bexp ((* mk_bcond' gd.init_cond tt *) ok) in
+         (add_state_var ~pref gd sink Initial.tbool ok None, sink_expr)
   in
-  { gd with
-    assertion = mk_and' gd.assertion ak;
-    invariant = mk_and' gd.invariant ok; }
+  let assertion = mk_and' gd.assertion ak
+  and invariant = mk_and' gd.invariant ok in
+  ({ gd with assertion; invariant; }, { contract with c_eq = equs'; }, locals)
+
+(* --- *)
+
+let declare_output s { v_ident = id } =
+  IdentSet.add id s
+
+let declare_input m { v_ident = id; v_type = typ } =
+  SMap.add (mk_symb & name id) (translate_typ typ, `Input one, None) m
+
+let register_var_typ m { v_ident = id; v_type = typ } =
+  SMap.add (mk_symb & name id) (id, typ) m
+
+(* --- *)
+
+let finalize_uc_groups gd =
+  let gd = if SSet.is_empty gd.remaining_contrs then gd else
+      (* switch to last U/C group here, and declare controller call. *)
+      close_uc_group gd gd.remaining_contrs
+  in
+  if SSet.is_empty gd.extra_inputs then gd else
+    { gd with
+      extra_inputs = SSet.empty;
+      uc_groups = (gd.extra_inputs, SSet.empty) :: gd.uc_groups; }
+
+(* Note uc_groups are reversed in gd BEFORE the call to this function. *)
+let assign_uc_groups gd =
+  let gd = finalize_uc_groups gd in
+  let uc_groups = List.rev gd.uc_groups in      (* start from the first group *)
+  let decls, _ = List.fold_left begin fun (decls, group) (u, c) ->
+    let decls = SSet.fold (fun u decls -> match SMap.find u decls with
+      | (t, `Input _, l) ->
+          SMap.add u (t, `Input group, l) decls
+      | _ -> decls) u decls
+    in
+    let decls = SSet.fold (fun c decls -> match SMap.find c decls with
+      | (t, `Contr (_, r, l'), l) ->
+          SMap.add c (t, `Contr (group, r, l'), l) decls
+      | _ -> decls) c decls
+    in
+    decls, AST.succ group
+  end (gd.decls, AST.succ one) (List.tl uc_groups) in
+  { gd with decls; uc_groups }
+
+(* --- *)
+
+let scmp a b = String.compare (Symb.to_string a) (Symb.to_string b)
+
+let var_exp v ty =
+  mk_extvalue ~ty ~clock:Clocks.Cbase ~linearity:Linearity.Ltop (Wvar v)
+
+let decl_arg (v, t) =
+  mk_arg (Some (name v)) t Linearity.Ltop Signature.Cbase
+
+let gen_ctrlf_calls gd node_name equs =
+
+  let equs, _, _ = List.fold_left begin fun (equs, ubase, num) (u, c) ->
+
+    (* Controllable inputs of the current U/C group *)
+    let c = SSet.elements c in
+    let c = List.sort scmp c in                       (* XXX now optional (x) *)
+    let o = List.map (fun v -> SMap.find v gd.contrs) c in
+    let os = List.map decl_arg o in
+    let ov, ot = List.split o in
+    let ov = Etuplepat (List.map (fun v -> Evarpat v) ov) in
+
+    (* Accumulate state variables and all non-controllable inputs from the
+       beginning, plus all controllables from previous U/C groups *)
+    let u = SSet.fold (fun v -> SMap.add v (SMap.find v gd.local)) u ubase in
+    let i = SMap.bindings u in
+    let i = List.sort (fun (a, _) (b, _) -> scmp b a) i in  (* rev. i + ibid (x) *)
+    let is = List.rev_map (fun (_, p) -> decl_arg p) i in
+    let i = List.rev_map (fun (_, (v, t)) -> var_exp v t) i in
+
+    (* Build controller call *)
+    let func_name = controller_node ~num node_name in
+    let app = Eapp (mk_app (Efun func_name), i, None) in
+    let exp = mk_exp ~linearity:Linearity.Ltop Clocks.Cbase (Tprod ot) app in
+    let equ = mk_equation false ov exp in
+
+    (* Declare new node *)
+    let node_sig = Signature.mk_node Location.no_location ~extern:false is os
+      false false [] in
+    Modules.add_value func_name node_sig;
+
+    (* Augment base non-controllble inputs with current controllables *)
+    let u = List.fold_left (fun u v -> SMap.add v (SMap.find v gd.contrs) u) u c in
+
+    (equ :: equs, u, num + 1)
+  end (equs, gd.base, 0) gd.uc_groups in
+
+  equs
 
 (* --- *)
 
 (** Node translation. Note the given node is not expored if it does not comprize a
     contract. *)
-let translate_node typdefs : 'n -> 'n * (name * 'f AST.node) option = function
+let translate_node typdefs : 'n -> 'n * (qualname * 'f AST.node) option = function
   | ({ n_contract = None } as node) -> node, None
-  | ({ n_name; n_input; n_output; n_equs; n_contract = Some contr } as node) ->
-      let declare_output s { v_ident = id } = SSet.add (mk_symb & name id) s in
-      let declare_input decls { v_ident = id; v_type = typ } =
-        SMap.add (mk_symb & name id) (translate_typ typ, `Input one, None)
-          decls in
-
+  | ({ n_name; n_input; n_output; n_local; n_equs;
+       n_contract = Some contr } as node) ->
       let pref p = p in
-      let outputs = List.fold_left declare_output SSet.empty n_output in
+      let local = List.fold_left register_var_typ SMap.empty n_local in
+      let input = List.fold_left register_var_typ SMap.empty n_input in
+      let output = List.fold_left declare_output IdentSet.empty n_output in
       let decls = List.fold_left declare_input SMap.empty n_input in
 
-
       let init_cond_var = mk_symb init_cond_str in
-      let init_cond = mk_bref' init_cond_var in
-      let decls = SMap.add init_cond_var
-        (`Bool, `State (`Bexp ff, None), None) decls in
-      (* let init_cond = tt in *)
+      let init_cond = mk_bref' init_cond_var in    (* XXX what about gd.base? *)
+      let init_cond_spec = (`Bool, `State (`Bexp ff, None), None) in
+      let decls = SMap.add init_cond_var init_cond_spec decls in
 
-      let gd = { typdefs; decls; outputs;
-                 init_cond; init_state = tt;
-                 assertion = tt; invariant = tt; } in
-      let gd = translate_contract ~pref gd contr in
-      let gd = translate_eqs ~pref gd n_equs in
+      let gd = mk_gen_data typdefs decls input local output init_cond in
+      let gd, contract, locals' = translate_contract ~pref gd contr in
+      let gd, equs' = translate_eqs ~pref (gd, []) n_equs in
+      let gd = assign_uc_groups gd in
+      let equs' = gen_ctrlf_calls gd n_name equs' in
 
-      let ctrln_node_desc = {
-        cn_typs = typdefs;
-        cn_decls = gd.decls;
-        cn_init = mk_and' gd.init_state init_cond;
-        cn_assertion = (* mk_or' init_cond  *)gd.assertion;
-        cn_invariant = Some (mk_or' init_cond gd.invariant);
-        cn_reachable = None;
-        cn_attractive = None;
-      } in
-      node, Some (n_name.name, (`Desc ctrln_node_desc : 'f AST.node))
+      let ctrln_node_desc =
+        { cn_typs = typdefs;
+          cn_decls = gd.decls;
+          cn_init = mk_and' gd.init_state init_cond;
+          cn_assertion = (* mk_or' init_cond  *)gd.assertion;
+          cn_invariant = Some (mk_or' init_cond gd.invariant);
+          cn_reachable = None;
+          cn_attractive = None; }
+      and node =
+        { node with
+          n_equs = equs';
+          n_local = List.rev_append locals' n_local;
+          n_contract = Some contract; }
+      in
+
+      (node, Some (n_name, (`Desc ctrln_node_desc : 'f AST.node)))
 
 (* --- *)
 
@@ -330,9 +548,7 @@ let translate_node typdefs : 'n -> 'n * (name * 'f AST.node) option = function
     necessitating controller synthesis), (TODO: and a new Minils program, in
     which those nodes have been transformed so that they "call" their respective
     controller). *)
-let gen ({ p_desc = desc } as p) =
-  (* Highly insprited by Sigalimain.program. *)
-
+let gen ({ p_desc } as p) =
   let _cnp_typs, nodes, descs =
     (* XXX Should we gather all the type definitions before translating any
        node? *)
@@ -347,8 +563,7 @@ let gen ({ p_desc = desc } as p) =
           let typdefs = declare_typ tn typ typdefs in
           (typdefs, nodes, descs)
       | p -> (typdefs, nodes, p :: descs)
-    end (empty_typdefs, [], []) desc
+    end (empty_typdefs, [], []) p_desc
   in
-  (* let cnp_name = Names.modul_to_string p.p_modname *)
   let cnp_nodes = List.rev nodes and p_desc = List.rev descs in
   cnp_nodes, { p with p_desc }
diff --git a/compiler/minils/ctrln/ctrlNbacGen.mli b/compiler/minils/ctrln/ctrlNbacGen.mli
index daab23b..6355d65 100644
--- a/compiler/minils/ctrln/ctrlNbacGen.mli
+++ b/compiler/minils/ctrln/ctrlNbacGen.mli
@@ -31,4 +31,5 @@
 (* Interface documentation is in `ctrlNbacGen.ml' only. *)
 (** *)
 
-val gen: Minils.program -> (string * 'f CtrlNbac.AST.node) list * Minils.program
+val gen: Minils.program ->
+  (Names.qualname * 'f CtrlNbac.AST.node) list * Minils.program
diff --git a/compiler/minils/main/mls_compiler.ml b/compiler/minils/main/mls_compiler.ml
index 9f14ccb..f128167 100644
--- a/compiler/minils/main/mls_compiler.ml
+++ b/compiler/minils/main/mls_compiler.ml
@@ -7,6 +7,7 @@
 (* Adrien Guatto, Parkas, ENS                                          *)
 (* Cedric Pasteur, Parkas, ENS                                         *)
 (* Marc Pouzet, Parkas, ENS                                            *)
+(* Nicolas Berthier, SUMO, INRIA                                       *)
 (*                                                                     *)
 (* Copyright 2012 ENS, INRIA, UJF                                      *)
 (*                                                                     *)
@@ -41,10 +42,10 @@ let pp p = if !verbose then Mls_printer.print stdout p
     output into a file called "f_ctrln/n.nbac" *)
 let gen_n_output_ctrln p =
   let nodes, p = CtrlNbacGen.gen p in
-  let filename = filename_of_name (Names.modul_to_string p.Minils.p_modname) in
-  let dir = clean_dir (build_path (filename ^"_ctrln")) in
+  Ctrln_utils.save_controller_modul_for p.Minils.p_modname;
+  ignore (clean_dir (Ctrln_utils.dirname_for_modul p.Minils.p_modname));
   List.iter begin fun (node_name, node) ->
-    let oc = open_out (dir ^"/"^ node_name ^".ctrln") in
+    let oc = open_out (Ctrln_utils.ctrln_for_node node_name) in
     let fmt = Format.formatter_of_out_channel oc in
     CtrlNbac.AST.print_node ~print_header:print_header_info fmt node;
     close_out oc
@@ -53,12 +54,11 @@ let gen_n_output_ctrln p =
 
 let maybe_ctrln_pass p =
   let ctrln = List.mem "ctrln" !target_languages in
-  let _p = pass "Controllable Nbac generation" ctrln gen_n_output_ctrln p pp in
-  ()
+  pass "Controllable Nbac generation" ctrln gen_n_output_ctrln p pp
 
 ;; ELSE
 
-let maybe_ctrln_pass p = p
+let maybe_ctrln_pass p = None
 
 ;; END
 
@@ -101,20 +101,23 @@ let compile_program p =
       pass "Scheduling" true Schedule.program p pp
   in
 
-  let _p = maybe_ctrln_pass p in
-  (* NB: XXX _p is ignored for now... *)
-
   let z3z = List.mem "z3z" !target_languages in
+  let ctrln = List.mem "ctrln" !target_languages in
+  let ctrl = z3z || ctrln in
+  if z3z && ctrln then
+    warn "ignoring target `ctrln' (incompatible with target `z3z').";
+
+  let p = maybe_ctrln_pass p in
   let p = pass "Sigali generation" z3z Sigalimain.program p pp in
-  (* Re-scheduling after sigali generation *)
+
+  (* Re-scheduling after generation *)
   let p =
     if not !Compiler_options.use_old_scheduler then
-      pass "Scheduling (with minimization of interferences)" z3z Schedule_interf.program p pp
+      pass "Scheduling (with minimization of interferences)" ctrl Schedule_interf.program p pp
     else
-      pass "Scheduling" z3z Schedule.program p pp
+      pass "Scheduling" ctrl Schedule.program p pp
   in
 
-
   (* Memory allocation *)
   let p = pass "Memory allocation" !do_mem_alloc Interference.program p pp in
 
diff --git a/compiler/myocamlbuild.ml b/compiler/myocamlbuild.ml
index 61636e6..1e3e2da 100644
--- a/compiler/myocamlbuild.ml
+++ b/compiler/myocamlbuild.ml
@@ -49,7 +49,8 @@ let df = function
       flag ["ocaml"; "parser" ; "menhir" ; "use_menhir"] (S[A"--explain";
                                                             A"--table"]);
 
-      flag ["ocaml"; "compile" ] (S[A"-w"; A"Ae"; A"-warn-error"; A"PU"; A"-w"; A"-9"]);
+      flag ["ocaml"; "compile" ] (S[A"-w"; A"Ae"; A"-warn-error"; A"PU";
+                                    A"-w"; A"-9-48"]);
 
   | _ -> ()
 
diff --git a/compiler/utilities/_tags b/compiler/utilities/_tags
index 6ba28ef..d3a0c34 100644
--- a/compiler/utilities/_tags
+++ b/compiler/utilities/_tags
@@ -1 +1 @@
-<global> or <minils>:include
+<global> or <minils> or <ctrln>:include
diff --git a/compiler/utilities/ctrln/ctrln_utils.ml b/compiler/utilities/ctrln/ctrln_utils.ml
new file mode 100644
index 0000000..59dc4e9
--- /dev/null
+++ b/compiler/utilities/ctrln/ctrln_utils.ml
@@ -0,0 +1,67 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                             Heptagon                                *)
+(*                                                                     *)
+(* Gwenael Delaval, LIG/INRIA, UJF                                     *)
+(* Leonard Gerard, Parkas, ENS                                         *)
+(* Adrien Guatto, Parkas, ENS                                          *)
+(* Cedric Pasteur, Parkas, ENS                                         *)
+(* Marc Pouzet, Parkas, ENS                                            *)
+(* Nicolas Berthier, SUMO, INRIA                                       *)
+(*                                                                     *)
+(* Copyright 2014 ENS, INRIA, UJF                                      *)
+(*                                                                     *)
+(* This file is part of the Heptagon compiler.                         *)
+(*                                                                     *)
+(* Heptagon is free software: you can redistribute it and/or modify it *)
+(* under the terms of the GNU General Public License as published by   *)
+(* the Free Software Foundation, either version 3 of the License, or   *)
+(* (at your option) any later version.                                 *)
+(*                                                                     *)
+(* Heptagon is distributed in the hope that it will be useful,         *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of      *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the       *)
+(* GNU General Public License for more details.                        *)
+(*                                                                     *)
+(* You should have received a copy of the GNU General Public License   *)
+(* along with Heptagon.  If not, see <http://www.gnu.org/licenses/>    *)
+(*                                                                     *)
+(***********************************************************************)
+open Compiler_utils
+open Names
+
+let dirname_for_modul modul =
+  build_path (filename_of_name (modul_to_string modul) ^ "_ctrln")
+
+let ctrln_for_node { qual; name } =
+  dirname_for_modul qual ^"/"^ name ^".ctrln"
+
+let ctrls_for_node { qual; name } =
+  Printf.sprintf "%s/%s.%d.ctrls" (dirname_for_modul qual) name
+
+let ctrlf_for_node { qual; name } =
+  Printf.sprintf "%s/%s.ctrlf" (dirname_for_modul qual) name
+
+let controller_modul = function
+  | Module n -> Module (n ^ "_ctrls")
+  | QualModule ({ name = n } as q) -> QualModule { q with name = n ^ "_ctrls" }
+  | _ -> failwith "Unexpected module"
+
+let controller_node ?num { qual; name } = match num with
+  | Some num -> { qual = controller_modul qual;
+                 name = Printf.sprintf "%s_ctrlr%d" name num }
+  | None -> { qual = controller_modul qual;
+             name = Printf.sprintf "%s_ctrlr0" name }
+
+let save_controller_modul_for modul =
+  let om = Modules.current () in
+  let cm = controller_modul modul in
+  let epci = String.uncapitalize (Names.modul_to_string cm) ^ ".epci" in
+  Modules.select cm;
+  let oc = open_out_bin epci in
+  output_value oc (Modules.current_module ());
+  close_out oc;
+  Modules.select om
+
+let init_cond_str = "__init__"                             (* XXX uniqueness? *)
+and sink_state_str = "__sink__"
diff --git a/compiler/utilities/global/compiler_options.ml b/compiler/utilities/global/compiler_options.ml
index dbd5536..94f9373 100644
--- a/compiler/utilities/global/compiler_options.ml
+++ b/compiler/utilities/global/compiler_options.ml
@@ -56,7 +56,8 @@ and add_include d =
 (* where is the standard library *)
 let locate_stdlib () =
   print_string (try Sys.getenv "HEPTLIB" with Not_found -> standard_lib);
-  print_newline ()
+  print_newline ();
+  exit 0
 
 let show_version () =
   Format.printf "The Heptagon compiler, version %s (%s)@."