Promela Reference -- active(2)




active - prefix for proctype declarations to instantiate an initial set of processes.

active proctype name ( [ decl_lst ] ) { sequence }
active '[' const ']' proctype name ( [ decl_lst ] ) { sequence }

The keyword active can be prefixed to any proctype declaration to define a set of processes that are required to be active (i.e., running) in the initial system state. At least one active process must always exist in the initial system state. Such a process can also be declared with the help of the keyword init .

Multiple instantiations of the same proctype can be specified with an optional array suffix of the active prefix. The instantiation of a proctype requires the allocation of a process state and the instantiation of all associated local variables. At the time of instantiation, a unique process instantiation number is assigned. The maximum number of simultaneously running processes is 255. Specifying a constant greater than 255 in the suffix of an active keyword would result in a warning from the Spin parser, and the creation of only the first 255 processes.

Processes that are instantiated through an active prefix cannot be passed arguments. It is, nonetheless, legal to declare a list of formal parameters for such processes to allow for argument passing in additional instantiations with a run operator. In this case, copies of the processes instantiated through the active prefix have all formal parameters initialized to zero. Each active process is guaranteed to have a unique _pid within the system.


One instance of proctype A is created in the initial system state with a parameter value for a of zero. In this case, the variable a is indistinguishable from a locally declared variable. Four instances of proctype B are also created. Each of these four instances will create one additional copy of proctype A , and each of these has a parameter value equal to the process instantiation number of the executing process of type B . If the process of type A is assigned _pid zero, then the four process of type B will be assigned _pid numbers one to four. All five processes that are declared through the use of the two active prefixes are guaranteed to be created and instantiated before any of these processes starts executing.

In many Promela models, the init process is used exclusively to initialize other processes with the run operator. By using active prefixes instead, the init process becomes superfluous and can be omitted, which reduces the amount of memory needed to store global states.

If the total number of active processes specified with active prefixes is larger than 255, only the first 255 processes (in the order of declaration) will be created.


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page updated: 20 November 2014)