sig
  exception Terminate
  type 'a log_printer =
      Lib.log_level ->
      ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a
  type 'a m_log_printer = Lib.kind_module -> 'a log_printer
  val set_module : Lib.kind_module -> unit
  val get_module : unit -> Lib.kind_module
  type log_format = F_pt | F_xml | F_json | F_relay
  val get_log_format : unit -> log_format
  val set_log_format : log_format -> unit
  val set_log_format_pt : unit -> unit
  val set_log_format_xml : unit -> unit
  val set_log_format_json : unit -> unit
  val unset_relay_log : unit -> unit
  val pp_print_kind_module_xml_src :
    Format.formatter -> Lib.kind_module -> unit
  val print_xml_trailer : unit -> unit
  val printf_xml : 'a m_log_printer
  val printf_json : 'a m_log_printer
  val parse_log_xml : Lib.log_level -> Lib.position -> string -> unit
  val parse_log_json : Lib.log_level -> Lib.position -> string -> unit
  val log : 'Log.log_printer
  val log_uncond : ('a, Format.formatter, unit) format -> 'a
  val set_relay_log : unit -> unit
  val log_step_cex :
    Lib.kind_module ->
    Lib.log_level ->
    'InputSystem.t ->
    Analysis.param ->
    TransSys.t -> string -> (StateVar.t * Model.value list) list -> unit
  val log_disproved :
    Lib.kind_module ->
    Lib.log_level ->
    'InputSystem.t ->
    Analysis.param ->
    TransSys.t -> string -> (StateVar.t * Model.value list) list -> unit
  val log_proved :
    Lib.kind_module ->
    Lib.log_level -> TransSys.t -> int option -> string -> unit
  val log_prop_status :
    Lib.log_level ->
    TransSys.t -> (string * Property.prop_status) list -> unit
  val log_stat :
    Lib.kind_module ->
    Lib.log_level -> (string * Stat.stat_item list) list -> unit
  val terminate_log : unit -> unit
  val log_run_end : Analysis.result list -> unit
  val log_analysis_start : TransSys.t -> Analysis.param -> unit
  val log_analysis_end : Analysis.result -> unit
  val log_post_analysis_start : string -> string -> unit
  val log_post_analysis_end : unit -> unit
  val log_timeout : bool -> unit
  val log_interruption : int -> unit
  type event =
      Invariant of string list * Term.t * Certificate.t * bool
    | PropStatus of string * Property.prop_status
    | StepCex of string * (StateVar.t * Model.value list) list
  val pp_print_event : Format.formatter -> Event.event -> unit
  val all_stats :
    unit -> (Lib.kind_module * (string * Stat.stat_item list) list) list
  val stat : (string * Stat.stat_item list) list -> unit
  val progress : int -> unit
  val invariant : string list -> Term.t -> Certificate.t -> bool -> unit
  val step_cex :
    'InputSystem.t ->
    Analysis.param ->
    TransSys.t -> string -> (StateVar.t * Model.value list) list -> unit
  val prop_status :
    Property.prop_status ->
    'InputSystem.t -> Analysis.param -> TransSys.t -> string -> unit
  val execution_path :
    'InputSystem.t ->
    Analysis.param ->
    TransSys.t -> (StateVar.t * Model.value list) list -> unit
  val terminate : unit -> unit
  val recv : unit -> (Lib.kind_module * Event.event) list
  val update_child_processes_list : (int * Lib.kind_module) list -> unit
  val check_termination : unit -> unit
  val update_trans_sys_sub :
    'InputSystem.t ->
    Analysis.param ->
    TransSys.t ->
    (Lib.kind_module * Event.event) list ->
    (Term.TermSet.t * Term.TermSet.t) Scope.Map.t *
    (Lib.kind_module * (string * Property.prop_status)) list
  val update_trans_sys :
    'InputSystem.t ->
    Analysis.param ->
    TransSys.t ->
    (Lib.kind_module * Event.event) list ->
    (Term.TermSet.t * Term.TermSet.t) *
    (Lib.kind_module * (string * Property.prop_status)) list
  type messaging_setup
  type mthread
  val setup : unit -> Event.messaging_setup
  val run_im :
    Event.messaging_setup ->
    (int * Lib.kind_module) list -> (exn -> unit) -> unit
  val run_process :
    Lib.kind_module ->
    Event.messaging_setup -> (exn -> unit) -> Event.mthread
  val exit : Event.mthread -> unit
  val pp_print_path_pt :
    'InputSystem.t ->
    Analysis.param ->
    TransSys.t ->
    '-> Format.formatter -> (StateVar.t * Model.value list) list -> unit
end