Promela Reference -- len(5)

Google

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)