caesar.open [caesar_opt] spec[.lotos] [cc_opt] evaluator [evaluator_opt] prop[.mcl]
exp.open [exp_opt] spec[.exp] [cc_opt] evaluator [evaluator_opt] prop[.mcl]
fsp.open [fsp_opt] spec[.lts] [cc_opt] evaluator [evaluator_opt] prop[.mcl]
lnt.open [lnt_opt] spec[.lnt] [cc_opt] evaluator [evaluator_opt] prop[.mcl]
seq.open [seq_opt] spec[.seq] [cc_opt] evaluator [evaluator_opt] prop[.mcl]
evaluator 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 evaluator 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 new version 4.0 of the model checker is also available as evaluator4 (see the corresponding manual page for details).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 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:
Regular alternation-free mu-calculus allows direct encodings of "pure" branching-time logics like CTL [CES86] or ACTL [DV90], as well as of regular logics like PDL [FL79] or PDL-delta [Str82]. Moreover, it has an efficient model checking algorithm, linear in the size of the formula (number of operators) and the size of the LTS model (number of states and transitions). The logic is built from three types of formulas, indicated in the table below.
+--------+-----------------+ | Symbol | Description | +--------+-----------------+ | A | action formula | | R | regular formula | | F | state formula | +--------+-----------------+
The BNF syntax and the informal semantics of these formulas are defined
below. In the grammar, terminal symbols are written between double quotes.
The axiom of the grammar is the
Identifiers are built from letters,
digits, and underscores (beginning with a letter or an underscore). Keywords
must be written in lowercase. Comments are enclosed between '
(*' and '
comments are not allowed. evaluator is case-sensitive.
The formulas are interpreted over an LTS <S, A, T, s0>, where: S is the set of states, A is the set of actions (transition labels), T is the transition relation (a subset of S * A * S), and s0 is the initial state. A transition (s1, a, s2) of T, also noted s1-a->s2, indicates that the program from which the LTS has been generated can move from state s1 to state s2 by performing action a.
A ::= string | regexp | "true" | "false" | "not" A | A1 "or" A2 | A1 "and" A2 | A1 "implies" A2 | A1 "equ" A2
A string is a sequence of zero or more characters, enclosed between double
"'), which denotes a label of the LTS. A string may contain any
character but '
\n' (end-of-line). Double quotes are also allowed, if preceded
by a backslash ('
\'). Strings can be concatenated using the binary operator
string ::= "(any char but end-of-line)*" | string1 "#" string2
A transition label of the LTS satisfies a string iff it is identical to the corresponding character string (obtained after concatenation whenever needed).
A regexp is a UNIX regular expression (see the regexp
page for a detailed description of UNIX regular expressions), enclosed
between single quotes ('
''), which denotes a predicate on the labels of the
LTS. Regexp's can be concatenated using the binary operator '
#'. Strings can
be concatenated to regexp's, in which case they are implicitly converted
regexp ::= 'UNIX_regular_expression' | regexp1 "#" regexp2 | string1 "#" regexp2 | regexp1 "#" string2
A label of the LTS satisfies a regexp if it matches the corresponding UNIX_regular_expression (obtained after concatenation whenever needed).
Syntactically, all binary operators on action formulas are left-associative.
not" operator has the highest precedence, followed by "
or", followed by "
implies", followed by "
The boolean operators
have the usual semantics: a label of the LTS always satisfies "
never satisfies "
false"; it satisfies "
not" A iff it does not satisfy A;
it satisfies A1 "
or" A2 iff it satisfies A1 or it satisfies A2; it satisfies
and" A2 iff it satisfies both A1 and A2; it satisfies A1 "
A2 iff it does not satisfy A1 or it satisfies A2; it satisfies A1 "
A2 iff either it satisfies both A1 and A2, or none of them.
R ::= A | "nil" | R1 "." R2 | R1 "|" R2 | R "*" | R "+"
nil" is the empty operator, "
." is the concatenation operator,
|" is the choice operator, "
*" is the transitive and reflexive closure
operator, and "
+" is the transitive closure operator.
binary operators on regular formulas are left-associative. The "
*" and "
operators have the highest precedence, followed by "
|", followed by "
A regular formula R denotes a sequence of (consecutive) LTS transitions such that the word obtained by concatenating their labels belongs to the regular language defined by R.
The regular operators have the following semantics:
a sequence of LTS transitions satisfies A iff it has the form s1-a->s2, where
the label a satisfies the formula A; it satisfies "
nil" iff it is empty
(i.e., it contains no transition); it satisfies R1 "
." R2 iff it is the concatenation
of two sequences satisfying R1 and R2, respectively; it satisfies R1 "
R2 iff it satisfies R1 or it satisfies R2; it satisfies R "
*" iff it is
the concatenation of zero or more sequences satisfying R; it satisfies
+" iff it is the concatenation of one or more sequences satisfying R.
F ::= "true" | "false" | "not" F | F1 "or" F2 | F1 "and" F2 | F1 "implies" F2 | F1 "equ" F2 | "<" R ">" F | "[" R "]" F | "@" "(" R ")" | X | "mu" X "." F | "nu" X "." F
<" R "
>" F and "
[" R "
]" F are the possibility and necessity modal
(" R "
)" is the infinite looping operator, "
mu" X "
nu" X "
." F are the minimal and maximal fixed point operators, and
X is a propositional variable.
Syntactically, all binary operators on state
formulas are left-associative. The "
< >", "
[ ]", "
mu", and "
have the highest precedence, followed by "
and", followed by "
implies", followed by "
equ". The fixed point operators act as binders
for the variables X in a way similar to quantifiers in first-order logic.
In each meaningful "
mu" X "
." F or "
nu" X "
." F formula, X is supposed to
have free occurrences inside F. State formulas are assumed to be syntactically
monotonic (i.e., in each fixed point formula "
mu" X "
." F or "
nu" X "
free occurrences of X in F may appear only under an even number of negations
and/or left-hand sides of implications) and alternation-free (i.e., without
mutually recursive minimal and maximal fixed point variables).
operators have the usual semantics: a state of the LTS always satisfies
true"; it never satisfies "
false"; it satisfies "
not" F iff it does not
satisfy F; it satisfies F1 "
or" F2 iff it satisfies F1 or it satisfies
F2; it satisfies F1 "
and" F2 iff it satisfies both F1 and F2; it satisfies
implies" F2 iff it does not satisfy F1 or it satisfies F2; it satisfies
equ" F2 iff either it satisfies both F1 and F2, or none of them.
modal and looping operators have the following semantics: a state of the
LTS satisfies "
<" R "
>" F iff there is (at least) one transition sequence
starting at the state, satisfying R, and leading to a state satisfying
F; it satisfies "
[" R "
]" F iff all transition sequences starting at the
state and satisfying R are leading to states satisfying F; it satisfies
(" R "
)" iff there is a transition sequence starting at the state
and being an infinite concatenation of sequences that satisfy R.
point operators have the following semantics: a state satisfies "
." F iff it belongs to the minimal solution of the fixed point equation
X = F (X), and it satisfies "
nu" X "
." F iff it belongs to the maximal solution
of the same equation, where the propositional variable X denotes a set
of LTS states. Intuitively, minimal (resp. maximal) fixed point operators
allow to characterize finite (resp. infinite) tree-like patterns in the LTS.
An LTS satisfies a state formula F iff its initial state s0 satisfies F.
implies", and "
equ" can be expressed in terms of "
or", and "
not" in the usual way. The diamond and box modalities are dual:
[ R ] F = not < R > not FThe same holds for minimal and maximal fixed point operators:
nu X . F = not mu X . not F (not X)where F
)denotes the syntactic substitution of X by
notX in F. The modalities containing regular expressions can be translated in terms of boolean operators, fixed point operators, and modalities containing only action formulas, by recursively applying the identities below:
< nil > F = < false* > F < R1 . R2 > F = < R1 > < R2 > F < R1 | R2 > F = < R1 > F or < R2 > F < R* > F = mu X . (F or < R > X) < R+ > F = < R . R* > Fwhere X is a "fresh" propositional variable (the corresponding identities for box modalities are obtained by duality). Similarly, the infinite looping operator is equivalent to the maximal fixed point formula below:
@ (R) = nu X . < R > Xwith X a "fresh" propositional variable. Note that, since the fixed point formulas resulting after the above translations must be alternation-free, the regular expressions present inside "
(" R "
)" formulas may not contain "
*" or "
A fixed point formula "
mu" X "
." F or "
nu" X "
." F is
unguarded [Koz83] if F contains at least one free occurrence of X which
is not preceded (not necessarily immediately) by a modality. The evaluation
of an unguarded formula on an LTS may yield a BES with cyclic dependencies
between variables even if the LTS is acyclic.
Note that a state formula
containing regular modalities with nested star operators may yield after
translation an unguarded mu-calculus formula. For example, in the following
< A1** . A2 > true = mu X1 . (< A2 > true or mu X2 . (X1 or < A1 > X2)the free occurrence of X1 is not preceded by any modality, and hence the formula is unguarded. Unguarded occurrences of propositional variables can always be eliminated from a mu-calculus formula, at the price of an increase in size [Koz83,Mat02].
[ true* . "OPEN !1" . (not "CLOSE !1")* . "OPEN !2" ] false
which states that every time process 1 enters its critical section (action "OPEN !1"), it is impossible that process 2 also enters its critical section (action "OPEN !2") before process 1 has left its critical section (action "CLOSE !1").
Other typical safety properties are the invariants, expressing that every state of the LTS satisfies some "good" property. For example, deadlock freedom can be expressed by the formula below:
[ true* ] < true > true
stating that every state has at least one successor. Alternately, this formula may be expressed directly using a fixed point operator:
nu X . (< true > true and [ true ] X)
but less concisely than by using a regular formula.
Potentiality assertions can be directly expressed using diamond modalities containing regular formulas. For instance, the following formula:
< true* . "GET !0" > true
states that there exists a sequence leading to a "GET !0" action after performing zero or more transitions. Regular formulas allow to express succinctly complex potentiality assertions, such as the formula below:
< true* . "SEND" . (true* . "ERROR")* . true* . "RECV" > true
stating that there exists a sequence leading (after zero or more transitions) to a "SEND" action, possibly followed by a sequence of "ERROR" actions (possibly separated by other actions) and leading (after zero or more transitions) to a "RECV" action.
Inevitability assertions can be expressed using fixed point operators. For instance, the following formula:
mu X . (< true > true and [ not "START" ] X)
states that all transition sequences starting at the current state lead to "START" actions after a finite number of steps.
[ true* . "SEND" . (not "RECV")* ] < (not "RECV")* . "RECV" > true
Intuitively, the formula above considers the sequences following the "SEND" action by "skipping" the circuits of the LTS that do not contain "RECV" actions: it states that from every state of such a circuit, there is still a finite sequence leading to a "RECV" action.
< true* . 'SEND !1.*' and not 'SEND !1.*!2' > true
states the potential reachability of an action having the gate SEND and the value of the first offer equal to 1, possibly followed by other offers with values different from 2. Moreover, action formulas combined with modalities allow to express invariants over actions (i.e., action formulas that must be satisfied by all transition labels of the LTS). For instance, the following formula:
[ true* . not ('RECV !.* !.*' and 'RECV !\(.*\) !\1') ] false
states that all message receptions (actions "RECV !source !dest") have
different source and destination fields. Note the use of the UNIX regular
expression construct `
\( \)' allowing to match a portion of a string and to
re-use it later in the same regexp.
"macro" M "(" P1"," ..."," Pn ")" "=" <text> "end_macro"
The above construct defines a macro M having the parameters P1, ..., Pn and the body <text>, which is a string of alpha-numeric characters (normally) containing occurrences of the parameters P1, ..., Pn. For example, the following macro-definition:
macro EU_A (F1, A, F2) = mu X . ((F2) or ((F1) and < A > X)) end_macro
encodes the "Exists Until" operator of ACTL, which states that there exists a sequence of transitions leading to a state satisfying F2 such that all intermediate states satisfy F1 and all intermediate labels satisfy A.
The calls of a macro M have the following form:
M "(" <text1>"," ..."," <textn> ")"
where the arguments <text1>, ..., <textn> are strings. The result of the call is the body <text> of the macro M in which all occurrences of the parameters Pi have been syntactically substituted with the arguments <texti>, for all i between 1 and n. For example, the following call:
EU_A (true, not "SEND", < "RECV" > true)
expands into the formula below:
mu X . ((< "RECV" > true) or ((true) and < not "SEND" > X))
A macro is visible from the point of its definition until the end of the program. The macros may be overloaded: several macros with the same name, but different arities, may be defined in the same scope.
Various macro-definitions (typically encoding the operators of some particular temporal logic) can be grouped into files called libraries. These files may be included in the source program using the following command:
"library" <file0.mcl>"," ..."," <filen.mcl> "end_library"
At the compilation of the program, the above construct is syntactically replaced with the contents of the files <file0.mcl>, ..., <filen.mcl>, placed one after the other in this order. For example, the following command:
library actl.mcl end_library
is syntactically replaced with the content of the file actl.mcl, which implements the ACTL operators.
The included files are searched first in the current directory, then in the directory referenced by $CADP/src/xtl. Multiple inclusions of the same file are silently discarded.
Version 3.0 of evaluator was developed by Radu Mateescu and Mihaela Sighireanu (INRIA/VASY) and used a completely new on-the-fly BES resolution algorithm.
Hubert Garavel suggested the enhancement of action formulas with the string concatenation operator, which was implemented by David Champelovier.
The enhancements leading to the versions 3.5 and 3.6 of evaluator, which use the caesar_solve_1 library of OPEN/CAESAR for on-the-fly BES resolution, were implemented by Radu Mateescu (INRIA/VASY).
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.Radu.Mateescu@inria.fr