Table of Contents
evaluator3 - on-the-fly model checking of MCL v3 formulas
[exp_opt] spec[.exp] [cc_opt] evaluator3 [evaluator_opt] prop[.mcl]
[fsp_opt] spec[.lts] [cc_opt] evaluator3 [evaluator_opt] prop[.mcl]
[lnt_opt] spec[.lnt] [cc_opt] evaluator3 [evaluator_opt] prop[.mcl]
[lotos_opt] spec[.lotos] [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 composition expression
spec.exp, an FSP program spec.lts, an LNT program spec.lnt, a LOTOS program
spec.lotos, 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 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 lotos_opt, if any, are passed to caesar
and to caesar.adt
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, .xz, 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
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.
- 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 Section EXAMPLES OF TEMPORAL PROPERTIES
in the mcl3
manual page). Default option.
- -diag [ diag[.bcg] ]
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
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 SEQ format (see the seq
manual page for the definition of this format). Not a default option.
- Display the list of library files included (directly or transitively) in
the file prop[.mcl] and stop. This list may be incomplete if the formula
is syntactically incorrect. If present, this option has precedence over
all the other options. 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.
- Execute silently. Opposite of -verbose. Default
- -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.
- 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
See the AUTHORS section of the evaluator
- BCG graph (input)
- network of communicating LTSs (input)
- FSP specification (input)
- LNT specification (input)
- LOTOS specification (input)
- sequence file (input)
mu-calculus formula (input)
- 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 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