Dining philosophers example
This is a small toy example which is well-suited as an introduction to state spaces (also called occurrence graphs). The analysis of the state space is described in great detail and a large number of different queries are illustrated.
The CPN model describes how a number of processes (philosophers) share common resources (chopsticks). The Dining Philosophers is one of the traditional examples used by computer scientists to illustrate new concepts in the area of synchronisation and concurrency.
The example is taken from Sect. 1.6 of Vol. 2 of
K. Jensen. Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use, Monographs on Theoretical Computer Science, vol. 2:Analysis Methods.
Springer-Verlag, Berlin (1997).
Most of the detailed explanation is taken from the state space tool manual, which uses the Dining philosophers as its main example.
Documentation on the state space tool can be found here here.
The files for this net can be found in a subdir of cpntools called Samples\\DiningPhilosophers
The files are
- diningphilosophers.zip (The net file to load in CPN Tools)
- diningphilosophers.pdf (A document describing the model)