Promela Reference -- empty(5)

Promela

Predefined

empty


NAME
empty - predefined, boolean function to test emptiness of a buffered channel.

SYNTAX
empty( name )

DESCRIPTION
Empty is a predefined function that takes the name of a channel as an argument and returns true if the number of messages that it currently holds is zero; otherwise it returns false. The expression

where q is a channel name, is equivalent to the expression

EXAMPLES

This example shows how the contents of a message channel can be flushed in one indivisible step, without knowing, or storing, the detailed contents of the channel. Note that execution of this code is deterministic. The reason for the skip statement at the end is explained in the manual page for d_step .

NOTES
A call on empty can be used as a guard, or it can be used in combination with other conditionals in a boolean expression. The expression in which it appears, though, may not be negated. (The Spin parser will intercept this.) Another predefined function, nempty , can be used when the negated version is needed. The reason for the use of empty and nempty is to assist Spin's partial order reduction strategy during verification.

If predefined functions such as empty and nempty are used in the symbol definitions of an LTL formula, they may unintentionally appear under a negation sign in the generated automaton, which can then trigger a surprising syntax error from Spin. The easiest way to remedy such a problem, if it occurs, is to revise the generated never claim automaton directly, and replace every occurrence of !empty() with nempty() and every occurrence of !nempty() with empty() .

SEE ALSO
_
condition
full
ltl
len
nempty
nfull


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page updated: 28 November 2004)