for excluding data from the state descriptor during verification.
can be used to prefix the declaration of any variable,
to exclude the value of that variable from the definition
of the global system state.
The addition of this prefix can affect only the verification
process, by potentially changing the outcome of state matching
and cycle detection.
hidden byte a;
hidden short p;
The prefix should only be used for write-only scratch variables.
The keyword is likely to become obsolete in future versions of
Promela, being superseded by the predefined write-only variable
(i.e., typed as a single underscore).
It is safe to use
variables as pseudo local variables inside
sequences provided that the variables never occur
within the guards of an
construct, and provided that there is no
reference to the
variables from outside the
datatypes(2), show(2), _(5).