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)