Promela |
Declarator |
active(2) |
NAME
active
-
prefix for
proctype
declarations, to instantiate initial processes.
SYNTAX
active proctype
name ( [
decl_lst ] ) {
sequence }
active '['
const ']'
proctype
name ( [
decl_lst ] ) {
sequence }
DESCRIPTION
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.
EXAMPLES
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.
NOTES
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.
SEE ALSO
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) |