Promela |
Predefined |
nfull |
NAME
nfull -
predefined, boolean function to test fullness of a channel.
SYNTAX
nfull( varref )
DESCRIPTION
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.
NOTES
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.
SEE ALSO
condition
empty
full
len
ltl
nempty
xr
xs
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page updated: 28 November 2004) |