Module Model


module Model: sig .. end
This module defines the input interface of the model-checking engine, which is given by the signature S below. This signature specifies models given by:
  • a control-flow automaton where transitions are labeled by commands
  • a region algebra to represent sets of environments
  • post/pre operators over regions giving the semantics of the commands
  • an extrapolation operator over regions for abstraction refinement Intuitively, an environment is a valuation of the variables of the model. Variables of the model are not explicit in this interface: one may assume that there is only one variable over some domain whose value is modified by commands. A region represents a subset of this domain, i.e. a set of values of this implicit variable. Thus commands glue together the syntax (control-flow automaton) and the semantics (post/pre operators).


module type COMMAND = sig .. end
The COMMAND signature simply specifies an abstract data-type for commands.
module type AUTOMATON = sig .. end
The AUTOMATON signature specifies the syntactic representation of models.

The REGION signature specifies a boolean algebra that provides a symbolic representation for sets of environments. Elements in this algebra are called regions. Operators over regions (union, intersection and difference) shall be exact.
module type REGION = sig .. end
module type SEMANTICS = sig .. end
The SEMANTICS signature specifies how the semantics of the model shall be given to the model-checking engine.
module type CLOSURE = sig .. end
The CLOSURE signature specifies a hierarchy of extensive idempotent operators on a Region module.
module type SEMANTICS_CLOSURE = sig .. end
Aggregation of SEMANTICS and CLOSURE over the same region algebra.
module type S = sig .. end
The main signature of this module, defining the input interface of the model-checking engine.