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 (that is, the keyword cannot be used as an argument to the run operator).

Active processes can be differentiated from each other by the value of their process instantiation number, which is available in the predefined local variable _pid . Active processes are always instantiated in the order in which they appear in the model, so that the first such process (whether it is declared as an active process or as an init process) will receive the lowest instantiation number, which is zero.

The smallest possible Promela model is:

where skip is Promela's null statement, or perhaps more usefully The init process is most commonly used to initialize global variables, and to instantiate other processes, through the use of the run operator, before system execution starts. Any process, not just the init process, can do so, though.

It is convention to instantiate groups of processes within atomic sequences, to make sure that their execution begins at the same instant. For instance, in the leader election example, included as a test case in the Spin distribution, the initial process is used to start up N copies of the proctype node . Each new instance of the proctype is given different parameters, which in this case consist of two channel names and an indentifying number. The node proctype is then of the form:

and the init process is structured as follows. After the 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. That is, Promela processes can only die in reverse order of creation (in stack order). This means that if an init process is used to create all other processes in the system, the init process itself 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:

Because no parameter values can be passed to an active process declaration, the parameters are now replaced with local variables.

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


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