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