Promela Reference -- _pid(5)

Google

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)