nfull - predefined, boolean function to test fullness of a channel.
nfull( varref )
The expression nfull(q) is equivalent to the expression
(len(q) < QSZ)where q is a channel name, and QSZ the capacity of this channel. The Promela grammar prohibits the same from being written as !full(q) .
Using nfull instead of its equivalents can preserve the validity of reductions that are applied during verifications, especially in combination with the use of xr and xs channel assertions.
Note that if predefined functions such as empty , nempty , full , and nfull are used in macro definitions used for propositional symbols in LTL formulae, they may well unintentionally appear under a negation sign, which will trigger syntax errors from Spin.
Spin Online References
Promela Manual Index
|(Page updated: 28 November 2004)|