Promela Reference -- proctype(2)





Proctype declarations, for declaring process behavior.

proctype name ( [ decl_lst ] ) { sequence }

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.

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.

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.

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)