Promela Reference -- _last(5)




_last - a predefined, global, read-only variable of type pid .


_last is a predefined, global, read-only variable of type pid 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 _last variable can only be used inside never claims. It is an error to assign a value to this variable in any context.

The following sample never claim attempts to match an infinite run in which the process with process initialization number one executes every other step, once it starts executing.

Because the initial value of variable _last is zero, the first guard in the first do loop is always true in the initial state. This first loop is designed to allow the claim automaton to execute dummy steps (passing through its else clause) until the process with instantiation number one executes its first step, and the value of _last becomes one. Immediately after this happens, the claim automaton moves from into its second state, which is accepting. The remainder of the run can only be accepted, and reported through Spin's acceptance cycle detection method, if the process with instantiation number one continues to execute every other step. The system as a whole may very well allow other executions, of course. The never claim is designed, though, to intercept just those runs that match the property of interest.

During verifications, this variable is not part of the state descriptor unless it is referred to at least once. The additional state information that is recorded in this variable will generally cause an increase of the number of reachable states. The most serious side effect of the use of the variable _last in a model is, though, that it prevents the use of both partial order reduction and of the breadth-first search option.


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page updated: 28 November 2004)