Promela Reference -- priority(2)





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

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

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.


run name(...) priority P

active proctype name() priority P { sequence }

where P a constant greater than or equal to one.

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.

provided(2), active(2), proctype(2).

Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page Updated: 16 December 1997)