NAME
nfull - predefined unary operator to test fullness of a channel.

SYNTAX
nfull( varref )

DESCRIPTION
The expression nfull(q) is equivalent to len(q) < QSZ , where q is a channel name, and QSZ the capacity of this channel. The Promela grammar prohibits the same from being written as !full(q) .

Using nfull 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), nempty(5).