Promela Reference -- _pid(5)





_pid - predefined read-only local variable that stores the process instantiation number.

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.

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 {


	:: A[0]@L -> break



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)