Module Model
module Model: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:sig
..end
- 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.