Promela Reference -- run(5)




run - predefined, unary operator for creating new processes.

run name ( [ arg_lst ] )

The run operator takes as arguments the name of a previously declared proctype , and a possibly empty list of actual parameters that must match the number and types of the formal parameters of that proctype . The operator returns zero if the maximum number of processes is already running, otherwise it returns the process instantiation number of a new process that is created. The new process executes asynchronously with the existing active processes from this point on. When the run operator completes, the new process need not have executed any statements.

The run operator must pass actual parameter values to the new process, if the proctype declaration specified a non-empty formal parameter list. Only message channels and instances of the basic data types can be passed as parameters. Arrays of variables cannot be passed.

Run can be used in any process to spawn new processes, not just in the initial process. An active process need not disappear from the system immediately when it terminates (i.e., reaches the end of the body of its process type declaration). It can only truly disappear if all younger processes have terminated first. That is, processes can only disappear from the system in reverse order of their creation.


Because Promela defines finite state systems, the number of processes and message channels is required to be bounded. Spin limits the number of active processes to 255.

Because run is an operator, run A() is an expression that can be embedded in other expressions. It is the only operator allowed inside expressions that can have a side effect, and therefore there are some special restrictions that are imposed on expressions that contain run operators.

Note, for instance, that if the condition statement

were allowed, in the evaluation of this expression it would be possible that the first application of the run operator succeeds, and the second fails when the maximum number of runnable processes is reached. This would produce the value false for the expression, and the condition statement would then block, yet a side effect of the evaluation has occurred. Each time the evaluation of the expression is repeated, one more process could then be created.

Therefore, the Spin parser imposes the restriction that an expression cannot contain more than one run operator, and this operator cannot be combined in a compound expression with other conditionals. Also, as a further precaution, an attempt to create a 256th process is always flagged as an error by the verifier, although technically it would suffice to allow the run operator to return a zero value.


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page updated: 28 November 2004)