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).