Coloured Petri net
Coloured Petri nets (CPN) are a backward compatible extension of the concept of Petri nets.
CPN preserve useful properties of Petri nets and at the same time extend initial formalism to allow the distinction between tokens.[1]
Coloured Petri Nets allow tokens to have a data value attached to them. This attached data value is called token color. Although the color can be of arbitrarily complex type, places in CPNs usually contain tokens of one type. This type is called color set of the place.
Definition 1. A net is a tuple N = (P, T, A, Σ, C, N, E, G, I ) where:
- P is a set of places.
- T is a set of transitions.
- A is a set of arcs
In CPNs sets of places, transitions and arcs are pairwise disjoint P ∩ T=P ∩ A=T ∩ A=∅
- Σ is a set of color sets defined within CPN model. This set contains all possible colors, operations and functions used within CPN.
- C is a color function. It maps places in P into colors in Σ.
- N is a node function. It maps A into (P × T)∪(T × P).
- E is an arc expression function. It maps each arc a∈A into the expression e. The input and output types of the arc expressions must correspond to type of nodes the arc connected to.
Use of node function and arc expression function allows multiple arcs connect the same pair of nodes with different arc expressions.
- G is a guard function. It maps each transition t∈T into guard expression g. The output of the guard expression should evaluate to Boolean value true or false.
- I is an initialization function. It maps each place p into an initialization expression i. The initialization expression must evaluate to multiset of tokens with a color corresponding to the color of the place C(p).