Coloured Petri Nets
Defined by:
- set of types for describing token state - colour set;
- sets of places, transitions and arcs;
- node function, maps arc to place/transition pair;
- colour function, maps place to colour set (of token if resident there);
- guard function, maps transition to boolean expression;
- arc expression function, maps arc to expression at place yielding a multiset;
- an initialization.