module Aorai_register: sig
.. end
val promela_file : string Pervasives.ref
val ya_file : Aorai_option.Ya.t Pervasives.ref
val c_file : string Pervasives.ref
val output_c_file : Aorai_option.Output_C_File.t Pervasives.ref
val ltl_tmp_file : string Pervasives.ref
val ltl_file : Aorai_option.Ltl_File.t Pervasives.ref
val dot_file : string Pervasives.ref
val generatesCFile : bool Pervasives.ref
val ltl2ba_params : string
val ltl_to_promela : (string,
Logic_ptree.relation * Promelaast.expression * Promelaast.expression)
Hashtbl.t
val set_ltl_correspondence : (string,
Logic_ptree.relation * Promelaast.expression * Promelaast.expression)
Hashtbl.t -> unit
val convert_ltl_exprs : Promelaast.parsed_condition Promelaast.trans list ->
Promelaast.parsed_condition Promelaast.trans list
val syntax_error : Lexing.position * Lexing.position -> string -> 'a
val ltl_to_ltlLight : string -> string -> unit
val load_ya_file : string -> unit
val load_promela_file : string -> unit
val load_promela_file_withexps : string -> unit
val display_status : unit -> unit
val init_file_names : unit -> bool
val init_test : unit -> unit
val printverb : string -> unit
val output : unit -> unit
val work : unit -> unit
val run : unit -> unit
val run : unit -> unit
val main : unit -> unit