Table of Contents
evaluator3 - on-the-fly model checking of MCL v3 formulas
[caesar_opt] spec[.lotos] [cc_opt] evaluator3 [evaluator_opt] prop[.mcl]
exp.open [exp_opt] spec[.exp] [cc_opt] evaluator3 [evaluator_opt] prop[.mcl]
fsp.open [fsp_opt] spec[.lts] [cc_opt] evaluator3 [evaluator_opt] prop[.mcl]
lnt.open [lnt_opt] spec[.lnt] [cc_opt] evaluator3 [evaluator_opt] prop[.mcl]
seq.open [seq_opt] spec[.seq] [cc_opt] evaluator3 [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 version 3.
evaluator3 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 below).
Note: The verification method underlying the current
version of evaluator3 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 newer version of the model checker is
also available as evaluator4
(see the corresponding manual page
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 to fsp.open
The options lnt_opt, if any, are passed
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 evaluator3 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.
- -source file:line
- Change the
file name and line number displayed in error messages as if the formula
was contained in file file starting at line line (instead of starting at
line 1 in file prop[.mcl]). This option has effect only on the messages triggered
by the errors occurring in the top-level file prop[.mcl]. The messages triggered
by the errors occurring in the included libraries (if any) are left unchanged.
- 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.
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
See the AUTHORS section of the evaluator
- BCG graph (input)
- network of communicating LTSs (input)
- LOTOS specification (input)
- FSP specification (input)
- LNT specification (input)
- sequence file (input)
- regular mu-calculus formula (input)
- diagnostic in BCG format (output)
- BES in textual format (output)
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