Promela |
Predefined |
_ |
NAME
_ -
a predefined, global, write-only, integer variable.
SYNTAX
_
DESCRIPTION
The underscore symbol
_ refers to a global, predefined, write-only, integer variable
that can be used to store scratch values.
It is an error to attempt to use or reference the value
of this variable in any context.
EXAMPLES
The following example uses a
do -loop to flush the contents of a channel with two message fields
of arbitrary type, while ignoring the values of the retrieved
messages:
do :: q?_,_ :: empty(q) -> break od
SEE ALSO
_nr_pr
_last
_pid
np_
hidden
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page updated: 28 November 2004) |