local - prefix on global variable declarations to assert exclusive use by a single process.
local typename ivar
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.
local byte a; local short p;
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.
Spin Online References
Promela Manual Index
|(Page updated: 28 November 2004)|