sig
  module Command : COMMAND
  module Automaton :
    sig
      module Owner :
        sig
          type t
          val print : Format.formatter -> t -> unit
          val compare : t -> t -> int
          val equal : t -> t -> bool
          val hash : t -> int
        end
      module Location :
        sig
          type t
          val print : Format.formatter -> t -> unit
          val compare : t -> t -> int
          val equal : t -> t -> bool
          val hash : t -> int
        end
      module Command :
        sig
          type t = Command.t
          val print : Format.formatter -> t -> unit
          type t_command = Command.t_command = Internal | Input | Output
          val give_type : t -> t_command
          val give_queue : t -> int
          val give_message : t -> string
        end
      module Transition :
        sig
          type t
          val print : Format.formatter -> t -> unit
          val owner : t -> Owner.t
          val is_controllable : t -> bool
          val source : t -> Location.t
          val target : t -> Location.t
          val command : t -> Command.t
        end
      val nb_locations : int
      val nb_transitions : int
      val nb_owners : int
      val iter_locations : (Location.t -> unit) -> unit
      val iter_transitions : (Transition.t -> unit) -> unit
      val iter_owners : (Owner.t -> unit) -> unit
      val fold_locations : (Location.t -> '-> 'a) -> '-> 'a
      val fold_transitions : (Transition.t -> '-> 'a) -> '-> 'a
      val fold_owners : (Owner.t -> '-> 'a) -> '-> 'a
      val iter_out_transitions : (Transition.t -> unit) -> Location.t -> unit
      val iter_in_transitions : (Transition.t -> unit) -> Location.t -> unit
      val fold_out_transitions :
        (Transition.t -> '-> 'a) -> Location.t -> '-> 'a
      val fold_in_transitions :
        (Transition.t -> '-> 'a) -> Location.t -> '-> 'a
      val print_automaton : Format.formatter -> unit -> unit
    end
  module Semantics :
    sig
      module Region : REGION
      module Command :
        sig
          type t = Command.t
          val print : Format.formatter -> t -> unit
          type t_command = Command.t_command = Internal | Input | Output
          val give_type : t -> t_command
          val give_queue : t -> int
          val give_message : t -> string
        end
      val post : Region.t -> Command.t -> Region.t
      val pre : Region.t -> Command.t -> Region.t
      val rel : Command.t -> Region.t -> Region.t -> bool
    end
  module Closure :
    sig
      module Region :
        sig
          type t = Semantics.Region.t
          val print : Format.formatter -> t -> unit
          val bot : t
          val top : t
          val eq : t -> t -> bool
          val leq : t -> t -> bool
          val union : t -> t -> t
          val inter : t -> t -> t
          val compl : t -> t
          val minus : t -> t -> t
          val simplify : t -> t
          val size : t -> int
          val dump : Format.formatter -> t -> unit
        end
      val clo : int -> Region.t -> Region.t
    end
  module State :
    sig
      type t = Automaton.Location.t * Semantics.Region.t
      val print : Format.formatter -> t -> unit
    end
  val nb_init : int
  val nb_error : int
  val iter_init : (Model.S.State.t -> unit) -> unit
  val iter_error : (Model.S.State.t -> unit) -> unit
  val fold_init : (Model.S.State.t -> '-> 'a) -> '-> 'a
  val fold_error : (Model.S.State.t -> '-> 'a) -> '-> 'a
  val print_model : Format.formatter -> unit -> unit
end