Promela Reference -- _(5)

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:

SEE ALSO
_nr_pr
_last
_pid
np_
hidden


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