Promela |
Meta Term |
ltl |
NAME
ltl -
linear time temporal logic formulae for specifying correctness requirements.
SYNTAX
Grammar: ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl Operands (opd): true, false, user-defined names starting with a lower-case letter, or embedded expressions inside curly braces, e.g.,: { a+b>n }. Unary Operators (unop): [] (the temporal operator always) <> (the temporal operator eventually) ! (the boolean operator for negation) Binary Operators (binop): U (the temporal operator strong until) W (the temporal operator weak until (only when used in inline formula) V (the dual of U): (p V q) means !(!p U !q)) && (the boolean operator for logical and) || (the boolean operator for logical or) /\ (alternative form of &&) \/ (alternative form of ||) -> (the boolean operator for logical implication) <-> (the boolean operator for logical equivalence)
DESCRIPTION
Starting with Spin version 6 there are two different formalisms for specifying
LTL formulae. The most convenient mechanism is to specify LTL formulae inline,
as part of a verification model. The older mechanism of using Spin to first
convert a formula into a never claim and to include that never claim into the
model is still supported as well.
We first describe the new mechanism.
INLINE SPECIFICATION
The easiest way to specify an LTL property is to specify it inline.
The formula is specified globally (i.e., outside all proctype
or init declarations) with the following syntax:
ltl [ name ] '{' formula '}'The name is optional, but can be useful when specifying multiple formulae. (Each such formula follows the same basic format.) The formula has the grammar outlined above, with some extensions. First, white space (newlines, spaces, tabs) can be used anywhere to separate operands and operators. Second, the names of operators can either be abbreviated with the symbols shown above, or spelled out in full (as always, eventually, until, implies, and equivalent. The alternative operators weakuntil, stronguntil, and release (for the V operator, see above), are also supported.
ltl p1 { []<> p } ltl p2 { always eventually p }The properties stated in this way are taken as positive properties that must be satisfied by the model. The model checker will perform an automatic negation of the formula to find counter-examples. (The negation is not automatic when you use the alternative, and older, method described below).
Another improvement in the specification of ltl formula in Spin version 6 and later is that the inline ltl formula can contain any propositional state formula, i.e., it is not restricted to the lower-case propositional symbols from before, where each propositional symbol has to be defined in macro definitions. This means that we can write:
ltl p3 { eventually (a > b) implies len(q) == 0 }There is just one restriction: you cannot use the predefined operators empty, nempty, full, nfull in inline ltl formula (and should not use them in the alternative method either, although it is not enforced there). The reason is technical: under the specific partial order reduction rules used in the model checker the four channel operators listed cannot be negated. In the conversion process from LTL formula into never claims (Buchi automata) negations will take place and can end up in the final automaton though, which would risk making partial order reductions invalid (logically unsound).
When multiple inline LTL formulae are specified, you get to choose which one will be applied during a verification run with a new runtime parameter -N for the pan verifiers. By default this will be the first LTL formula that appears in the specification. To disable all LTL formula during a verification you can compile pan.c with the directive -DNOCLAIM.
ALTERNATIVE METHOD
Spin can translate LTL formulae into Promela
never claims with command line option
-f . The
never claim that is generated encodes the Buchi acceptance conditions
from the LTL formula.
Formally, any omega-run that satisfies the LTL formula is
guaranteed to correspond to an accepting run of the
never claim.
The operands of an LTL formula are often one-character symbols, such as
p , q , r , but they can also be symbolic names,
provided that they start with a lowercase character, to avoid confusion
with some of the temporal operators which are in uppercase.
The names or symbols must be defined to represent boolean
expressions on global variables from the model.
The names or symbols are normally defined with
macro definitions.
Starting with Spin version 5.2.4 operands can also be defined
as embedded free-form expressions enclosed in curly braces,
for instance, something like: [] ( {a>b} -> {a>100} ).
This form avoids the need for the use of macros to define predicate symbols.
(The inline method described earlier also avoids the need
to use the curly braces.)
All binary operators are left-associative. Parentheses (round braces) can be used to override this default. Note that implication and equivalence are not temporal but logical operators.
EXAMPLES
Some examples of valid LTL formulae follow, as they would
be passed in command-line arguments to Spin for translation into
never claims.
Each formula passed to Spin has to be quoted.
We use single quotes in all examples given here, which will work
correctly on most systems (including Unix systems and Windows
systems with the
cygwin toolset).
On some systems double quotes can also be used.
spin -f '[] p' spin -f '!( <> !q )' spin -f 'p U q' spin -f 'p U ([] (q U r))'The conditions p , q , and r can be defined with macros, for instance as:
#define p (a > b) #define q (len(q) < 5) #define r ([email protected])elsewhere in the Promela model. It is prudent to always enclose these macro definitions in round braces to avoid misinterpretation of the precedence rules on any operators in the context where the names end up being used in the final never claim. The variables a and b , the channel name q , and the proctype name root from the preceding example, must be globally declared.
NOTES
If the Spin sources are compiled with the
preprocessor directive -DNXT,
the set of temporal operators is extended with
one additional unary operator:
X (next).
The
X operator asserts the truth of the subformula that follows it
for the next system state that is reached.
The use of this operator can void the validity of the
partial order reduction algorithm that is used in Spin, if
it changes the stutter invariance of an LTL formula.
For the partial order reduction strategy to be valid,
only LTL properties that are stutter invariant can be used.
Every LTL property that does not contain the
X operator is guaranteed to satisfy the required property.
A property that is not stutter invariant can still
be checked, but only without the application of
partial order reduction.
An alternative converter for LTL formulae, that can often produce smaller automata, is the tool ltl2ba, which can be downloaded from the Spin distribution website.
SEE ALSO
condition
macros
never
notrace
remoterefs
trace
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page updated: 6 September 2017) |