Promela Reference -- local(2)

Google

Promela

Declarator

local(2)

NAME
local - for marking a global variable as being used by only one process.

SYNTAX
local typename ivar

DESCRIPTION
The keyword local can be used to prefix the declaration of any global variable. It persuades the partial order reduction algorithm in the model checker to treat the variable as if it were declared local to a single process. The addition of this prefix can affect only the verification process.

EXAMPLES

local byte a;

local short p[3];

NOTES
If in effect the variable marked as local is accessed by more than one process, the result of a verification may be rendered incomplete. As yet there is no run-time check to detect such cases. In a future revision the check is likely to be added though.

SEE ALSO
datatypes(2), hidden(2), show(2), _(5).


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page Updated: 16 December 1997)