sig
  module type COMMAND =
    sig
      type t
      val print : Format.formatter -> t -> unit
      type t_command = Internal | Input | Output
      val give_type : t -> Model.COMMAND.t_command
      val give_queue : t -> int
      val give_message : t -> string
    end
  module type 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 : COMMAND
      module Transition :
        sig
          type t
          val print : Format.formatter -> t -> unit
          val owner : t -> Model.AUTOMATON.Owner.t
          val is_controllable : t -> bool
          val source : t -> Model.AUTOMATON.Location.t
          val target : t -> Model.AUTOMATON.Location.t
          val command : t -> Command.t
        end
      val nb_locations : int
      val nb_transitions : int
      val nb_owners : int
      val iter_locations : (Model.AUTOMATON.Location.t -> unit) -> unit
      val iter_transitions : (Model.AUTOMATON.Transition.t -> unit) -> unit
      val iter_owners : (Model.AUTOMATON.Owner.t -> unit) -> unit
      val fold_locations :
        (Model.AUTOMATON.Location.t -> '-> 'a) -> '-> 'a
      val fold_transitions :
        (Model.AUTOMATON.Transition.t -> '-> 'a) -> '-> 'a
      val fold_owners : (Model.AUTOMATON.Owner.t -> '-> 'a) -> '-> 'a
      val iter_out_transitions :
        (Model.AUTOMATON.Transition.t -> unit) ->
        Model.AUTOMATON.Location.t -> unit
      val iter_in_transitions :
        (Model.AUTOMATON.Transition.t -> unit) ->
        Model.AUTOMATON.Location.t -> unit
      val fold_out_transitions :
        (Model.AUTOMATON.Transition.t -> '-> 'a) ->
        Model.AUTOMATON.Location.t -> '-> 'a
      val fold_in_transitions :
        (Model.AUTOMATON.Transition.t -> '-> 'a) ->
        Model.AUTOMATON.Location.t -> '-> 'a
      val print_automaton : Format.formatter -> unit -> unit
    end
  module type REGION =
    sig
      type 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
  module type SEMANTICS =
    sig
      module Region : REGION
      module Command : COMMAND
      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 type CLOSURE =
    sig module Region : REGION val clo : int -> Region.t -> Region.t end
  module type SEMANTICS_CLOSURE =
    sig
      module Region : REGION
      module Command : COMMAND
      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
      val clo : int -> Region.t -> Region.t
    end
  module type S =
    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
end