Table of Contents
evaluator - on-the-fly model checking of MCL v3 formulas
[caesar_opt] spec[.lotos] [cc_opt] evaluator [evaluator_opt] prop[.mcl]
exp.open [exp_opt] spec[.exp] [cc_opt] evaluator [evaluator_opt] prop[.mcl]
fsp.open [fsp_opt] spec[.lts] [cc_opt] evaluator [evaluator_opt] prop[.mcl]
lnt.open [lnt_opt] spec[.lnt] [cc_opt] evaluator [evaluator_opt] prop[.mcl]
seq.open [seq_opt] spec[.seq] [cc_opt] evaluator [evaluator_opt] prop[.mcl]
takes two different 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 MCL version 3 formula (i.e., a formula
of the regular alternation-free mu-calculus). See the mcl3
for a complete definition of MCL v3.
evaluator 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 on
the standard output, possibly accompanied by a diagnostic (see OPTIONS
Note: The verification method underlying the current version of
evaluator is based upon a translation of the model checking problem into
the resolution of a Boolean Equation System (BES), which is performed on-the-fly
using the algorithms provided by the caesar_solve_1
library of OPEN/CAESAR
(see the corresponding manual page and the article [Mat06] for details).
Complete descriptions of regular alternation-free mu-calculus and of the
verification method are available in [MS03] (the reference article for
version 3.0 of evaluator) and in [Mat06] (the reference article for versions
3.5 and 3.6 of evaluator).
A new version 4.0 of the model checker is also available
(see the corresponding manual page for details).
, if any, are passed to bcg_lib
The options caesar_opt,
if any, are passed to caesar
and to caesar.adt
exp_opt, if any, are passed to exp.open
The options fsp_opt, if any,
are passed to fsp.open
The options lnt_opt, if any, are passed to
The options seq_opt, if any, are passed to seq.open
The options cc_opt, if any, are passed to the C compiler.
options evaluator_opt are currently available:
- -bes [ file[.bes[.ext]] ]
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 evaluator 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
STATE FORMULAS of the mcl3
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, 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.
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 Section EXAMPLES OF TEMPORAL PROPERTIES in the mcl3
manual page). Default option.
- -diag [ diag[.bcg] ]
- Generate a diagnostic in
BCG format (see the bcg
manual 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 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
on standard output 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.
silently. Opposite of -verbose. Default option.
- 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 on the command line. Subsequent options
and/or arguments, if any, will be discarded. Not a default option.
status is 0 if everything is alright, 1 otherwise.
When the source
] is erroneous, error messages are issued.
- R. 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. "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
- R. Mateescu and M. Sighireanu. "Efficient On-the-Fly Model-Checking for Regular
Alternation-Free Mu-Calculus." Science of Computer Programming, v. 46, no. 3,
p. 255-281, 2003. Available from http://cadp.inria.fr/publications/Mateescu-Sighireanu-03.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 (INRIA/VASY) and used a completely new on-the-fly BES
Hubert Garavel suggested the enhancement of action
formulas with the string concatenation operator, which was implemented
by David Champelovier (INRIA/VASY).
The enhancements leading to the versions
3.5 and 3.6 of evaluator, which use the caesar_solve_1
OPEN/CAESAR for on-the-fly BES resolution, were implemented by Radu Mateescu
- BCG graph (input)
- network of communicating
- LOTOS specification (input)
- FSP specification
- LNT specification (input)
- sequence file (input)
- regular mu-calculus formula (input)
- diagnostic in BCG format
- BES in textual format (output)
- predefined libraries (input)
Additional information is available
from the CADP Web page located at http://cadp.inria.fr
Directives for installation
are given in files $CADP/INSTALLATION_*.
Recent changes and improvements
to this software are reported and commented in file $CADP/HISTORY.
report bugs to Radu.Mateescu@inria.fr
Table of Contents