Promela |
Predefined |
nempty(5) |
NAME
nempty
-
predefined unary operator to test emptiness of a channel.
SYNTAX
nempty(
varref )
DESCRIPTION
The expression
nempty(q) ,
with
q
a channel name, is equivalent to
len(q) != 0 .
The Promela grammar prohibits this from being written as
!empty(q) .
Using nempty instead of its equivalents can preserve the validity of an addition partial order reduction during verifications, that can be defined with xr or xs declarations.
SEE ALSO
xr(2), xs(2), empty(5), full(5), len(5), nfull(5).
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |