Promela |
Predefined |
_pid(5) |
NAME
_pid
-
predefined read-only local variable that stores the process
instantiation number.
DESCRIPTION
Process instantiation numbers begin at zero for the
first process created, and count up for every new process added.
The first process is always created by the system, and is either the
init
process, or one of the processes declared to be
active
in a
proctype
declaration.
At any point in time, only the process with the highest instantiation number can die (i.e., the most recently created child). Processes instantiation numbers can, but need not be be recycled. The process instantiation numbers for processes created with a run operator is returned by that operator, if successful.
Instantiation numbers can be referred to in remote references inside never claims, or ltl formulae. A never claim itself, also has an instantiation number (a negative value) that cannot be referred to by the user.
EXAMPLES
The following example shows a way to discover the
_pid
of a process, and a possible use for a process
instantiation number in a remote reference inside a
never
claim.
active [3] proctype A() { printf("hi, i am process number: %d\n", _pid); L: printf("and i'm already done\n") } never { do :: A[0]@L -> break od }
SEE ALSO
ltl(1), never(2), _last(5), remoterefs(5), run(5).
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |