Promela Reference -- len(5)

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

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)