# Henshin/Examples/DiningPhilosophers

The Dining Philosophers problem is a classical model checking scenario. We use it as an example to give an intuition about the rule-based modeling in Henshin and to conduct a benchmark for its state space exploration feature.

#### Transformation System

The transformation consists of four rules shown below. In rule left(p) philosopher p picks up his left fork, and analogously for the rule right(p). In rule release(p) the philospher p releases his fork again. The most interesting rule is createPhilosopher(x) where x refers to the highest philosopher ID in the model (note that Henshin can find all parameters automatically here). The rule createPhilosopher(x) can be used to dynamically add a philosopher to the table and to link it to its neighbors. We use this rule to derive initial models for different numbers of philosophers below.

#### State Space Generation

The state space can be either generated in the state space explorer (slow), or by right-clicking on a statespace file and selecting State Space -> Explore State Space, or programmatically as done the DiningPhilsBenchmark class. The screenshot below shows the state space for 3 philosophers as visualized in the state space explorer. Note that we do not make use of graph isomorphy checking for making the state space smaller, because we want to be able to identify each philosopher individually (by its ID).

We conducted a benchmark to measure the speed of the state space generator. The models and the source code for the example can be found here. The following benchmark was conducted on a Intel(R) Xeon(R) CPU @ 2.50GHz with 8GB of main memory using Henshin 0.9.2. We measured the time to generate the full state space.

Philosophers     States (= 3^p)     Transitions     Time
3 27 63 56ms
4 81 252 69ms
5 243 945 224ms
6 729 3,402 616ms
7 2,187 11,907 1.3s
8 6,561 40,824 5.0s
9 19,683 137,781 19.8s
10 59,049 459,270 80.5s
11 177,147 1,515,591 6min
12 531,441 4,960,116 61min
13 1,594,323 16,120,377 593min

contributed by Christian Krause