-- Dining Philosopher's problem
-- by David Paul Boerschlein
-- August, 1998
program dining
const N=5;
STARVELIMIT=100;
var
starvation.0..0: integer[0];
deadlock.0..0: integer[0];
iter.0..0: integer[0];
fork.1..N: integer [all(, j:1..N | 0)];
want2eat.1..N: integer [all(, j:1..N | 0)];
eat.1..N: integer [all(, j:1..N | 0)];
eatcount.1..N: integer [all(, j:1..N | 0)];
process
p: 1..N
actions
-- Philosopher decides he wants to eat
(want2eat.p == 0) and
(fork.(1 + ((p+N-1) mod N)) == 0) and
(fork.(1 + (p mod N)) == 0)
	-> iter.0:= iter.0+ 1;
	   want2eat.p := iter.0
[]
-- Philosopher can pick up left fork
(want2eat.p > 0) and
(fork.(1 + ((p+N-1) mod N)) == 0)
	-> fork.(1 + ((p+N-1) mod N)) := p;
	   iter.0:= iter.0+ 1

 []

-- Philosopher can pick up right fork
(want2eat.p > 0) and
(fork.(1 + (p mod N)) == 0)
	-> fork.(1 + (p mod N)) := p;
	   iter.0:= iter.0+ 1 
[]
 -- Philosopher starts eating
(want2eat.p > 0) and
(eat.p == 0) and
(fork.(1 + ((p+N-1) mod N)) == p) and
(fork.(1 + (p mod N)) == p)
	-> eat.p := 1;
	   eatcount.p := eatcount.p + 1; 
	   iter.0:= iter.0+ 1
[]
-- Philosopher decides to stop eating
(eat.p == 1) and
(want2eat.p > 0)
	-> want2eat.p := 0;
	   iter.0:= iter.0+ 1
[]
-- Philosopher stops eating and lays down forks
(eat.p == 1) and
(want2eat.p == 0)
	-> eat.p := 0;
	   fork.(1 + ((p+N-1) mod N)) := 0;
	   fork.(1 + (p mod N)) := 0;
	   iter.0:= iter.0+ 1

 []

-- Deadlock occurs when everybody wants to eat and everybody
-- holds one and only one fork.
(all (and j:1..N | (
  (want2eat.j > 0) and
  (
   ((fork.(1 + ((j+N-1) mod N)) == j) and (fork.(1 + (j mod N)) != j)
     and (fork.(1 + (j mod N)) != 0)) or
     ((fork.(1 + (j mod N)) == j) and (fork.(1 + ((j+N-1) mod N)) != j)
     and (fork.(1 + ((j+N-1) mod N)) != 0))
    )
   ) 
  )
 )
	-> deadlock.0 := 1;
	   iter.0:= iter.0+ 1

 []

-- Starvation occurs when some philosopher has wanted to eat for
-- too many iterations
(want2eat.p > 0) and
(iter.0 > (want2eat.p + STARVELIMIT))
	-> starvation.0 := p;
	   iter.0 := iter.0 + 1
topology 5 ring
semantics interleaving
invariant
	(deadlock.0 == 0) and
	(starvation.0 == 0)