Promela |
Declarator |
local |
NAME
local -
prefix on global variable declarations to assert exclusive use by a single process.
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
local byte a; local short p[3];
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) |