Promela |
Declarator |
proctype(2) |
NAME
Proctype declarations, for declaring process behavior.
SYNTAX
proctype
name ( [
decl_lst ] ) {
sequence }
DESCRIPTION
Process behavior must be declared before it can be instantiated.
The
proctype
construct is used for the declaration.
Instantiation can be done either with the
run
operator, or with the prefix
active
that can be used at the time of declaration.
Declarations for local variables and message channels may be placed anywhere inside the proctype body. In all cases, though, these declarations are treated as if they were all placed at the start of the proctype declaration. The scope of local variables cannot be restricted to only part of the proctype body.
EXAMPLES
The following program declares a
proctype
with one local variable named
state .
proctype A(mtype x) { byte state; state = x }
The process type is named
A ,
and has one formal parameter named
x .
The body, enclosed in parentheses,
contains one additional local variable declaration
and a single assignment statement, assigning the value of
the formal parameter to the local variable.
NOTES
Within a
proctype
body, formal parameters are indistinguishable from local
variables. Their only distinguishing feature is that their
initial values need not be determined until process instantiation.
An experimental variant of the standard process declaration can be obtained by replacing the keyword proctype with D_proctype (short for deterministic proctype ). Any process instantiated from a D_proctype is declared to be a deterministic process. The verifier can detect if non-determinism is nonetheless possible, and will generate a run-time error if this is the case.
SEE ALSO
active(2), init(2), priority(2), provided(2), _pid(5), remoterefs(5), run(5).
|
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |