EVALUATOR3 manual page
Table of Contents

Name

evaluator3 - on-the-fly model checking of MCL v3 formulas

Synopsis

bcg_open [bcg_opt] spec[.bcg] [cc_opt] evaluator3 [evaluator_opt] prop[.mcl]

or:

exp.open [exp_opt] spec[.exp] [cc_opt] evaluator3 [evaluator_opt] prop[.mcl]

or:

fsp.open [fsp_opt] spec[.lts] [cc_opt] evaluator3 [evaluator_opt] prop[.mcl]

or:

lnt.open [lnt_opt] spec[.lnt] [cc_opt] evaluator3 [evaluator_opt] prop[.mcl]

or:

lotos.open [lotos_opt] spec[.lotos] [cc_opt] evaluator3 [evaluator_opt] prop[.mcl]

or:

seq.open [seq_opt] spec[.seq] [cc_opt] evaluator3 [evaluator_opt] prop[.mcl]

Description

evaluator3 takes two different inputs:

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 for details).

Options

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 to lnt.open .

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.

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, .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.

-block
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.

-acyclic
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.

-bfs
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.

-dfs
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] ]
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 and bcg_edit 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.

-depend
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
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.

-silent
Execute 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.

-stat
Display statistical information about the resolution of the BES corresponding to the evaluation of the formula on the LTS. Not a default option.

-tauconfluence
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.

-verbose
Animate the user's screen, telling what is going on. Opposite of -silent. Default option is -silent.

-version
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.

Exit Status

Exit status is 0 if everything is alright, 1 otherwise.

Diagnostics

When the source file prop[.mcl] is erroneous, error messages are issued.

Bibliography

[DV90]
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.

[Mat06]
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

[MS03]
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

Authors

See the AUTHORS section of the evaluator manual page.

Operands

spec.bcg
BCG graph (input)

spec.exp
network of communicating LTSs (input)

spec.lts
FSP specification (input)

spec.lnt
LNT specification (input)

spec.lotos
LOTOS specification (input)

spec.seq
sequence file (input)

prop.mcl
regular mu-calculus formula (input)

diag.bcg
diagnostic in BCG format (output)

file.bes
BES in textual format (output)

Files

$CADP/src/mcl/*.mcl
predefined libraries (input)

See Also

bcg , bcg_open , caesar.adt , caesar_graph , caesar_solve_1 , caesar , evaluator , evaluator4 , exhibitor , exp , exp.open , fsp.open , lnt.open , lotos , lotos.open , mcl , mcl3 , mcl4 , seq , seq.open , regexp

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.

Bugs

Please report bugs to Radu.Mateescu@inria.fr

Table of Contents