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.
active [3] proctype A() { printf("this is process: %d\n", _pid); L: printf("it terminates after two steps\n") } never { do :: A[0]@L -> break od }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) |