diff --git a/src/plugins/aorai/aorai_dataflow.ml b/src/plugins/aorai/aorai_dataflow.ml
index 13bf13719f7650a0b0c82d1e37f6f30cdcc42a27..35cd5f132a0c47e1abee4185c2c646daeb40e9f6 100644
--- a/src/plugins/aorai/aorai_dataflow.ml
+++ b/src/plugins/aorai/aorai_dataflow.ml
@@ -430,7 +430,7 @@ module Computer(I: Init) = struct
 
   let do_call s f args (state,loops as d) =
     let kf = Globals.Functions.get f in
-    if Data_for_aorai.isIgnoredFunction (Kernel_function.get_name kf)
+    if Data_for_aorai.isIgnoredFunction kf
     then d (* we simply skip ignored functions. *)
     else begin
       set_call_state s state;
@@ -532,7 +532,7 @@ module Computer(I: Init) = struct
 end
 
 let compute_func_aux stack call_site kf init_state =
-  if Data_for_aorai.isIgnoredFunction (Kernel_function.get_name kf) then
+  if Data_for_aorai.isIgnoredFunction kf then
     Aorai_option.fatal "compute_func on function %a which is ignored by Aorai"
       Kernel_function.pretty kf
   else if List.mem_assq kf stack then begin
@@ -620,7 +620,7 @@ let () = compute_func := compute_func_aux
 
 let compute_forward () =
   let kf = Globals.Functions.find_by_name (Kernel.MainFunction.get()) in
-  if Data_for_aorai.isIgnoredFunction (Kernel_function.get_name kf) then
+  if Data_for_aorai.isIgnoredFunction kf then
     Aorai_option.abort "Main function %a is ignored by Aorai"
       Kernel_function.pretty kf;
   let (states,_) = Data_for_aorai.getGraph () in
@@ -757,7 +757,7 @@ struct
 
   let do_call s f state =
     let kf = Globals.Functions.get f in
-    if Data_for_aorai.isIgnoredFunction (Kernel_function.get_name kf)
+    if Data_for_aorai.isIgnoredFunction kf
     then Dataflow2.Default (* we simply skip ignored functions. *)
     else begin
       try
@@ -912,7 +912,7 @@ let filter_init_state restrict initial map acc =
   with Not_found -> acc
 
 let backward_analysis_aux stack kf ret_state =
-  if (Data_for_aorai.isIgnoredFunction (Kernel_function.get_name kf)) then
+  if Data_for_aorai.isIgnoredFunction kf then
     Aorai_option.fatal 
       "Call backward analysis on ignored function %a" Kernel_function.pretty kf
   else if List.memq kf stack then begin
@@ -1002,7 +1002,7 @@ let () = backward_analysis := backward_analysis_aux
 
 let compute_backward () =
   let kf = Globals.Functions.find_by_name (Kernel.MainFunction.get()) in
-  if Data_for_aorai.isIgnoredFunction (Kernel_function.get_name kf) then
+  if Data_for_aorai.isIgnoredFunction kf then
     Aorai_option.abort "Main function %a is ignored by Aorai"
       Kernel_function.pretty kf;
   let final_state = Data_for_aorai.get_kf_return_state kf in
diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index 341fb420f6d0e2636d66fbbcc1c8204cd21bee7b..7615b72d83c5c6ba6554e5cd857ad39a0ec978ee 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -629,6 +629,16 @@ let crosscond_to_exp generated_kf curr_f curr_status loc cond res =
 (** Local copy of the file pointer *)
 let file = ref Cil.dummyFile
 
+let initFunction kf =
+  let fname = Kernel_function.get_name kf in
+  List.iter
+    (fun vi -> set_paraminfo fname vi.vname vi)
+    (Kernel_function.get_formals kf);
+  match (Kernel_function.find_return kf).skind with
+  | Cil_types.Return (Some { enode = Lval (Var vi,NoOffset) },_) ->
+    set_returninfo fname vi (* Add the vi of return stmt *)
+  | exception Kernel_function.No_Statement | _ -> () (* function without returned value *)
+
 (** Copy the file pointer locally in the class in order to ease globals
     management and initializes some tables. *)
 let initFile f =
@@ -636,27 +646,7 @@ let initFile f =
   Data_for_aorai.setCData ();
   (* Adding C variables into our hashtable *)
   Globals.Vars.iter (fun vi _ -> set_varinfo vi.vname vi);
-  Globals.Functions.iter
-    (fun kf ->
-       let fname = Kernel_function.get_name kf in
-       List.iter
-         (fun vi -> set_paraminfo fname vi.vname vi)
-         (Kernel_function.get_formals kf);
-       if not (Data_for_aorai.isIgnoredFunction fname) then
-         begin
-           try
-             let ret  = Kernel_function.find_return kf in
-             match ret.skind with
-             | Cil_types.Return (Some e,_) ->
-               (match e.enode with
-                | Lval (Var vi,NoOffset) ->
-                  set_returninfo fname vi (* Add the vi of return stmt *)
-                | _ -> () (* function without returned value *))
-             | _ -> () (* function without returned value *)
-           with Kernel_function.No_Statement ->
-             Aorai_option.fatal
-               "Don't know what to do with a function declaration"
-         end)
+  Globals.Functions.iter initFunction
 
 (** List of globals awaiting for adding into C file globals *)
 let globals_queue = ref []
@@ -760,6 +750,11 @@ let mk_global_c_enum_type name elements =
 let mk_global_c_initialized_enum name name_enuminfo ini =
   mk_global_c_initialized_vars name (TEnum(get_usedinfo name_enuminfo,[])) ini
 
+let mk_global_c_enum name name_enuminfo =
+  let init = {Cil_types.init=None} in
+  mk_global_c_initialized_enum name name_enuminfo init
+
+
 (* ************************************************************************* *)
 (** {b Terms management / computation} *)
 
@@ -913,15 +908,6 @@ let mk_global_states_init root =
        mk_global_var_init var { Cil_types.init = Some init})
     states
 
-let func_to_init name =
-  {Cil_types.init=
-     Some(SingleInit(
-         new_exp ~loc:(CurrentLoc.get()) (Const(func_to_cenum (name)))))}
-
-let funcStatus_to_init st =
-  {Cil_types.init=Some(SingleInit(new_exp ~loc:(CurrentLoc.get())
-                                    (Const(op_status_to_cenum (st)))))}
-
 class visit_decl_loops_init () =
   object(self)
     inherit Visitor.frama_c_inplace
@@ -1138,13 +1124,11 @@ let initGlobals root complete =
   mk_global_c_enum_type
     listOp
     (List.map
-       (fun e -> func_to_op_func e)
-       (getFunctions_from_c() @ getIgnoredFunctions()));
-  mk_global_c_initialized_enum curOp listOp
-    (func_to_init (Kernel_function.get_name root));
+       (fun kf -> func_to_op_func (Kernel_function.get_name kf))
+       (getObservablesFunctions() @ getIgnoredFunctions()));
+  mk_global_c_enum curOp listOp;
   mk_global_c_enum_type  listStatus (callStatus::[termStatus]);
-  mk_global_c_initialized_enum
-    curOpStatus listStatus (funcStatus_to_init Promelaast.Call);
+  mk_global_c_enum curOpStatus listStatus;
 
   mk_global_comment "//* ";
   mk_global_comment "//* States and Trans Variables";
diff --git a/src/plugins/aorai/aorai_visitors.ml b/src/plugins/aorai/aorai_visitors.ml
index f771e84066947d6ff88d6a21fa480a390b6aa254..7ceadc22a6184da07c546578cfe16d4ebe226fb1 100644
--- a/src/plugins/aorai/aorai_visitors.ml
+++ b/src/plugins/aorai/aorai_visitors.ml
@@ -118,100 +118,106 @@ class visit_adding_code_for_synchronisation =
 
     val aux_post_table = Kernel_function.Hashtbl.create 17
 
+    method do_fundec fundec loc =
+      let kf = Extlib.the self#current_kf in
+      let vi = Kernel_function.get_vi kf in
+      let vi_pre = Cil_const.copy_with_new_vid vi in
+      vi_pre.vname <- Data_for_aorai.get_fresh (vi_pre.vname ^ "_pre_func");
+      vi_pre.vdefined <- true;
+      vi_pre.vghost <- true;
+      Cil_datatype.Varinfo.Hashtbl.add func_orig_table vi_pre (Pre_func kf);
+      (* TODO:
+         - what about protos that have no specified args
+           (NB: cannot be identified here because of implem of Kernel_function).
+         - what about varargs?
+      *)
+      let (rettype,args,varargs,_) = Cil.splitFunctionTypeVI vi_pre in
+      Cil.update_var_type vi_pre (TFun(Cil.voidType, args, varargs,[]));
+      vi_pre.vattr <- [];
+
+      (* in particular get rid of __no_return if set in vi*)
+
+      let arg =
+        if Cil.isVoidType rettype
+        then []
+        else ["res",rettype,[]]
+      in
+      let vi_post =
+        Cil.makeGlobalVar ~ghost:true
+          (Data_for_aorai.get_fresh (vi.vname ^ "_post_func"))
+          (TFun(voidType,Some arg,false,[]))
+      in
+      Kernel_function.Hashtbl.add aux_post_table kf vi_post;
+      Cil_datatype.Varinfo.Hashtbl.add func_orig_table vi_post (Post_func kf);
+      let fun_dec_pre = Cil.emptyFunctionFromVI vi_pre in
+      let fun_dec_post = Cil.emptyFunctionFromVI vi_post in
+      (* For a future analysis of function arguments,
+         we have to update the function's formals. Search
+         for LBLsformals. *)
+      Cil.setFunctionTypeMakeFormals
+        fun_dec_pre (TFun(Cil.voidType, args, varargs,[]));
+      Cil.setFunctionTypeMakeFormals
+        fun_dec_post (TFun(voidType,Some arg,false,[]));
+      (* We will now fill the function with the result
+         of the automaton's analysis. *)
+      Globals.Functions.replace_by_definition
+        (Cil.empty_funspec()) fun_dec_pre loc;
+      Globals.Functions.replace_by_definition
+        (Cil.empty_funspec()) fun_dec_post loc;
+      let kf_pre = Globals.Functions.get vi_pre in
+      let kf_post = Globals.Functions.get vi_post in
+      let aux_func_pre, pre_block,pre_locals = mk_pre_fct_block kf_pre kf in
+      let aux_func_post, post_block,post_locals =
+        mk_post_fct_block
+          kf_post kf (Extlib.opt_of_list fun_dec_post.sformals)
+      in
+      fun_dec_pre.slocals <- pre_locals;
+      fun_dec_pre.sbody <- pre_block;
+      fun_dec_pre.svar.vdefined <- true;
+      fun_dec_post.slocals <- post_locals;
+      fun_dec_post.sbody <- post_block;
+      fun_dec_post.svar.vdefined <- true;
+      let aux_funcs =
+        Cil_datatype.Varinfo.Set.union aux_func_pre aux_func_post
+      in
+      let globs =
+        Cil_datatype.Varinfo.Set.fold
+          (fun x acc ->
+             GFunDecl(Cil.empty_funspec(),x,loc) :: acc) aux_funcs
+          [ GFun(fun_dec_pre,loc); GFun(fun_dec_post,loc)]
+      in
+      Cil_datatype.Varinfo.Set.iter (add_aux_bhv kf) aux_funcs;
+      fundec.sbody.bstmts <-
+        Cil.mkStmtOneInstr ~ghost:true
+          (Call(None,Cil.evar ~loc vi_pre,
+                List.map (fun x -> Cil.evar ~loc x)
+                  (Kernel_function.get_formals kf),
+                loc))
+        :: fundec.sbody.bstmts;
+      (* Finally, we update the CFG for the new fundec *)
+      let keepSwitch = Kernel.KeepSwitch.get() in
+      Cfg.prepareCFG ~keepSwitch fun_dec_pre;
+      Cfg.cfgFun fun_dec_pre;
+      Cfg.prepareCFG ~keepSwitch fun_dec_post;
+      Cfg.cfgFun fun_dec_post;
+      globs
+
     method! vglob_aux g =
       match g with
       | GFun (fundec,loc) ->
-        let kf = Option.get self#current_kf in
-        let vi = Kernel_function.get_vi kf in
-        let vi_pre = Cil_const.copy_with_new_vid vi in
-        vi_pre.vname <- Data_for_aorai.get_fresh (vi_pre.vname ^ "_pre_func");
-        vi_pre.vdefined <- true;
-        vi_pre.vghost <- true;
-        Cil_datatype.Varinfo.Hashtbl.add func_orig_table vi_pre (Pre_func kf);
-        (* TODO:
-           - what about protos that have no specified args
-             (NB: cannot be identified here because of implem of Kernel_function).
-           - what about varargs?
-        *)
-        let (rettype,args,varargs,_) = Cil.splitFunctionTypeVI vi_pre in
-        Cil.update_var_type vi_pre (TFun(Cil.voidType, args, varargs,[]));
-        vi_pre.vattr <- [];
-
-        (* in particular get rid of __no_return if set in vi*)
-
-        let arg =
-          if Cil.isVoidType rettype
-          then []
-          else ["res",rettype,[]]
-        in
-        let vi_post =
-          Cil.makeGlobalVar ~ghost:true
-            (Data_for_aorai.get_fresh (vi.vname ^ "_post_func"))
-            (TFun(voidType,Some arg,false,[]))
-        in
-        Kernel_function.Hashtbl.add aux_post_table kf vi_post;
-        Cil_datatype.Varinfo.Hashtbl.add func_orig_table vi_post (Post_func kf);
-        let fun_dec_pre = Cil.emptyFunctionFromVI vi_pre in
-        let fun_dec_post = Cil.emptyFunctionFromVI vi_post in
-        (* For a future analysis of function arguments,
-           we have to update the function's formals. Search
-           for LBLsformals. *)
-        Cil.setFunctionTypeMakeFormals
-          fun_dec_pre (TFun(Cil.voidType, args, varargs,[]));
-        Cil.setFunctionTypeMakeFormals
-          fun_dec_post (TFun(voidType,Some arg,false,[]));
-        (* We will now fill the function with the result
-           of the automaton's analysis. *)
-        Globals.Functions.replace_by_definition
-          (Cil.empty_funspec()) fun_dec_pre loc;
-        Globals.Functions.replace_by_definition
-          (Cil.empty_funspec()) fun_dec_post loc;
-        let kf_pre = Globals.Functions.get vi_pre in
-        let kf_post = Globals.Functions.get vi_post in
-        let aux_func_pre, pre_block,pre_locals = mk_pre_fct_block kf_pre kf in
-        let aux_func_post, post_block,post_locals =
-          mk_post_fct_block
-            kf_post kf (Extlib.opt_of_list fun_dec_post.sformals)
-        in
-        fun_dec_pre.slocals <- pre_locals;
-        fun_dec_pre.sbody <- pre_block;
-        fun_dec_pre.svar.vdefined <- true;
-        fun_dec_post.slocals <- post_locals;
-        fun_dec_post.sbody <- post_block;
-        fun_dec_post.svar.vdefined <- true;
-        let aux_funcs =
-          Cil_datatype.Varinfo.Set.union aux_func_pre aux_func_post
-        in
-        let globs =
-          Cil_datatype.Varinfo.Set.fold
-            (fun x acc ->
-               GFunDecl(Cil.empty_funspec(),x,loc) :: acc) aux_funcs
-            [ GFun(fun_dec_pre,loc); GFun(fun_dec_post,loc)]
-        in
-        Cil_datatype.Varinfo.Set.iter (add_aux_bhv kf) aux_funcs;
-        fundec.sbody.bstmts <-
-          Cil.mkStmtOneInstr ~ghost:true
-            (Call(None,Cil.evar ~loc vi_pre,
-                  List.map (fun x -> Cil.evar ~loc x)
-                    (Kernel_function.get_formals kf),
-                  loc))
-          :: fundec.sbody.bstmts;
-        (* Finally, we update the CFG for the new fundec *)
-        let keepSwitch = Kernel.KeepSwitch.get() in
-        Cfg.prepareCFG ~keepSwitch fun_dec_pre;
-        Cfg.cfgFun fun_dec_pre;
-        Cfg.prepareCFG ~keepSwitch fun_dec_post;
-        Cfg.cfgFun fun_dec_post;
-        ChangeDoChildrenPost([g], fun x -> globs @ x)
+        let kf = Globals.Functions.get fundec.svar in
+        if Data_for_aorai.isObservableFunction kf then
+          let globs = self#do_fundec fundec loc in
+          ChangeDoChildrenPost([g], fun x -> globs @ x)
+        else
+          DoChildren
       | _ -> DoChildren
 
     method! vstmt_aux stmt =
       match stmt.skind with
       | Return (res,loc)  ->
         let kf = Option.get self#current_kf in
-        let vi = Kernel_function.get_vi kf in
-        let current_function = vi.vname in
-        if not (Data_for_aorai.isIgnoredFunction current_function) then begin
+        if Data_for_aorai.isObservableFunction kf then begin
           let args = match res with
             | None -> []
             | Some exp -> [Cil.copy_exp exp]
diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index ec4242b8b794db748713326beae4166d7c5ea4fa..157f44778f221d425e88170fdc2beacb164518ca 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -211,11 +211,9 @@ let automata = ref None
 (* Each transition with a parametrized cross condition (call param access or return value access) has its parametrized part stored in this array. *)
 let cond_of_parametrizedTransitions = ref (Array.make (1) [[]])
 
-(* List of variables name observed in the C file *)
-let variables_from_c = ref []
-(* List of functions name observed in the C file *)
-let functions_from_c = ref []
-(* List of functions call observed in the C file without declaration *)
+(* List of functions defined in the C file *)
+let defined_functions = ref []
+(* List of functions without declaration *)
 let ignored_functions = ref []
 
 (** Return the buchi automata as stored after parsing *)
@@ -1545,6 +1543,27 @@ let checkMetavariableCompatibility auto =
       "The use of metavariables is incompatible with non-deterministic \
        automata, such as automa using extended transitions."
 
+let check_observables auto =
+ match auto.observables with
+ | None -> () (* No observable list set, everything is observable *)
+ | Some set ->
+   let is_relevant name =
+     try
+       ignore (Globals.Functions.find_by_name name)
+     with Not_found ->
+       Aorai_option.fatal "Observable %s doesn't match any function" name
+   in
+   let rec check = function
+     | TAnd (c1,c2) | TOr (c1,c2) -> check c1; check c2
+     | TNot (c) -> check c
+     | TRel _ | TTrue | TFalse -> ()
+     | TCall (kf,_) | TReturn kf ->
+       let name = Kernel_function.get_name kf in
+       if not (Datatype.String.Set.mem name set) then
+         Aorai_option.fatal "Function %s is not observable" name
+   in
+   Datatype.String.Set.iter is_relevant set;
+   List.iter (fun tr -> check tr.cross) auto.trans
 
 (** Stores the buchi automaton and its variables and
     functions as it is returned by the parsing *)
@@ -1553,6 +1572,7 @@ let setAutomata auto =
   let auto = type_cond_auto auto in
   automata:=Some auto;
   check_states "typed automata";
+  check_observables auto;
   if Aorai_option.debug_atleast 1 then
     Promelaoutput.Typed.output_dot_automata auto "aorai_debug_reduced.dot";
   if (Array.length !cond_of_parametrizedTransitions) <
@@ -1577,41 +1597,39 @@ let setCData () =
   let (f_decl,f_def) =
     Globals.Functions.fold
       (fun f (lf_decl,lf_def) ->
-         let name = (Kernel_function.get_name f) in
          match f.fundec with
-           | Definition _ -> (lf_decl,name::lf_def)
-           | Declaration _ -> (name::lf_decl,lf_def))
+           | Definition _  -> (lf_decl, f :: lf_def)
+           | Declaration _ -> (f :: lf_decl, lf_def))
       ([],[])
   in
-  functions_from_c:=f_def;
-  ignored_functions:=f_decl;
-  variables_from_c:=
-    Globals.Vars.fold
-    (fun v _ lv ->
-      Format.asprintf "%a" Cil_datatype.Varinfo.pretty v :: lv)
-    []
+  defined_functions := f_def;
+  ignored_functions := f_decl
 
-(** Return the list of all function name observed in the C file, except ignored functions. *)
-let getFunctions_from_c () =
-  (!functions_from_c)
+let addIgnoredFunction kf =
+  ignored_functions := kf :: !ignored_functions
 
-(** Return the list of all variables name observed in the C file. *)
-let getVariables_from_c () =
-  (!variables_from_c)
+(** Return true if and only if the given string fname denotes an ignored function. *)
+let isIgnoredFunction kf =
+  List.exists (Kernel_function.equal kf) !ignored_functions
 
-(** Return the list of names of all ignored functions. A function is ignored if it is used in C file and if its declaration is unavailable. *)
-let getIgnoredFunctions () =
-  (!ignored_functions)
+let isDeclaredObservable kf =
+  let auto = getAutomata () in
+  let fname = Kernel_function.get_name kf in
+  match auto.observables with
+  | None -> true
+  | Some set ->
+    Datatype.String.Set.mem fname set
 
-(** Return the list of names of all ignored functions. A function is ignored if it is used in C file and if its declaration is unavailable. *)
-let addIgnoredFunction fname =
-  ignored_functions:=fname::(!ignored_functions)
+let isObservableFunction kf =
+  not (isIgnoredFunction kf) && isDeclaredObservable kf
 
-(** Return true if and only if the given string fname denotes an ignored function. *)
-let isIgnoredFunction fname =
-  List.exists
-    (fun s -> (String.compare fname s)=0)
-    (!ignored_functions)
+(** Return the list of all function name observed in the C file, except ignored functions. *)
+let getObservablesFunctions () =
+  List.filter isDeclaredObservable !defined_functions
+
+(** Return the list of names of observable but ignored functions. A function is ignored if it is used in C file and if its declaration is unavailable. *)
+let getIgnoredFunctions () =
+  List.filter isDeclaredObservable !ignored_functions
 
 let is_reject_state state =
   match Reject_state.get_option () with
diff --git a/src/plugins/aorai/data_for_aorai.mli b/src/plugins/aorai/data_for_aorai.mli
index 8c7ed586075255f9c356a763d28debfe3859f17b..786ca7217fbe4d5d1e6e5c7b912deea6a570da71 100644
--- a/src/plugins/aorai/data_for_aorai.mli
+++ b/src/plugins/aorai/data_for_aorai.mli
@@ -218,20 +218,20 @@ val getNumberOfTransitions : unit -> int
 (** return the number of states of the automata *)
 val getNumberOfStates : unit -> int
 
-(** Return the list of all function name observed in the C file. *)
-val getFunctions_from_c : unit -> string list
+(** Return the list of all function name observed in the C file, except ignored functions. *)
+val getObservablesFunctions : unit -> Cil_types.kernel_function list
 
-(** Return the list of all variables name observed in the C file. *)
-val getVariables_from_c : unit -> string list
+(** Return the list of names of observable but ignored functions. A function is ignored if it is used in C file and if its declaration is unavailable. *)
+val getIgnoredFunctions : unit -> Cil_types.kernel_function list
 
 (** Return the list of names of all ignored functions. A function is ignored if it is used in C file and if its declaration is unavailable. *)
-val getIgnoredFunctions : unit -> string list
-
-(** Return the list of names of all ignored functions. A function is ignored if it is used in C file and if its declaration is unavailable. *)
-val addIgnoredFunction : string -> unit
+val addIgnoredFunction : Cil_types.kernel_function -> unit
 
 (** Return true if and only if the given string fname denotes an ignored function. *)
-val isIgnoredFunction : string -> bool
+val isIgnoredFunction : Cil_types.kernel_function -> bool
+
+(** Return true if and onfly if the given function can be observed *)
+val isObservableFunction : Cil_types.kernel_function -> bool
 
 (** returns the state of given index.
     @since Nitrogen-20111001
diff --git a/src/plugins/aorai/promelaast.mli b/src/plugins/aorai/promelaast.mli
index fe0bdcfe677bb92ffb947f99580bb7814134e60f..833e13eddde29c8f22eff7970b4e0ba17806d62e 100644
--- a/src/plugins/aorai/promelaast.mli
+++ b/src/plugins/aorai/promelaast.mli
@@ -142,6 +142,7 @@ type ('c,'a) automaton = {
   states: state list;
   trans: (('c,'a) trans) list;
   metavariables: Cil_types.varinfo Datatype.String.Map.t;
+  observables: Datatype.String.Set.t option;
 }
 
 type parsed_automaton = (guard, action) automaton
diff --git a/src/plugins/aorai/promelaparser.mly b/src/plugins/aorai/promelaparser.mly
index 4bcac643722e16f76ec9c72423f3e4f44d030119..1badbbe38a966ef35ed9cea04e2344cd7da29be0 100644
--- a/src/plugins/aorai/promelaparser.mly
+++ b/src/plugins/aorai/promelaparser.mly
@@ -77,7 +77,10 @@ promela
                 st::l
               ) observed_states []
             in
-            { states; trans = $3; metavariables = Datatype.String.Map.empty }
+            { states; trans = $3;
+              metavariables = Datatype.String.Map.empty;
+              observables = None;
+            }
         }
         | PROMELA_NEVER PROMELA_LBRACE states PROMELA_SEMICOLON 
             PROMELA_RBRACE EOF {
@@ -91,7 +94,11 @@ promela
                   st::l
                 ) observed_states []
               in
-              { states; trans = $3; metavariables = Datatype.String.Map.empty } }
+              { states; trans = $3;
+                metavariables = Datatype.String.Map.empty;
+                observables = None;
+              }
+          }
   ;
 
 states   
diff --git a/src/plugins/aorai/promelaparser_withexps.mly b/src/plugins/aorai/promelaparser_withexps.mly
index bf852a65f3747b7a4c976151a3b593b90fe4da18..4f8abab8a0e026c3d93198c570da28cf22b9178c 100644
--- a/src/plugins/aorai/promelaparser_withexps.mly
+++ b/src/plugins/aorai/promelaparser_withexps.mly
@@ -88,7 +88,10 @@ promela
                 st::l
               ) observed_states []
             in
-            { states; trans = $3; metavariables = Datatype.String.Map.empty }
+            { states; trans = $3;
+              metavariables = Datatype.String.Map.empty;
+              observables = None;
+            }
         }
         | PROMELA_NEVER PROMELA_LBRACE states 
             PROMELA_SEMICOLON PROMELA_RBRACE EOF {
@@ -102,7 +105,11 @@ promela
                 st::l
               ) observed_states []
             in
-            { states; trans = $3; metavariables = Datatype.String.Map.empty } }
+            { states; trans = $3;
+              metavariables = Datatype.String.Map.empty;
+              observables = None;
+            }
+        }
   ;
 
 states   
diff --git a/src/plugins/aorai/tests/ltl/oracle/goto.res.oracle b/src/plugins/aorai/tests/ltl/oracle/goto.res.oracle
index c1554953000b5e332460b05a1a5bb6c832c1829c..265c294b60c1352009e8cf0edac82d1896ccfa55 100644
--- a/src/plugins/aorai/tests/ltl/oracle/goto.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/goto.res.oracle
@@ -18,8 +18,8 @@ int status = 0;
 int rr = 1;
 /*@ global invariant inv: 0 ≤ rr ≤ 5000;
  */
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int accept_S2 = 0; */
 /*@ ghost int accept_S3 = 0; */
 /*@ ghost int accept_S4 = 0; */
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_boucle.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_boucle.res.oracle
index af9bc71a2b3a1adf94c0022438693926ffc17f6f..844192381021eed94fa7c2989f7b24ba1f12aa01 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_boucle.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_boucle.res.oracle
@@ -16,8 +16,8 @@ enum aorai_OpStatusList {
 };
 extern int call_to_an_undefined_function(void);
 
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int T0_S2 = 0; */
 /*@ ghost int T0_init = 1; */
 /*@ ghost int accept_S1 = 0; */
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_boucle1.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_boucle1.res.oracle
index 9da27b6622ebd3fbb5ae7fefb8a0e694d48175d1..d48aaf2d91ec30b8856d568c26a89d02de957748 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_boucle1.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_boucle1.res.oracle
@@ -17,8 +17,8 @@ int cpt = 3;
 int status = 0;
 /*@ global invariant inv_status: 0 ≤ status ≤ 1;
  */
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int accept_S1 = 0; */
 /*@ ghost int accept_S2 = 0; */
 /*@ ghost int accept_S3 = 0; */
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_boucle2.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_boucle2.res.oracle
index 3b6f510bb856cc315fcedd97a9d0796d7bbf4d9a..8491e8c23edf107114bbcc7deeb208bca688e321 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_boucle2.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_boucle2.res.oracle
@@ -15,8 +15,8 @@ int status = 0;
 int rr = 1;
 /*@ global invariant inv: 0 ≤ rr ≤ 50;
  */
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int T0_S2 = 0; */
 /*@ ghost int T0_init = 1; */
 /*@ ghost int accept_S3 = 0; */
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_boucle3.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_boucle3.res.oracle
index 0e2861364d6f1efef4a6191a0cd4ac2a817c7b23..4521080b3e1763859975e8f0d81762316305d61c 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_boucle3.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_boucle3.res.oracle
@@ -15,8 +15,8 @@ int status = 0;
 int rr = 1;
 /*@ global invariant inv: 0 ≤ rr ≤ 50;
  */
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int T0_S4 = 0; */
 /*@ ghost int T0_init = 1; */
 /*@ ghost int T1_S2 = 0; */
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_factorial.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_factorial.res.oracle
index 76309462d15d0678365eb0f899d7dc1730f6ad87..c1aac176071c4e4f44da6263665a845b67f6eb08 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_factorial.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_factorial.res.oracle
@@ -11,8 +11,8 @@ enum aorai_OpStatusList {
     aorai_Terminated = 1,
     aorai_Called = 0
 };
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int accept_S1 = 0; */
 /*@ ghost int accept_S2 = 0; */
 /*@ ghost int accept_init = 1; */
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_recursion1.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_recursion1.res.oracle
index c3757b98233f81226e3bf18a2a4fdf0ba0e6aba9..eaaac90fdb2269338410ce6fac7a19c5f87a50cf 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_recursion1.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_recursion1.res.oracle
@@ -45,8 +45,8 @@ axiomatic string_len {
 predicate valid_string{L}(char *s) =
   \valid(s) ∧ \valid(s + (0 .. string_len(s)));
  */
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int T0_S2 = 0; */
 /*@ ghost int T0_init = 1; */
 /*@ ghost int accept_S1 = 0; */
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_recursion2.0.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_recursion2.0.res.oracle
index fd43837e998528a1c7cfa61c0424d06e0c3d4508..eb681fba1c9bb4c765e3b1b3b0c173541738b297 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_recursion2.0.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_recursion2.0.res.oracle
@@ -60,8 +60,8 @@ axiomatic sum_tab {
   }
  */
 int global_argc = 0;
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int S1 = 0; */
 /*@ ghost int T0_init = 1; */
 /*@ ghost int T1 = 0; */
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_recursion2.1.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_recursion2.1.res.oracle
index a40a3eae30459dfa081154ccd2b0eed95761f1b8..e92778bcb0cee2799033715b02f935ecf75e8d43 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_recursion2.1.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_recursion2.1.res.oracle
@@ -60,8 +60,8 @@ axiomatic sum_tab {
   }
  */
 int global_argc = 0;
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int S1 = 0; */
 /*@ ghost int T0_init = 1; */
 /*@ ghost int T1 = 0; */
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_switch2.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_switch2.res.oracle
index 2ceecc16fc151c2ddca917d597dc7114a5a58dd8..41a59d023f0609c5b9faf6659d71d5a8afe5b8de 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_switch2.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_switch2.res.oracle
@@ -20,8 +20,8 @@ int status = 0;
 int rr = 1;
 /*@ global invariant inv: 0 ≤ rr ≤ 50;
  */
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int accept_S2 = 0; */
 /*@ ghost int accept_S3 = 0; */
 /*@ ghost int accept_S4 = 0; */
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_switch3.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_switch3.res.oracle
index d81509eb53661bace2a79e5e2babdface3e95275..4ed3b4a39a1a4b99f1c6cbe87ff005554824fd37 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_switch3.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_switch3.res.oracle
@@ -11,8 +11,8 @@ enum aorai_OpStatusList {
     aorai_Terminated = 1,
     aorai_Called = 0
 };
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int T0_S2 = 0; */
 /*@ ghost int T0_init = 1; */
 /*@ ghost int accept_S1 = 0; */
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_switch3_et_recursion.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_switch3_et_recursion.res.oracle
index e5154fb858165466a56370e5d91986cf92384539..62566d6ad713caa507dc98dff28f8670a270d0bc 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_switch3_et_recursion.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_switch3_et_recursion.res.oracle
@@ -13,8 +13,8 @@ enum aorai_OpStatusList {
     aorai_Terminated = 1,
     aorai_Called = 0
 };
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int T0_S2 = 0; */
 /*@ ghost int T0_init = 1; */
 /*@ ghost int accept_S1 = 0; */
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_switch3_if.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_switch3_if.res.oracle
index 5cc019fcad43e0cfacafa6eb123b8055daf1dda4..88b0352589bb165941afa451c1e9a37bfc82e997 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_switch3_if.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_switch3_if.res.oracle
@@ -11,8 +11,8 @@ enum aorai_OpStatusList {
     aorai_Terminated = 1,
     aorai_Called = 0
 };
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int T0_S2 = 0; */
 /*@ ghost int T0_init = 1; */
 /*@ ghost int accept_S1 = 0; */
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_switch3_return.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_switch3_return.res.oracle
index 0fb781bb7040975d8e51beef6328114ceb34a501..9e0438a0e71a1f5807dfbede85a61cfd25b58cf9 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_switch3_return.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_switch3_return.res.oracle
@@ -11,8 +11,8 @@ enum aorai_OpStatusList {
     aorai_Terminated = 1,
     aorai_Called = 0
 };
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int T0_S2 = 0; */
 /*@ ghost int T0_init = 1; */
 /*@ ghost int accept_S1 = 0; */
diff --git a/src/plugins/aorai/tests/ya/oracle/assigns.0.res.oracle b/src/plugins/aorai/tests/ya/oracle/assigns.0.res.oracle
index 09b37de9a73706afe84ec0fa380d5be28c09a3a8..f4acc0402458f1f853e851fdc62267159d610c1c 100644
--- a/src/plugins/aorai/tests/ya/oracle/assigns.0.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/assigns.0.res.oracle
@@ -11,8 +11,8 @@ enum aorai_OpStatusList {
     aorai_Called = 0
 };
 int X;
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int S1 = 1; */
 /*@ ghost int S2 = 0; */
 /*@ ghost int S_in_f = 0; */
diff --git a/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle b/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle
index fd7526444df55abd2c128af76809b32c0a411955..28be1b6491e4d556fdcbc99882eb5dae9fb753cc 100644
--- a/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle
@@ -29,8 +29,8 @@ enum aorai_OpStatusList {
 /*@ check lemma S1_deterministic_trans{L}: \true;
  */
 int X;
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int aorai_CurStates = S1; */
 /*@ ghost
   /@ requires aorai_CurStates ≡ Sf;
diff --git a/src/plugins/aorai/tests/ya/oracle/bts1289.0.res.oracle b/src/plugins/aorai/tests/ya/oracle/bts1289.0.res.oracle
index 74d55944211b288cd559e0c0f19e44b01dbcbbc6..ded70303a39942fd04bed926f5cfb44b400fb576 100644
--- a/src/plugins/aorai/tests/ya/oracle/bts1289.0.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/bts1289.0.res.oracle
@@ -11,8 +11,8 @@ enum aorai_OpStatusList {
     aorai_Terminated = 1,
     aorai_Called = 0
 };
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int S = 0; */
 /*@ ghost
   /@ requires \false;
diff --git a/src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle b/src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle
index adebb6ca55ae7558e8d58bd9d45d024806c68784..c7ab7fc71c40604749775aee8ffd3063ab29279e 100644
--- a/src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle
@@ -10,8 +10,8 @@ enum aorai_OpStatusList {
     aorai_Terminated = 1,
     aorai_Called = 0
 };
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int S = 0; */
 /*@ ghost int T = 0; */
 /*@ ghost int aorai_intermediate_state = 0; */
diff --git a/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle b/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle
index 7141a6e19585342e2f1f9571efaa71e68c2ba704..9aac8e4561e2046e3363b3e1986e89443b6ff944 100644
--- a/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle
@@ -16,8 +16,8 @@ enum aorai_OpStatusList {
 };
 int f(void);
 
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@
 check lemma I_deterministic_trans{L}:
   (∀ int __retres_f;
diff --git a/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle b/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
index 6b9c9095bc9917c070ddd1dbf2ec9d73de8d75c4..eac5b5331dea0f341ab284906042b6468f412140 100644
--- a/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
@@ -35,8 +35,8 @@ enum aorai_OpStatusList {
  */
 int X;
 int Y;
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@
 check lemma S3_deterministic_trans{L}:
   ∀ int x;
diff --git a/src/plugins/aorai/tests/ya/oracle/formals.res.oracle b/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
index 52323f131b74b603bc960c19408f6ea80930453f..1b5982df2b99caeb671563defdd0c978475437ac 100644
--- a/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
@@ -28,8 +28,8 @@ enum aorai_OpStatusList {
  */
 /*@ check lemma OK_deterministic_trans{L}: \true;
  */
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@
 check lemma main_0_deterministic_trans{L}:
   ∀ int x;
diff --git a/src/plugins/aorai/tests/ya/oracle/generate_assigns_bts1290.res.oracle b/src/plugins/aorai/tests/ya/oracle/generate_assigns_bts1290.res.oracle
index 6d8dc5b0067777a8f5ab853f8611e02a22d4925e..a409f76aa7ac5194420e1825744755a472e97f68 100644
--- a/src/plugins/aorai/tests/ya/oracle/generate_assigns_bts1290.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/generate_assigns_bts1290.res.oracle
@@ -9,8 +9,8 @@ enum aorai_OpStatusList {
     aorai_Terminated = 1,
     aorai_Called = 0
 };
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int S = 1; */
 /*@ ghost
   /@ requires 1 ≡ S;
diff --git a/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle b/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle
index ea603b7e865bbc3a1982b4512166a5ed8cf48eb7..b8271b7f3704cc26e61134cc57f31bb16d75406e 100644
--- a/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle
@@ -10,8 +10,8 @@ enum aorai_OpStatusList {
     aorai_Terminated = 1,
     aorai_Called = 0
 };
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int S0 = 1; */
 /*@ ghost int Sf = 0; */
 /*@ ghost int aorai_intermediate_state = 0; */
diff --git a/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle b/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle
index ccfb249eba5eb4f3b759bba09f44a869117caa21..bcd7dddbbf40385d8d4339e4dc6f5f884bf631d4 100644
--- a/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle
@@ -19,8 +19,8 @@ enum aorai_OpStatusList {
  */
 int f(void);
 
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int aorai_CurStates = s0; */
 /*@ ghost
   /@ requires \false;
diff --git a/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle b/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
index ccc98a41d83d4339cb70a182bed8396973f9d901..926ceb3efd81f583b13bdb57410e2dc8a350816c 100644
--- a/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
@@ -11,8 +11,8 @@ enum aorai_OpStatusList {
     aorai_Terminated = 1,
     aorai_Called = 0
 };
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int S0 = 1; */
 /*@ ghost int Sf = 0; */
 /*@ ghost int aorai_intermediate_state = 0; */
diff --git a/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle b/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
index 39843d1a28ef389cbcc34ab6095bff3f80d0ec8a..f9cbea2f85d0a3e5d8f936783cce082dded8059d 100644
--- a/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
@@ -39,8 +39,8 @@ enum aorai_OpStatusList {
  */
 /*@ check lemma a_deterministic_trans{L}: \true;
  */
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@
 check lemma b_deterministic_trans{L}:
   ¬(\at(aorai_CurOperation,L) ≡ op_g ∧
diff --git a/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle b/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
index 86ceb3e991278c964faf62706c167f6710087817..b0789f55dee4aedb27898df52aca2a53fe61924a 100644
--- a/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
@@ -21,8 +21,8 @@ enum aorai_OpStatusList {
 };
 /*@ check lemma aorai_reject_deterministic_trans{L}: \true;
  */
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@
 check lemma aorai_intermediate_state_deterministic_trans{L}:
   ¬(\at(aorai_CurOperation,L) ≡ op_main ∧
diff --git a/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle b/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle
index 1d964840b06fc2869b27dc1f9ff1115c052861fc..e2b8af2f5f8c2edd8827cdbe6b9e0d81c81499ef 100644
--- a/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle
@@ -9,8 +9,8 @@ enum aorai_OpStatusList {
     aorai_Terminated = 1,
     aorai_Called = 0
 };
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_f; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int S0 = 1; */
 /*@ ghost int Sf = 0; */
 /*@ ghost
diff --git a/src/plugins/aorai/tests/ya/oracle/other.res.oracle b/src/plugins/aorai/tests/ya/oracle/other.res.oracle
index 8f230ecadb224c890456d0ef3ef0415fa9db4e9a..24195e41f5e3f2034d9deeb0369017289bf4f9bf 100644
--- a/src/plugins/aorai/tests/ya/oracle/other.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/other.res.oracle
@@ -12,8 +12,8 @@ enum aorai_OpStatusList {
     aorai_Called = 0
 };
 int x = 0;
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int init = 1; */
 /*@ ghost int last = 0; */
 /*@ ghost int step1 = 0; */
diff --git a/src/plugins/aorai/tests/ya/oracle/seq.res.oracle b/src/plugins/aorai/tests/ya/oracle/seq.res.oracle
index 506dca121a3f23b957ced47740eee807cff752ec..ad8e58e2c0a5251a4299d62bf2bfc419738d2f6a 100644
--- a/src/plugins/aorai/tests/ya/oracle/seq.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/seq.res.oracle
@@ -11,8 +11,8 @@ enum aorai_OpStatusList {
     aorai_Terminated = 1,
     aorai_Called = 0
 };
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int S0 = 1; */
 /*@ ghost int Sf = 0; */
 /*@ ghost int aorai_intermediate_state = 0; */
diff --git a/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle b/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
index 91097fdf88b9aa56ad5e7d32f14521e41cb9cbd8..74c4b90d5d2ac7f17973e6170696db87575565e8 100644
--- a/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
@@ -11,8 +11,8 @@ enum aorai_OpStatusList {
     aorai_Terminated = 1,
     aorai_Called = 0
 };
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int S0 = 1; */
 /*@ ghost int Sf = 0; */
 /*@ ghost int aorai_intermediate_state = 0; */
diff --git a/src/plugins/aorai/tests/ya/oracle/single_call.res.oracle b/src/plugins/aorai/tests/ya/oracle/single_call.res.oracle
index ee4213fd46c5d23bbeacb123d8f1409c65f5ef1a..8140ad900ee448b23e0d0ab056c90be13f42ebd8 100644
--- a/src/plugins/aorai/tests/ya/oracle/single_call.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/single_call.res.oracle
@@ -9,8 +9,8 @@ enum aorai_OpStatusList {
     aorai_Terminated = 1,
     aorai_Called = 0
 };
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int S0 = 1; */
 /*@ ghost int Sf = 0; */
 /*@ ghost int aorai_intermediate_state = 0; */
diff --git a/src/plugins/aorai/tests/ya/oracle/singleassignment-right.res.oracle b/src/plugins/aorai/tests/ya/oracle/singleassignment-right.res.oracle
index 47bd37cf3ee9430554f51b2119e5f95c25f49990..964d18945b278a6d0d8a87aca748535bb645db42 100644
--- a/src/plugins/aorai/tests/ya/oracle/singleassignment-right.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/singleassignment-right.res.oracle
@@ -21,8 +21,8 @@ enum aorai_OpStatusList {
  */
 /*@ check lemma a_deterministic_trans{L}: \true;
  */
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int aorai_CurStates = a; */
 /*@ ghost int aorai_x = 0; */
 /*@ ghost int aorai_y = 0; */
diff --git a/src/plugins/aorai/tests/ya/oracle/stack.res.oracle b/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
index 6ca094fa00c5447876ad01b5e9f2b6297b9ecbcd..9ff7ca0aecdd7464bd5a26e5dabe134ca5e47e22 100644
--- a/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
@@ -27,8 +27,8 @@ enum aorai_OpStatusList {
 /*@ check lemma accept_deterministic_trans{L}: \true;
  */
 int g = 0;
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@
 check lemma empty_stack_deterministic_trans{L}:
   ¬(\at(aorai_CurOperation,L) ≡ op_push ∧
diff --git a/src/plugins/aorai/tests/ya/oracle/test_acces_params.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_acces_params.res.oracle
index 89553036d1a684d71bccedc4dc525fe7dbcb2ed1..20787049401870e0d034354f17271fc1c4a30eee 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_acces_params.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_acces_params.res.oracle
@@ -15,8 +15,8 @@ int status = 0;
 int rr = 1;
 /*@ global invariant inv: 0 ≤ rr ≤ 5000;
  */
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int S1 = 0; */
 /*@ ghost int S2 = 0; */
 /*@ ghost int S3 = 0; */
diff --git a/src/plugins/aorai/tests/ya/oracle/test_acces_params2.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_acces_params2.res.oracle
index 16997723976399ec7e581375b99d0be6dc37e33e..c6d27622ae3da9ddb41c15b669517df025313969 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_acces_params2.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_acces_params2.res.oracle
@@ -15,8 +15,8 @@ enum aorai_OpStatusList {
 int rr = 1;
 /*@ global invariant inv: 0 ≤ rr ≤ 5000;
  */
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int S1 = 1; */
 /*@ ghost int S2 = 0; */
 /*@ ghost int S3 = 0; */
diff --git a/src/plugins/aorai/tests/ya/oracle/test_boucle_rechercheTableau.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_boucle_rechercheTableau.res.oracle
index 6bd1a0b39b8010458503b8e83ae36ac33f416ecf..6bb7bed4d3159b60efac15e5c8cdd6eadf1c409c 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_boucle_rechercheTableau.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_boucle_rechercheTableau.res.oracle
@@ -15,8 +15,8 @@ enum aorai_OpStatusList {
     aorai_Terminated = 1,
     aorai_Called = 0
 };
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int End = 0; */
 /*@ ghost int Idle = 1; */
 /*@ ghost int WillDoFoo = 0; */
diff --git a/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle
index 009f14f70dd4771f190e1b6b609515a3a8316b8a..ef459e69225d1cf2833865df30d46ea4dc7b7aed 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle
@@ -11,8 +11,8 @@ enum aorai_OpStatusList {
     aorai_Terminated = 1,
     aorai_Called = 0
 };
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int S1 = 0; */
 /*@ ghost int S2 = 0; */
 /*@ ghost int main_0 = 1; */
diff --git a/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle
index cdfe4aba74bff1e589436adad382f28f9967766a..9ff8daac4d006c4b2c7654824e4778e6d8869700 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle
@@ -12,8 +12,8 @@ enum aorai_OpStatusList {
     aorai_Called = 0
 };
 #pragma JessieIntegerModel(math)
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int End = 0; */
 /*@ ghost int Idle = 1; */
 /*@ ghost int WillDoFoo = 0; */
diff --git a/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle
index bc9334eec11d7af2e8fcb00eb21f5fb24d1a832f..6510597aa4dbf5cca3ffa2ace04e3c9d207deedc 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle
@@ -16,8 +16,8 @@ enum aorai_OpStatusList {
     aorai_Terminated = 1,
     aorai_Called = 0
 };
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int End = 0; */
 /*@ ghost int Idle = 1; */
 /*@ ghost int IgnoreFoo = 0; */
diff --git a/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle
index 0e102ceda9633ce37d9262207c569e610ce0a69b..b73119bb7007bd98d2ff9ae0121f38547cd3bfdf 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle
@@ -16,8 +16,8 @@ enum aorai_OpStatusList {
 };
 struct People nobody;
 int myAge = 0;
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int S1 = 0; */
 /*@ ghost int main_0 = 1; */
 /*@ ghost
diff --git a/src/plugins/aorai/yaparser.mly b/src/plugins/aorai/yaparser.mly
index 3a88ed02f8f6e646fb116fe4846ee366ea58e190..699489687f31b95eaecdead54796d716fa0709a5 100644
--- a/src/plugins/aorai/yaparser.mly
+++ b/src/plugins/aorai/yaparser.mly
@@ -32,7 +32,11 @@ open Logic_ptree
 open Promelaast
 open Bool3
 
-type options = Deterministic | Init of string list | Accept of string list
+type options =
+  | Deterministic
+  | Init of string list
+  | Accept of string list
+  | Observables of string list
 
 let to_seq c =
   [{ condition = Some c;
@@ -104,13 +108,22 @@ let check_state st =
    Aorai_option.abort
     "Error: the state '%s' is used but never defined." st.name
 
-let interpret_option = function
+let interpret_option auto = function
   | Init states ->
-    List.iter set_init_state states
+    List.iter set_init_state states; auto
   | Accept states ->
-    List.iter set_accept_state states
+    List.iter set_accept_state states; auto
   | Deterministic ->
-    Aorai_option.Deterministic.set true
+    Aorai_option.Deterministic.set true; auto
+  | Observables names ->
+    let module Set = Datatype.String.Set in
+    let new_set = Set.of_list names in
+    let observables =
+      match auto.observables with
+      | None -> Some new_set
+      | Some set -> Some (Set.union set new_set)
+    in
+    { auto with observables }
 
 let build_automaton options metavariables trans =
   let htable_to_list table = Hashtbl.fold (fun _ st l -> st :: l) table [] in
@@ -119,15 +132,15 @@ let build_automaton options metavariables trans =
   and metavariables =
     List.fold_left add_metavariable Datatype.String.Map.empty metavariables
   in
-  List.iter interpret_option options;
+  let auto = { states; trans; metavariables; observables = None } in
+  let auto = List.fold_left interpret_option auto options in
   List.iter check_state states;
   if not (List.exists (fun st -> st.init=True) states) then
     Aorai_option.abort "Automaton does not declare an initial state";
   if undefined_states <> [] then
     Aorai_option.abort "Error: the state(s) %a are used but never defined."
       (Pretty_utils.pp_list ~sep:"," Format.pp_print_string) undefined_states;
-  { states; trans; metavariables }
-
+  auto
 
 type pre_cond = Behavior of string | Pre of Promelaast.condition
 
@@ -169,6 +182,7 @@ option
     | "init" -> Init $3
     | "accept" -> Accept $3
     | "deterministic" -> Deterministic
+    | "observables" -> Observables $3
     | _ ->  Aorai_option.abort "unknown option: '%s'" $2
   }