Promela |
Declarator |
provided |
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 the expression (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.
If both a priority clause and a provided clause are specified, the priority clause should come first.
active proctype name() priority 2 provided (a > b ) { ... }
NOTES
Provided clauses are incompatible with partial order reduction
and they are incompatible with the fairness algorithm (runtime option -f).
They can be useful during random simulations, or in rare
cases to control and reduce the complexity of verifications.
SEE ALSO
_pid
active
hidden
priority
proctype
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page updated: 8 November 2008) |