Table of Contents
evaluator4 - on-the-fly model checking of MCL v4 formulas
[caesar_opt] spec[.lotos] [cc_opt] evaluator4 [evaluator_opt] prop[.mcl]
exp.open spec[.exp] [cc_opt] evaluator4 [evaluator_opt] prop[.mcl]
fsp.open [fsp_opt] spec[.lts] [cc_opt] evaluator4 [evaluator_opt] prop[.mcl]
lnt.open [lnt_opt] spec[.lnt] [cc_opt] evaluator4 [evaluator_opt] prop[.mcl]
seq.open spec[.seq] [cc_opt] evaluator4 [evaluator_opt] prop[.mcl]
(also referred below as evaluator
4.0) takes two inputs:
- A Labelled Transition
System, expressed either as a BCG graph spec.bcg, a LOTOS program spec.lotos,
a composition expression spec.exp, an FSP program spec.lts, an LNT program
spec.lnt, or a sequence file spec.seq.
- A temporal logic property, contained
in the file prop[.mcl], expressed as a formula in the MCL version 4 language.
See the mcl
manual page for a complete definition of the MCL v4
evaluator4 performs an on-the-fly verification of the temporal property
on the given Labelled Transition System (LTS for short). The result of this
verification (TRUE or FALSE) is displayed, possibly accompanied by a diagnostic
(see OPTIONS below).
The verification method underlying version 4.0 of evaluator
is based upon a translation of the model checking problem into the resolution
of a Parameterized Boolean Equation System (PBES) [Mat98a], which is carried
out by combining two simultaneous on-the-fly activities:
- Instantiation of
the PBES to yield a plain Boolean Equation System (BES), using the approach
proposed in [Mat98b].
- Resolution of the resulting BES, using the algorithms
provided by the caesar_solve_1
library of OPEN/CAESAR (see the corresponding
manual page and the article [Mat06] for details).
The options bcg_opt
if any, are passed to bcg_lib
The options caesar_opt, if any, are
passed to caesar
and to caesar.adt
The options exp_opt, if
any, are passed to exp.open
The options fsp_opt, if any, are passed
The options lnt_opt, if any, are passed to lnt.open
The options seq_opt, if any, are passed to seq.open
The options cc_opt,
if any, are passed to the C compiler.
The following options evaluator_opt
are currently available:
- -bes [ file[.bes[.ext]] ]
- Print in file[.bes] or,
if the file name argument is missing, in file evaluator.bes, a textual description
of the BES corresponding to the evaluation of the formula on the LTS. If
present, the extension .ext must correspond to a known file compression
format (e.g., .Z, .gz, .bz2, etc.). In this case, the file containing the BES
is compressed according to the corresponding format. The list of currently
supported extensions and compression formats is given by the $CADP/src/com/cadp_zip
shell-script. This option does not influence the evaluation of the formula.
Not a default option.
- Assume that the property is specified as a system
of modal equations in a file file[.blk] that must be given as argument to
evaluator4 instead of prop[.mcl]. This option is mainly intended for debugging
purposes. The format of the input file is undocumented and subject to future
changes. Not a default option.
- Evaluate the formula on the LTS using
an algorithm optimized for acyclic graphs. If option -dfs is present (which
is the case by default), the tool checks during verification whether the
LTS contains cycles; if this is the case, an error message is displayed
and the execution is aborted. If option -bfs is present, the tool may not
always detect the presence of cycles in the LTS, and hence it may enter
an infinite loop; in this case, it is the user's responsibility to ensure
that the LTS is acyclic. If the formula is unguarded (see Section REMARKS
of the mcl
manual page), which may yield a BES with cyclic dependencies
between variables even if the LTS is acyclic, an error message is displayed
and the execution is aborted. Not a default option.
- Evaluate the formula
on the LTS using a breadth-first search algorithm. Compared to -dfs, this
option is generally slower, but produces diagnostics of smaller depth. If
option -acyclic is present, the breadth-first search algorithm is optimized
for reducing memory consumption: in particular, if the LTS is a sequence
and the formula is dataless, the memory used for verification is bounded
by the size of the formula (number of operators) and independent of the
length of the sequence (number of transitions). Not a default option.
- Evaluate the formula on the LTS using a depth-first search algorithm. Compared
to -bfs, this option produces diagnostics of greater depth, but is generally
faster and consumes less memory for certain classes of formulas (such as
those shown in EXAMPLES OF TEMPORAL PROPERTIES below). Default option.
[ diag[.bcg] ]
- Generate a diagnostic in BCG format (see the bcg
page for details) explaining the truth value of the formula. The diagnostic
is generated in the file diag[.bcg] or, if the file name argument is missing,
in the file evaluator.bcg. The BCG files containing diagnostics can be visualized
using the bcg_draw
tools of CADP (see the respective
manual pages for details). Diagnostics are (usually small) portions of the
LTS on which the formula yields the same result as when it is evaluated
on the whole LTS. If the diagnostic is a sequence of LTS transitions, it
will also be displayed using the SEQUENCE format (see the exhibitor
manual page for the definition of the SEQUENCE format). Not a default option.
- Expand the macro definitions and the source files included as libraries
in the file prop[.mcl], producing as output a file prop.xm, and stop. This
option is useful for debugging purposes. Not a default option.
- -hide [ -total
| -partial | -gate ] hiding_filename
- Use the hiding rules defined in hiding_filename
to hide (on-the-fly) the labels of spec. See the caesar_hide_1
page for a detailed description of the appropriate format for hiding_filename.
The -total, -partial, and -gate options specify the "total matching", "partial
matching", and "gate matching" semantics, respectively. See the caesar_hide_1
manual page for more details about these semantics. Option -total is the
- -rename [-total|-single|-multiple|-gate] renaming_filename
- Use the renaming
rules defined in renaming_filename to rename (on-the-fly) the labels of spec.
See the caesar_rename_1
manual page for a detailed description of
the appropriate format for renaming_filename.
The -total, -single, -multiple,
and -gate options specify the "total matching", "single partial matching",
"multiple partial matching", and "gate matching" semantics, respectively.
See the caesar_rename_1
manual page for more details about these
semantics. Option -total is the default.
As for the bcg_labels
several hiding and/or renaming options can be present on the command line,
in which case they are processed from left to right.
The hiding and renaming
options are useful for converting the transition labels of spec on-the-fly
in order to make them compatible with the LTS model on which MCL formulas
are interpreted (see Section OVERVIEW OF THE MCL LANGUAGE of the mcl
- Display a list of UNIX regular expressions (see the
manual page for a detailed description of UNIX regular expressions),
which over-approximate the set of visible LTS actions (transition labels)
satisfying the action predicates occurring in the formula. In other words,
if an action a satisfies some action predicate, then there exists a regular
expression among those displayed by this option such that a matches it.
Each regular expression is written on a separate line and is enclosed between
double quotes, thus being compatible with the format of labels in hiding
and renaming files (see the caesar_hide_1
manual pages for a description of these files).
The formula is not evaluated
on spec. Not a default option.
- Execute silently. Opposite of -verbose.
- Display statistical information about the resolution
of the BES corresponding to the evaluation of the formula on the LTS. Not
a default option.
- Reduce the LTS on the fly modulo tau-confluence
(a form of partial order reduction that preserves branching equivalence)
while evaluating the formula. This option can be safely used only for verifying
formulas adequate w.r.t. branching equivalence, i.e., whose evaluation yields
the same result on all branching equivalent LTSs. For example, formulas
belonging to the fragment ACTL-X (i.e., ACTL without the next time operators)
are adequate w.r.t. branching equivalence [DV90]. In some cases, this option
may improve speed and memory consumption significantly. Not a default option.
- Animate the user's screen, telling what is going on. Opposite of
-silent. Default option is -silent.
- Display the current version number
of the tool and stop. To be effective, this option should occur as the first
argument in the evaluator_opt section of the command line. Subsequent options
and/or arguments, if any, will be discarded. Not a default option.
- Suppress all warning diagnostics, at the risk of leaving actual issues
in the MCL formula undetected. Not a default option.
is 0 if everything is alright, 1 otherwise.
When the source file
] is erroneous, error messages are issued.
De Nicola and F. W. Vaandrager. "Action versus State based Logics for Transition
Systems." Proceedings Ecole de Printemps on Semantics of Concurrency, LNCS
v. 469, p. 407-419, 1990.
- R. Mateescu. "Verification des proprietes
temporelles des programmes paralleles." PhD Thesis, Institut National Polytechnique
de Grenoble, April 1998. Available from http://cadp.inria.fr/publications/Mateescu-98-a.html
- R. Mateescu. "Local Model-Checking of an Alternation-Free Value-Based
Modal Mu-Calculus." Proceedings of the 2nd International Workshop on Verification,
Model Checking and Abstract Interpretation VMCAI'98, 1998. Available from
- R. Mateescu. "CAESAR_SOLVE:
A Generic Library for On-the-Fly Resolution of Alternation-Free Boolean Equation
Systems." Springer International Journal on Software Tools for Technology
Transfer (STTT), v. 8, no. 1, p. 37-56, 2006. Full version available as INRIA
Research Report RR-5948. Available from http://cadp.inria.fr/publications/Mateescu-06-a.html
Versions 1.x and 2.x of evaluator
were developed by Marius Dorel Bozga
(IMAG) and used an on-the-fly BES resolution algorithm proposed by J-C. Fernandez
and L. Mounier.
Version 3.0 of evaluator was developed by Radu Mateescu and
Mihaela Sighireanu (both at INRIA/VASY) and used a completely new on-the-fly
BES resolution algorithm.
Hubert Garavel (INRIA/VASY) suggested the enhancement
of action formulas with the string concatenation operator, which was implemented
by David Champelovier (INRIA/VASY).
The enhancements leading to version
3.5 of evaluator, which uses the caesar_solve_1
library of OPEN/CAESAR
for on-the-fly BES resolution, were implemented by Radu Mateescu (INRIA/VASY).
Version 4.0 of evaluator, which handles the full MCL language, was implemented
by Radu Mateescu and Damien Thivolle (both at INRIA/VASY).
- BCG graph (input)
- network of communicating LTSs (input)
- LOTOS specification (input)
- FSP specification (input)
- sequence file (input)
- regular mu-calculus
- diagnostic in BCG format (output)
- BES in
textual format (output)
- predefined libraries
Additional information is available from the CADP Web page
located at http://cadp.inria.fr
Directives for installation are given in
Recent changes and improvements to this software
are reported and commented in file $CADP/HISTORY.
Please report bugs
Table of Contents