|
NAME
DESCRIPTION
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
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
|