diff --git a/compiler/minils/ctrl-n/ctrlNbac.ml b/compiler/minils/ctrl-n/ctrlNbac.ml
index 7dd3113..0fdfe6a 100644
--- a/compiler/minils/ctrl-n/ctrlNbac.ml
+++ b/compiler/minils/ctrl-n/ctrlNbac.ml
@@ -157,8 +157,9 @@ type process =
       cn_decls: decls;               (** all variable specifications *)
       cn_init: bexp;                 (** initial state specification *)
       cn_assertion: bexp;            (** assertion on environment *)
-      cn_invariance: bexp option;    (** {e invariance} property to enforce *)
-      cn_reachability: bexp option;  (** {e reachability} property to enforce *)
+      cn_invariant: bexp option;     (** {e invariance} property to enforce *)
+      cn_reachable: bexp option;     (** {e reachability} property to enforce *)
+      cn_attractive: bexp option;    (** {e attractivity} property to enforce *)
     }
 
 (** A whole controllable-nbac program contains type definitions and
@@ -176,7 +177,7 @@ type prog =
 (** Building variables *)
 let mk_var s = s
 
-(** Prefixing variables with a string. *)
+(** Prefixing variables with a string *)
 let (^~) = Printf.sprintf "%s%s"
 
 (* -------------------------------------------------------------------------- *)
@@ -198,15 +199,15 @@ type process_infos =
     of various information about [process]. *)
 let gather_info { cn_decls } =
   let empty = VMap.empty in
-  let s, i, c, l, d, f = VMap.fold begin fun v -> function
-    | t, NBstate e -> fun (s,i,c,l,d,f) -> (VMap.add v t s,i,c,l, d,VMap.add v e f)
-    | t, NBlocal e -> fun (s,i,c,l,d,f) -> (s,i,c,VMap.add v t l, VMap.add v e d,f)
-    | t, NBinput   -> fun (s,i,c,l,d,f) -> (s,VMap.add v t i,c,l, d,f)
-    | t, NBcontr p -> fun (s,i,c,l,d,f) -> (s,i,VMap.add v (t,p) c,l, d,f)
+  let s, i, c, l, d, f = VMap.fold begin fun v (t, e) -> match e with
+    | NBstate e -> fun (s,i,c,l,d,f) -> (VMap.add v t s,i,c,l, d,VMap.add v e f)
+    | NBlocal e -> fun (s,i,c,l,d,f) -> (s,i,c,VMap.add v t l, VMap.add v e d,f)
+    | NBinput   -> fun (s,i,c,l,d,f) -> (s,VMap.add v t i,c,l, d,f)
+    | NBcontr p -> fun (s,i,c,l,d,f) -> (s,i,VMap.add v (t,p) c,l, d,f)
   end cn_decls (empty, empty, empty, empty, empty, empty) in
   let cl = VMap.bindings c in
   let cl = List.sort (fun (_, (_, a)) (_, (_, b)) -> compare a b) cl in
-  let cl = List.map (fun (v, (t, _)) -> (v, t)) cl in            (* forger rank *)
+  let cl = List.map (fun (v, (t, _)) -> (v, t)) cl in             (* forget rank *)
   { cni_state_vars = s;
     cni_input_vars = i;
     cni_contr_vars = c; cni_contr_vars' = cl;
@@ -529,8 +530,9 @@ module Printer = struct
     print_cat  fmt "transition" print_trans pi.cni_trans_specs;
     print_cat  fmt "initial" print_predicate process.cn_init;
     print_cat  fmt "assertion" print_predicate process.cn_assertion;
-    print_cao' fmt "invariant" print_predicate process.cn_invariance;
-    print_cao' fmt "reachable" print_predicate process.cn_reachability
+    print_cao' fmt "invariant" print_predicate process.cn_invariant;
+    print_cao' fmt "reachable" print_predicate process.cn_reachable;
+    print_cao' fmt "attractive" print_predicate process.cn_attractive
 
   (** [dumps mk_fmt p] dumps separately each process of program [p] in
       formatters produced calling [mk_fmt] with the process's name. The latter
diff --git a/compiler/minils/ctrl-n/ctrlNbac.mli b/compiler/minils/ctrl-n/ctrlNbac.mli
index a97714d..2e0ad34 100644
--- a/compiler/minils/ctrl-n/ctrlNbac.mli
+++ b/compiler/minils/ctrl-n/ctrlNbac.mli
@@ -97,10 +97,6 @@ type exp =
   | `Nexp of nexp
   ]
 
-(* type pbexp = [ exp | bexp ] *)
-(* type peexp = [ exp | eexp ] *)
-(* type pnexp = [ exp | nexp ] *)
-
 (* -------------------------------------------------------------------------- *)
 (** {3 Nodes & Programs} *)
 
@@ -118,8 +114,9 @@ type process =
       cn_decls: decls;
       cn_init: bexp;
       cn_assertion: bexp;
-      cn_invariance: bexp option;
-      cn_reachability: bexp option;
+      cn_invariant: bexp option;
+      cn_reachable: bexp option;
+      cn_attractive: bexp option;
     }
 type prog =
     {
diff --git a/compiler/minils/ctrl-n/ctrlNbacGen.ml b/compiler/minils/ctrl-n/ctrlNbacGen.ml
index fac76da..653f605 100644
--- a/compiler/minils/ctrl-n/ctrlNbacGen.ml
+++ b/compiler/minils/ctrl-n/ctrlNbacGen.ml
@@ -300,8 +300,9 @@ let translate_node typdefs = function
         cn_decls = gd.decls;
         cn_init = gd.init;
         cn_assertion = mk_or' init_cond gd.assertion;
-        cn_invariance = Some (mk_or' init_cond gd.invariant);
-        cn_reachability = None;
+        cn_invariant = Some (mk_or' init_cond gd.invariant);
+        cn_reachable = None;
+        cn_attractive = None;
       } in
       node, Some ctrln_proc