PAT: Process Analysis Toolkit

An Enhanced Simulator, Model Checker and Refinement Checker for Concurrent and Real-time Systems

Dining Philosophers

The dining philosophers problem is summarized as five philosophers sitting at a table doing one of two things – eating or thinking. While eating, they are not thinking, and while thinking, they are not eating. The five philosophers sit at a circular table with a large bowl of spaghetti in the center. A fork is placed in between each philosopher, and as such, each philosopher has one fork to his or her left and one fork to his or her right. As spaghetti is difficult to serve and eat with a single fork, it is assumed that a philosopher must eat with two forks. The philosopher can only use the fork on his or her immediate left or right.

The CSP Definition of Dining Philosophers:




The property interested states that every philosopher will always eventually eat, i.e., no one shall starve.




The following defintion is the Dining Philosophers example with size 3.
====================Process Definitions====================
phi0()=((t0->phi0())[](wl(g01)->(g00->(e0->(p01->(p00->phi0()))))));
f0()=((g00->(wl(p00)->f0()))[](g20->(wl(p20)->f0())));
phi1()=((t1->phi1())[](wl(g12)->(g11->(e1->(p12->(p11->phi1()))))));
f1()=((g11->(wl(p11)->f1()))[](g01->(wl(p01)->f1())));
phi2()=((t2->phi2())[](wl(g20)->(g22->(e2->(p20->(p22->phi2()))))));
f2()=((g22->(wl(p22)->f2()))[](g12->(wl(p12)->f2())));
DiningPhilosophers()=(phi0()||f0()||phi1()||f1()||phi2()||f2());

============================Assertions===========================

  1. assert DiningPhilosophers() |= []<>e0;
  2. assert DiningPhilosophers() deadlockfree;
  3. assert DiningPhilosophers() feasible;
  4. assert DiningPhilosophers() |= []<>e0 && []<>e1 && []<>e2;