Promela Reference -- proctype(2)

Promela

Declarator

proctype


NAME
proctype - for declaring new process behavior.

SYNTAX
proctype name ( [ decl_lst ] ) { sequence }

D_proctype name ( [ decl_lst ] ) { sequence }

DESCRIPTION
All 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 keyword D_proctype can be used to declare process behavior that is to be executed completely deterministically . If non-determinism is nonetheless present in this type of process definition, it is resolved in simulations in a deterministic, though otherwise undefined, manner. During verifications an error is reported if non-determinism is encountered in a D_proctype process.

EXAMPLES
The following program declares a proctype with one local variable named state :

The process type is named A , and has one formal parameter named x .

NOTES
Within a proctype body, formal parameters are indistinguishable from local variables. Their only distinguishing feature is that their initial values can be determined by an instantiating process, at the moment when a new copy of the process is created.

The current spin implementation forbids the use of arrays as formal parameters (both when used explicitly and when the array is hidden in a typedef'ed structure.

SEE ALSO
_pid
active
init
priority
provided
remoterefs
run
typedef


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page updated: 4 September 2021)