sig
  module Common :
    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
  module Reverse : functor (E : TraceChecker.S-> TraceChecker.S
  module DiscardStates : functor (E : TraceChecker.S-> TraceChecker.S
  module Validate : functor (E : TraceChecker.S-> TraceChecker.S
end