- UPPAAL Help
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.
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.
chan a,b,c,d,e; chan priority a,d < default < b,e;
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.
system A < B,C < D;
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.
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.