Notice: this Wiki will be going read only early in 2024 and edits will no longer be possible. Please see: https://gitlab.eclipse.org/eclipsefdn/helpdesk/-/wikis/Wiki-shutdown-plan for the plan.
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.
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|
contributed by Christian Krause