linear-time temporal logic formulae, for specifying correctness requirements.
ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl
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) == !(!p U !q)
&& (the boolean operator for logical and)
|| (the boolean operator for logical or)
-> (the boolean operator for logical implication)
<-> (the boolean operator for logical equivalence)
Predefined: true, false
User-defined: names starting with a lowercase letter.
Promela itself does not include syntax for linear temporal logic (LTL) formulae.
Spin, however, can translate such formulae into Promela syntax, with
command line option -f. The translation is a
claim, encoding the Büchi acceptance condition. The formulae must
then express negative properties (errors): execution
sequences that satisfy the formula will be reported as correctness
violations in a verification.
The operands of an LTL formula are names
that represent symbolic propositions, i.e., boolean conditions
on the global system state.
The meaning of these conditions can be defined with
The temporal operators
Parentheses can be used to override this default where necessary.
Below are some examples of valid LTL formulae, as they would
be passed in command-line arguments to Spin for translation
spin -f " p"
spin -f "!( <> !q )"
spin -f "p U q"
spin -f "p U ( (q U r))"
can be defined with
#define p (a > b)
#define q (len(q) < 5)
elsewhere in the Promela program.
and channel name
must be globally declared to be visible to LTL formulae.
Remote references, as defined in
remoterefs(5), can be used indirectly, via
If the Spin source itself is compiled with the
preprocessor directive -DNXT,
the set of temporal operators is extended with
one additional unary operator:
operator asserts the truth of the sub-formula 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. To show that this is not the case requires a proof that the property that
is specified is closed under stuttering. Spin does not perform such checks
automatically (they are not needed for LTL formulae without X operators),
but it does issue a warning when the check may be needed.
macros(1), never(2), trace(2), notrace(2), condition(4), remoterefs(5).