module type S = sig
.. end
The main signature of this module, defining the input interface of the
model-checking engine. This signature basically is a container for the
above signatures. Note that the module equality constraints given in
this signature really means that the modules should be the same. However
the OCaml typing system only checks that type equality constraints are
satified.
module Command: Model.COMMAND
module Automaton: Model.AUTOMATON
with module Command = Command
module Semantics: Model.SEMANTICS
with module Command = Command
module Closure: Model.CLOSURE
with module Region = Semantics.Region
module State: Print.PRINTABLE_TYPE
with type t = Automaton.Location.t * Semantics.Region.t
val nb_init : int
val nb_error : int
val iter_init : (State.t -> unit) -> unit
val iter_error : (State.t -> unit) -> unit
val fold_init : (State.t -> 'a -> 'a) -> 'a -> 'a
val fold_error : (State.t -> 'a -> 'a) -> 'a -> 'a
val print_model : Format.formatter -> unit -> unit