Promela |
Predefined |
len(5) |
NAME
len
-
predefined operator to determine the number of messages
stored in a channel.
SYNTAX
len(
varref )
DESCRIPTION
A predefined unary operator that takes the name of a channel
as an operand and returns the number of messages
that it currently holds.
EXAMPLES
chan q = [4] of { mtype, short }; len(q) > 0 /* same as nempty(q) */ len(q) == 0 /* same as empty(q) */ len(q) == 4 /* same as full(q) */ len(q) < 4 /* same as nfull(q) */
NOTES
If
len
is used as a condition statement, rather than on
the right side of an assignment, it is unexecutable if
the channel is empty.
SEE ALSO
empty(5), full(5), nempty(5), nfull(5).
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |