Promela |
Predefined |
empty(5) |
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).
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |