Promela Reference -- nempty(5)

Promela

Predefined

nempty


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

SYNTAX
nempty( varref )

DESCRIPTION
The expression nempty(q) , with q a channel name, is equivalent to the expression

where q is a channel name. The Promela grammar prohibits this from being written as !empty(q) .

Using nempty instead of its equivalents can preserve the validity of reductions that are applied during verifications, especially in combination with the use of xr and xs channel assertions.

NOTES
Note that if predefined functions such as empty , nempty , full , and nfull are used in macro definitions used for propositional symbols in LTL formulae, they may well unintentionally appear under a negation sign, which will trigger syntax errors from Spin.

SEE ALSO
condition
empty
full
len
ltl
nfull
xr
xs


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