Promela |
Predefined |
run(5) |
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())The reason that this is unwise is that in the case where only one more processes can be created, the evaluation of the expression as a whole will fail, and each time it is repeated it may spawn one more process, giving rise to unpredictable behavior.
SEE ALSO
active(2), priority(2), proctype(2), provided(2), _pid(5), remoterefs(5).
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |