NAME
_last
-
predefined global read-only variable.
SYNTAX
_last
DESCRIPTION
_last
is a predefined global variable that holds the
instantiation number of the process that performed the last
step in the current execution sequence.
The initial value of
_last
is zero.
The variable can only be referenced inside
never
claim declarations. It is an error to assign any
value to it directly.
EXAMPLES
never {
/* it is/is not possible for the process with _pid 1
* to execute every other step forever
*/
accept: do
:: _last != 1 -> _last == 1
od
}
NOTES
During verifications this variable is not part of the state
descriptor unless it is referred to at least once in the
verification model.
The additional state information present in this variable
can cause an increase of the number of reachable states.
SEE ALSO
_pid(5) _(5)
|