NAME
empty - predefined unary operator to test emptiness of a channel.

SYNTAX
empty( name )

DESCRIPTION
Empty is a predefined unary operator that takes the name of a channel as an operand and returns true if the number of messages that it currently holds is zero, and it returns false otherwise. It is equivalent to the expression len(q) == 0 , where q is the channel name.

EXAMPLES

chan q = [8] of { mtype };



do

:: q?_			/* flush messages */

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

od

NOTES
Empty 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
full(5), len(5), nempty(5), nfull(5).