Prioritised Petri net

A Prioritised Petri net is a structure (PN, Π) where PN is a Petri net and Π is a priority function that maps transitions into non-negative natural numbers representing their priority level 
The enabled transitions with a given priority k always fire before any other enabled transition with priority j<k.