Promela Reference -- _nr_pr(5)




_nr_pr - a predefined, global, read-only, integer variable.


The predefined, global, read-only variable _nr_pr records the number of processes that are currently running (i.e., active processes). It is an error to attempt to assign a value to this variable in any context.

The variable can be used to delay a parent process until all of the child processes that it created have terminated. The following example illustrates this type of use:

The use of the precondition on the creation of a new child process in the parent process guarantees that each child process will have process instantiation number one: one higher than the parent process. There can never be more than two processes running simultaneously in this system. Without the condition, a new child process could be created before the last one terminates and dies. This means that, in principle, an infinite number of processes could result. The verifier puts the limit on the number of processes that can effectively be created at 256, so in practice, if this was attempted, the 256th attempt to create a child process would fail, and the run statement from this example would then block.

Another way to use the predefined variable is to wait for a newly started process to terminate, for instance as follows:

In this case we first store the current value of the number of running processes in a variable n, then start a new process, which will increase the value of _nr_pr. Then we wait until the value drops back to the original value stored in n, indicating that the newly started process (and all processes started since we assigned n) terminated.


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page updated: 27 November 2010)