functor (A : Model.SEMANTICS_CLOSURE->
  sig
    module Atom :
      sig
        type 'a t =
            [ `Command of A.Command.t
            | `Guard of A.Region.t
            | `State of 'a * A.Region.t ]
        val print :
          (Format.formatter -> '-> unit) ->
          Format.formatter -> 'a t -> unit
      end
    module Trace :
      sig
        type 'a t = 'Atom.t Util.Sequence.t
        val print :
          (Format.formatter -> '-> unit) ->
          Format.formatter -> 'a t -> unit
      end
    module Result :
      sig
        type 'a invariant =
            int * (('a * A.Region.t) * A.Region.t) Util.Sequence.t * int
        type 'a t =
            [ `Feasible of [ `Strong | `Weak ]
            | `Invariant_backward of 'a invariant
            | `Invariant_forward of 'a invariant ]
        val print :
          (Format.formatter -> '-> unit) ->
          Format.formatter -> 'a t -> unit
      end
    val atom_strong_post : A.Region.t -> 'Atom.t -> A.Region.t
    val atom_strong_pre : A.Region.t -> 'Atom.t -> A.Region.t
    val atom_weak_post : A.Region.t -> 'Atom.t -> A.Region.t
    val atom_weak_pre : A.Region.t -> 'Atom.t -> A.Region.t
    val num_state_atoms : 'Atom.t array -> int -> int -> int
    val reduce_fwd_invariant : 'Result.invariant -> 'Result.invariant
    val reduce_bwd_invariant : 'Result.invariant -> 'Result.invariant
  end