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 :
proctype A(mtype x) { mtype state; state = x }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) |