Promela Reference -- init(2)





init - for declaring an initial process.

init { sequence }

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.

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;


		:: proc <= N ->

			run node (q[proc-1], q[proc%N], (N+I-proc)%N+1);


		:: proc > N ->





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;



The init keyword has become largely redundant with the addition of the active prefix for proctype declarations.

active(2), proctype(2), _pid(5), run(5).

Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page Updated: 16 December 1997)