Skip to main content.

Priorities

Given some priority order on the transitions, the intuition is that, at a given time-point, a transition is enabled only if no higher priority transition is enabled (see also Semantics.) We say that the higher priority transition blocks the lower priority transition.

Priorities can be assigned to the channels and processes of a system. The priority orders defined in the system are translated into a priority order on tau-transitions and synchronizing transitions. Delay transitions are still non-deterministic (unless urgent channels are used.)

Priorities on Channels

ChanPriority ::= 'chan' 'priority' (ChanExpr | 'default') ((',' | '<') (ChanExpr | 'default'))* ';'
ChanExpr ::= ID
           | ChanExpr '[' Expression ']'

A channel priority declaration can be inserted anywhere in the global declarations section of a system (only one per system). The priority declaration consist of a list of channels, where the '<' separator defines a higher priority level for channels listed on its right side. The default priority level is used for all channels that are not mentioned, including tau transitions.

Note: the channels listed in the priority declaration must be declared earlier.

Example

chan a,b,c,d[2],e[2];
chan priority a,d[0] < default < b,e;

The example assigns the lowest priority to channels a and d[0], and the highest priority to channels b, e[0] and e[1]. The default priority level is assigned to channels c and d[1].

Priorities on Processes

Process priorities are specified on the system line, using the separator '<' to define a higher priority for processes to its right. If an instance of a template set is listed, all processes in the set will have the same priority.

Example

system A < B,C < D;

Resolving Synchronization

In a synchronisation the process priorities are ambigous, because more than one process is involved in such a transition.

When two processes A and B synchronize the priority of the transition is the pair (B,A), where B is the higher priority process. When there are two potential transitions with priorities (B,A) and (D,C), the priorities of B and D are compared. If B > D then (B,A) blocks (D,C), and if D > B then (D,C) blocks (B,A). When B=D we compare the priorities of A and C and resolve the priority of the transitions accordingly.

For a broadcast synchronization the priority is represented as an ordered tuple of descending process priorities, in a similar manner to the pairs used for binary synchronisations.

Priorities on both Channels and Processes

In a system with priorities on both processes and channels, priorities are resolved by comparing priorities on channels first. If they are the same, the process priorities are compared.