EVALUATOR manual page
Table of Contents

Name

evaluator - on-the-fly model checking of MCL formulas

Synopsis

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

or:

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

or:

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

or:

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

or:

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

or:

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

Description

evaluator is an on-the-fly model checker of CADP based on the modal mu-calculus. On the theoretical side, evaluator relies on the resolution of Boolean Equation Systems (BES), Parameterized Boolean Equation Systems (PBES) [Mat98a], and Linear Equation Systems (LES). On the practical side, it is implemented using the OPEN/CAESAR framework of CADP for on-the-fly verification.

Basically, evaluator takes two inputs: a state-transition model and a temporal-logic formula. It produces as output a verdict (TRUE or FALSE) indicating whether the model satisfies or not the formula. Optionally, it also produces a diagnostic explaining why the verdict is TRUE or FALSE.

The input model is a Labelled Transition System (LTS), 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.

The temporal-logic formula is expressed in the MCL language and contained in the file prop[.mcl]. See the mcl manual page for a complete definition of the MCL language.

The verification method underlying evaluator is based upon a translation of the model checking problem into the resolution of a PBES, which is carried out by combining two simultaneous on-the-fly activities:

When the MCL formula contains probabilistic operators, the input model is interpreted as a Probabilistic Transition System (PTS), in which transition labels are annotated with probabilities (see the mcl manual page for the definition of the PTS model). The output displayed by evaluator in this case may also contain some probability values, if they are requested by the probabilistic operators contained in prop[.mcl]. The verification method for probabilistic operators is based upon a translation into the resolutions of a PBES and a LES [MR18], which are carried out simultaneously using the algorithms provided by the caesar_solve_1 and caesar_solve_2 libraries of OPEN/CAESAR.

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

-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 REMARKS of the mcl4 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 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.

-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 mcl4 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 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 on standard output using the SEQ format (see the sequence 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 MCL formula is syntactically incorrect. If present, this option has precedence over all the other options. Not a default option.

-epsilon eps
Set the precision of floating-point comparisons to eps, where eps is a real value. When eps is out of [0..1[, evaluator reports an error. Default value for eps is 1E-6. This option has effect only when the MCL formula contains probabilistic operators.

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

-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 manual 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 default.

-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 tool, 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 manual page).

-labels
Display a list of UNIX regular expressions (see the regexp 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 or caesar_rename_1 manual pages for a description of these files).

The formula is not evaluated on spec. 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 in the evaluator_opt section of the command line. Subsequent options and/or arguments, if any, will be discarded. Not a default option.

-warning
Suppress all warning diagnostics, at the risk of leaving actual issues in the MCL formula undetected. 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.

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

[Mat98b]
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 http://cadp.inria.fr/publications/Mateescu-98-b.html

[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

[MR18]
R. Mateescu and J. I. Requeno. "On-the-Fly Model Checking for Extended Action-Based Probabilistic Operators." Springer International Journal on Software Tools for Technology Transfer (STTT), v. 20, no. 5, p. 563-587, 2018.

[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

[MT08]
R. Mateescu and D. Thivolle. "A Model Checking Language for Concurrent Value-Passing Systems." Proceedings of the 15th International Symposium on Formal Methods FM'08, LNCS v. 5014, p. 148-164, 2008. Available from http://cadp.inria.fr/publications/Mateescu-Thivolle-08.html

History and Authors

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. These versions, which accepted as input alternation-free modal mu-calculus (without regular expressions), are no longer available.

Version 3.0 of EVALUATOR handles regular alternation-free mu-calculus (an extension of alternation-free modal mu-calculus with action formulas and regular expressions over action sequences, in which LTS actions are character strings). It was developed by Radu Mateescu and Mihaela Sighireanu (both at INRIA/VASY) and used a completely new on-the-fly BES resolution algorithm [MS03]. Hubert Garavel (INRIA/VASY) suggested the enhancement of action formulas with the string concatenation operator, which was implemented by David Champelovier (INRIA/VASY).

Versions 3.5 and 3.6 of EVALUATOR replaced the dedicated BES resolution algorithm by the more general algorithms available in the caesar_solve_1 library of OPEN/CAESAR for on-the-fly BES resolution. All of this was implemented by Radu Mateescu (INRIA/VASY) and is described in [Mat06].

Version 4.0 of EVALUATOR handles the MCL language, which extends the regular alternation-free mu-calculus with data-handling constructs (data variables, parameterized fixed point operators, programming language constructs, generalized regular formulas over data-passing action sequences), and fairness operators similar to generalized Buchi automata. In this language, LTS actions are tuples containing event names and data values, which can be extracted and used in calculations. Version 4.0 was implemented by Radu Mateescu and Damien Thivolle (both at INRIA/VASY), and is described in [MT08].

Version 5.0 of EVALUATOR handles the MCL language extended with a probabilistic operator enabling to compute the probability of transition sequences characterized by generalized regular formulas. It was implemented by Radu Mateescu (INRIA/CONVECS) and is described in [MR18].

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
MCL 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 , exhibitor , exp , exp.open , fsp.open , lnt.open , lotos , lotos.open , mcl , mcl3 , mcl4 , regexp , sequence , seq.open

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