Promela Reference -- active(2)





active - prefix for proctype declarations, to instantiate initial processes.

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

In early versions of Spin there was only one predefined initial process, init(2). In newer versions, the keyword active can be prefixed to any proctype(2) declaration to define additional processes that are active in the initial global system state. The use of an init declaration has thereby become optional, the only requirement being that at least one active process exists in the initial state of the system. Multiple instantiations of the same proctype can be specified with an optional array suffix of active (separated from it by white space). The instantiation of a proctype implies the allocation of the data structure for an active process (cf. definition S.4 in intro(0)), the initialization of its parameters and local variables, and the assignment to that process of a unique pid number. The maximum number of active processes is necessarily bounded during verification. In Spin verifications, process instantiation only succeeds in global system states (cf. definition S.6) with fewer than 255 active processes. During simulations, however, no bound is enforced.


active proctype A() { \&... }

active [4] proctype B() { \&... }

In the first example one instance of proctype A is created in the initial system state; in the second example four instances of proctype B are created.

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.

In many Spin models, the init process is used exclusively to initiate 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.

For the purposes of verification there can be no more than 255 active processes at any one time. This means that if the total number of active processes specified with active prefixes is greater than 255, only the first (arbitrarily chosen) 255 processes will be created. After system initialization, the predefined run operator will return zero (instead of a non-zero process pid number) if the bound on the maximum number of active processes would be exceeded, thus blocking its execution when it is used as a conditional statement. No bound is enforced during simulations.

init(2), proctype(2), condition(4), remoterefs(5), _pid(5), run(5).

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