Promela Reference -- priority(2)

Promela

Declarator

priority


NAME
priority - for setting a numeric simulation priority for a process.

SYNTAX
active [ '[' const ']' ] proctype name ( [ decl_lst ] ) priority const { sequence }
run name ( [ arg_lst ] ) priority const

DESCRIPTION
Process priorities can be used in random simulations to change the probability that specific processes are scheduled for execution.

An execution priority is specified either as an optional parameter to a run operator, or as a suffix to 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 is always assigned the priority that is explicitly or implicitly specified there (overriding the priority that may be specified in the proctype declaration for that process).

EXAMPLES

If both a priority clause and a provided clause are specified, the priority clause should appear first.

NOTES
Priority annotations only affect random simulation runs. They have no effect during verification, or in guided and interactive simulation runs. A priority designation on a proctype declaration that contains no active prefix is ignored.

SEE ALSO
active
proctype
provided


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page updated: 28 November 2004)