Promela Reference -- priority(2)

Google

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)