NAME
run - predefined unary operator, used to create new processes.

SYNTAX
run name ( [ arg_lst ] )

DESCRIPTION
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, discussed later, and instances of the five basic data types can be passed as parameters. Arrays and process types 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 first all younger processes have terminated first. That is: processes can only disappear from the system in stack-order.

EXAMPLES

proctype A(byte state; short set)

{	(state == 1) -> state = set

}

init { run A(1, 3) }

NOTES
Because Promela defines finite state systems, the number of processes and message channels is required to be bounded. The precise value of the bound is implementation-dependent. In Spin verifications there can be no more than 255 active processes.

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. It would be valid, though not very wise, to use run operators to build a condition statement such as

(run A() && run B())

SEE ALSO
active(2), priority(2), proctype(2), provided(2), _pid(5), remoterefs(5).