Coloured Petri net

Coloured Petri nets are a backward compatible extension of the mathematical concept of Petri nets.
Coloured Petri nets preserve useful properties of Petri nets and at the same time extend the initial formalism to allow the distinction between tokens.
Coloured Petri nets allow tokens to have a data value attached to them. This attached data value is called the token color. Although the color can be of arbitrarily complex type, places in coloured Petri nets usually contain tokens of one type. This type is called the color set of the place.
Definition 1. A "net" is a tuple "N" = ("P", "T", "A", Σ, "C", "N", "E", "G", "I" ) where:
In coloured Petri nets, sets of places, transitions and arcs are pairwise disjoint "P" ∩ "T" = "P" ∩ "A" = "T" ∩ "A" = ∅
Use of node function and arc expression function allows multiple arcs connect the same pair of nodes with different arc expressions.
A well-known program for working with coloured Petri nets is cpntools.