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)