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) |