Module type Model.S


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