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, and user-defined names starting with a lower-case letter 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) 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
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.
All binary operators are left-associative. Parentheses 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 (root@Label)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: 28 November 2004) |