predefined unary operator to test fullness of a channel.
is equivalent to
len(q) < QSZ ,
is a channel name, and
the capacity of this channel.
The Promela grammar prohibits the same from being written as
instead of its equivalents can preserve the validity
of an addition partial order reduction during verifications,
that can be defined with
xr(2), xs(2), empty(5), full(5), len(5), nempty(5).