Promela |
Predefined |
len |
NAME
len -
predefined, integer function to determine the number of messages
that is stored in a buffered channel.
SYNTAX
len( varref )
DESCRIPTION
A predefined function that takes the name of a channel
as an argument and returns the number of messages
that it currently holds.
EXAMPLES
#define QSZ 4 chan q = [QSZ] of { mtype, short }; len(q) > 0 /* same as nempty(q) */ len(q) == 0 /* same as empty(q) */ len(q) == QSZ /* same as full(q) */ len(q) < QSZ /* same as nfull(q) */
NOTES
When possible, it is always better to use the predefined,
boolean functions
empty , nempty , full , and
nfull , since these define special cases that can be exploited
in Spin's partial order reduction algorithm during verification.
If len is used stand-alone as a condition statement, it will block execution until the channel is non-empty.
SEE ALSO
chan
condition
empty
full
nempty
nfull
xr
xs
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page updated: 28 November 2004) |