Promela Reference -- provided(2)

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:

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.

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)