Module ModelChecker
module ModelChecker:Model Checker.sig..end
 This module defines the interface of model-checking engines, as a functor
 taking as argument a module for the model to be model-checked, and returning
 a module with a model-checking function.  The interface used for models is
 defined in the Model module.
module type S =functor (A:Model.S) ->sig..end