Promela |
Declarator |
provided(2) |
NAME
provided
-
for setting a global constraint on process execution.
SYNTAX
proctype
name ( [
decl_lst ] ) provided (
expr ) {
sequence }
DESCRIPTION
Any proctype declaration can be suffixed by an optional
provided
clause to constrain its execution to those global system states
for which the corresponding expression evaluates to
true .
The provided clause has the effect of labeling all statements
in the
proctype
declaration with an additional, user-defined, executability constraint.
EXAMPLES
The declaration:
byte a, b;
active proctype A() provided (a > b) { ... }
makes the execution of all instances of
proctype A
conditional on the truth of
a>b ,
which is, for instance, not true in the initial system state.
The expression can contain global references, or references
to the process's
_pid ,
but no references to any local variables or parameters.
NOTES
Provided
clauses are incompatible with partial order reduction.
They can be useful during random simulations, or in rare
cases for constraining exhaustive verification runs.
SEE ALSO
active(2), priority(2), proctype(2), _pid(5).
|
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |