Module StaticAnalyzer.Make
module Make:ModelChecker.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 |
(* | Safety certificate: forward inductive invariant disjoint from error symbolic states, and backward inductive invariant disjoint from initial symbolic states. | *) |
| |
Counterexample of |
(* | 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 |
(* | 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.