hidden - for excluding global data from the state descriptor during verification.
hidden typename ivar
The keyword hidden can be used to prefix the declaration of any global 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 operations.
hidden byte a; hidden short p;
The prefix should only be used for write-only scratch variables. Alternatively, the predefined write-only scratch variable _ (underscore) can always be used instead of a hidden integer variable.
This mechanism can be used, for instance, to hide variables that are used as pseudo-local variables inside d_step sequences, provided that they are not used anywhere outside that sequence.
Spin Online References
Promela Manual Index
|(Page updated: 15 March 2011)|