functor (A : Model.S->
  sig
    type result =
        Invariant of A.State.t list Lazy.t option *
          A.State.t list Lazy.t option
      | Counterexample of A.Automaton.Transition.t list
      | Abort of string
    val model_check : unit -> ModelChecker.S.result
  end