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