Promela Reference -- full(5)

Promela

Predefined

full


NAME
full - predefined, boolean function to test fullness of a channel.

SYNTAX
full( varref )

DESCRIPTION
Full is a predefined function that takes the name of a channel as an argument and returns true if that channel currently contains its maximum number of messages, and otherwise it returns false. It is equivalent to the expression

where q is the channel name, and QSZ is the message capacity of the channel.

This function can only be applied to buffered channels. The value returned for rendezvous channels would always be false, since a rendezvous channel cannot store messages.

EXAMPLES

NOTES
Full can be used as a guard, by itself, or it can be used as a general boolean function in expressions. It can, however, not be negated (for an explanation see also the manual page for empty ).

If predefined functions such as full , or nfull are used in the symbol definitions of an LTL formula, they may unintentionally appear under a negation sign in the generated automaton, which can then trigger a surprising syntax error from Spin.

SEE ALSO
condition
empty
len
ltl
nempty
nfull


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page updated: 28 November 2004)