EVALUATOR5 manual page
Table of Contents

Name

evaluator5 - on-the-fly model checking of MCL v5 formulas

Synopsis

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

or:

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

or:

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

or:

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

or:

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

or:

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

Description

evaluator5 takes two inputs:

evaluator5 performs an on-the-fly verification of the temporal property on the given PTS. The result of this verification (TRUE or FALSE, preceded by the values of probabilities if they are requested by the probabilistic operators contained in prop[.mcl]) is displayed.

The verification method underlying evaluator5 is based upon a translation of the probabilistic model checking problem into the resolutions of a Linear Equation System (LES) and a Parameterized Boolean Equation System (PBES), as described in [MR18]. These resolutions are carried out simultaneously and on the fly, using the algorithms provided by the caesar_solve_1 and caesar_solve_2 libraries of OPEN/CAESAR (see the corresponding manual pages and the articles [Mat06,MR18] 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 options evaluator_opt are the same as those of evaluator4 (see the evaluator4 manual page), with the following addition:

-epsilon eps
Set the precision of certain floating-point comparisons to eps, where eps is a real value. When eps is out of [0..1[, evaluator5 reports an error. Default value for eps is 1E-6.

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

[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) 8(1):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) 20(5):563-587, 2018. Available from http://hal.inria.fr/hal-01862754/en

Authors

Version 5.0 of EVALUATOR handles version 5 of the MCL language. It was implemented by Radu Mateescu (INRIA/CONVECS).

For the previous versions of EVALUATOR, 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
MCL version 5 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_solve_2 , caesar , evaluator4 , exhibitor , exp , exp.open , fsp.open , lnt.open , lotos , lotos.open , mcl , regexp , seq , 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