Promela |
Predefined |
nfull(5) |
NAME
nfull
-
predefined unary operator to test fullness of a channel.
SYNTAX
nfull(
varref )
DESCRIPTION
The expression
nfull(q)
is equivalent to
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 an addition partial order reduction during verifications, that can be defined with xr or xs declarations.
SEE ALSO
xr(2), xs(2), empty(5), full(5), len(5), nempty(5).
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |