NAME
hidden - for excluding data from the state descriptor during verification.

SYNTAX
hidden typename ivar

DESCRIPTION
The keyword hidden 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.

EXAMPLES

hidden byte a;
hidden short p[3];

NOTES
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 hidden variables as pseudo local variables inside atomic sequences provided the variable name never occurs in a condition (a guard) from an if or do structure and provided there is no reference to the hidden variable from outside the atomic sequence.

SEE ALSO
datatypes(2), show(2), _(5).