Module type ModelChecker.S


module type S = functor (A : Model.S) -> sig .. end
Parameters:
A : Model.S


Specification of (and checking functions for) the result of model-checking functions is provided in the Validator module. See the documentation of the Validator module for more information on the result type below.

type result =
| Invariant of A.State.t list Lazy.t option * A.State.t list Lazy.t option (*Safety certificate: forward inductive invariant disjoint from error symbolic states, and backward inductive invariant disjoint from initial symbolic states.*)
| Counterexample of A.Automaton.Transition.t list (*Safety counterexample: path in the model's automaton that is feasible (i.e. corresponds to a run of the model) with respect to (1) the model's semantics and (2) the model's initial and error symbolic states.*)
| Abort of string (*Model checking abortion, with a message string.*)
Type of possible results of the model-checking function.
val model_check : unit -> result
The model-checking function.