Promela |
Declarator |
priority(2) |
NAME
priority
-
for setting a numeric simulation priority for a process.
SYNTAX
active
[ '[' N ']' ]
proctype
name priority
const ( [
decl_lst ] ) {
sequence }
run
name ( [
arg_lst ] )
priority const
DESCRIPTION
Process priorities are used in random
simulations to make higher priority processes
more likely to execute than lower priority processes.
An execution priority is specified either at the run statement, or in combination with an active proctype declaration. The optional priority field follows the closing brace of the parameter list in a proctype declaration.
The default execution priority for a process is one. Higher numbers indicate higher priorities, in such a way that a priority ten process is ten times more likely to execute than a priority one process.
The priority specified in an active proctype declaration affects all processes that are initiated through the active prefix, but no others. A process instantiated with a run statement always is assigned the priority that is explicitly or implicitly specified there (overriding the priority that may be specified in the proctype declaration for that process). In the absence of a priority clause, the execution priority is one.
EXAMPLES
run name(...) priority P active proctype name() priority P { sequence }where P a constant greater than or equal to one.
NOTES
Priority annotations have no effect during verification,
and no effect in guided, or interactive simulations.
It is syntactically valid, but meaningless, to specify
a priority in a
proctype
declaration that contains no
active
prefix.
SEE ALSO
provided(2), active(2), proctype(2).
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |