Promela Reference -- _pid(5)

Promela

Predefined

_pid


NAME
_pid - a predefined, local, read-only variable of type pid that stores the instantiation number of the executing process.

SYNTAX
_pid

DESCRIPTION
Process instantiation numbers begin at zero for the first process created and count up for every new process added. The first process, with instantiation number zero, is always created by the system. Processes are created in order of declaration in the model. In the initial system state only process are created for active proctype declarations, and for an init declaration, if present. There must be at least one active proctype or init declaration in the model.

When a process terminates, it can only die and make its _pid number available for the creation of another process, if and when it has the highest _pid number in the system. This means that processes can only die in the reverse order of their creation (in stack order).

The value of the process instantiation number for a process that is created with the run operator is returned by that operator.

Instantiation numbers can be referred to locally by the executing process, through the predefined local _pid variable, and globally in never claims through remote references.

It is an error to attempt to assign a new value to this variable.

EXAMPLES
The following example shows a way to discover the _pid number of a process, and gives a possible use for a process instantiation number in a remote reference inside a never claim.

The remote reference in the claim automaton checks whether the process with instantiation number zero has reached the statement that was marked with the label L . As soon as it does, the claim automaton reaches its end state by executing the break statement, and reports a match. The three processes that are instantiated in the active proctype declaration can execute in any order, so it is quite possible for the processes with instantiation numbers one and two to terminate before the first process reaches label L .

NOTES
A never claim, if present, is internally also represented by the verifier as a running process. This claim process has no visible instantiation number, and therefore cannot be referred to from within the model. From the user's point of view, the process instantiation numbers are independent of the use of a never claim.

SEE ALSO
_
_last
_nr_pr
active
init
never
proctype
remoterefs
run


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