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

SYNTAX
full( varref )

DESCRIPTION
Full is a predefined unary operator that takes the name of a channel as an operand and returns true if it currently contains its maximum number of messages, and it returns false otherwise. It is equivalent to the expression len(q) == QSZ , where q is the channel name, and QSZ is the message capacity of the channel.

EXAMPLES

chan q = [8] of { byte };

byte one_more = 0;



do

:: q!one_more; one_more++	/* fill the queue */

:: full(q) -> break		/* done */

od;

assert(len(q) == 8)

NOTES
Full can be used as a guard, by itself, or it can be used as a general boolean operator in expressions. It can, however, not be negated. There is a separate operator for this, that can be exploited by partial order reduction algorithms.

SEE ALSO
empty(5), len(5), nempty(5), nfull(5).