Module Armc.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.