Promela Reference -- local(2)

Promela

Declarator

local


NAME
local - prefix on global variable declarations to assert exclusive use by a single 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, yet by being declared global it can freely be used in LTL formulae and in never claims.

The addition of this prefix can increase the effect of partial order reduction during verification, and lower verification complexity.

EXAMPLES

NOTES
If a variable marked as local is in fact accessed by more than one process, the partial order reduction may become invalid and the result of a verification incomplete. Such violations are not detected by the verifier.

SEE ALSO
_
datatypes
hidden
ltl
never
show


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page updated: 28 November 2004)