Promela |
Declarator |
init(2) |
NAME
init
-
for declaring an initial process.
SYNTAX
init {
sequence }
DESCRIPTION
The
init
keyword is used to declare the behavior of a
process that is active in the initial system state.
An init process has no parameters, and no additional copies of the process can be created. If present, the init process is guaranteed to have the lowest process instantiation number, available in the local predefined variable _pid , also in the presence of other active proctype declarations.
Active processes can be differentiated from each other by the value of predefined local variable _pid . The value of _pid is incremented by one for each newly created process. The _pid numbers of no longer existing processes can be recycled. The most recently created process always has the highest _pid in the system, and the oldest process has the lowest number.
EXAMPLES
The smallest possible Promela specification is:
init { skip }
with
skip
the null statement (a predefined condition statement, see
skip(1)). Any process can be used to initialize global variables,
and to instantiate other processes, through the use of
the
run
operator.
It is convention to instantiate processes within an
atomic
sequence, to avoid cases where some processes already
start executing before others have been created.
For instance, in the
leader
election example, included as a test case in the
Spin distribution, the initial process is defined
follows.
init {
byte proc;
atomic {
proc = 1;
do
:: proc <= N ->
run node (q[proc-1], q[proc%N], (N+I-proc)%N+1);
proc++
:: proc > N ->
break
od
}
}
In this code, a total of N instantiations of
proctype
node ,
declared elsewhere,
are created, each with different parameters.
After this instantiation, the initial process terminates.
A process in Promela, however, cannot die, and be removed from the system, until all its children have died first. This means that an init process will continue to exist, and take up memory, as long as the system exists. Systems in which all processes can be instantiated with active prefixes, instead of through the intermediacy of an init process, can therefore often be verified more efficiently. The following code fragment illustrates an alternative initialization for the leader election protocol, avoiding the use of an init process.
active [N] proctype node ()
{ chan in = q[_pid];
chan out = q[(_pid+1)%N];
byte mynumber = (N+I-(_pid+1))%N+1;
&...
}
NOTES
The
init
keyword has become largely redundant with
the addition of the
active
prefix for
proctype
declarations.
SEE ALSO
active(2), proctype(2), _pid(5), run(5).
|
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |