Promela |
Declarator |
active |
NAME
active -
prefix for
proctype declarations to instantiate an initial set of processes.
SYNTAX
active proctype name ( [ decl_lst ] ) { sequence }
active '[' const ']' proctype name ( [ decl_lst ] ) { sequence }
DESCRIPTION
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.
EXAMPLES
active proctype A(int a) { \&... }
active [4] proctype B() { run A(_pid) }
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.
NOTES
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.
SEE ALSO
_pid
init
proctype
remoterefs
run
|
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page updated: 20 November 2014) |