#define NumOfPhilosophers 5
#define NumOfForks 5

mtype = { thinking, eating, available, nonavailable };
#define PhilosopherState mtype
#define ForkState mtype

bool Fail = false;
PhilosopherState philosophers[NumOfPhilosophers] = thinking;
ForkState forks[NumOfForks] = available;





proctype Philosopher_0(int i) {
do
  ::atomic{
    ((philosophers[i]==thinking)&&(forks[i]==available)&&(forks[(i+1)%NumOfForks]==available)) ->
    philosophers[i] = eating;
    forks[i] = nonavailable;
    forks[(i+1)%NumOfForks] = nonavailable;
    };
  ::atomic{
    philosophers[i]==eating ->
    philosophers[i] = thinking;
    forks[i] = available;
    forks[(i+1)%NumOfForks] = available;
    };
od;
}

proctype Philosopher_1(int i) {
do
  ::atomic{
    ((philosophers[i]==thinking)&&(forks[i]==available)&&(forks[(i+1)%NumOfForks]==available)) ->
    philosophers[i] = eating;
    forks[i] = nonavailable;
    forks[(i+1)%NumOfForks] = nonavailable;
    };
  ::atomic{
    philosophers[i]==eating ->
    philosophers[i] = thinking;
    forks[i] = available;
    forks[(i+1)%NumOfForks] = available;
    };
od;
}

proctype Philosopher_2(int i) {
do
  ::atomic{
    ((philosophers[i]==thinking)&&(forks[i]==available)&&(forks[(i+1)%NumOfForks]==available)) ->
    philosophers[i] = eating;
    forks[i] = nonavailable;
    forks[(i+1)%NumOfForks] = nonavailable;
    };
  ::atomic{
    philosophers[i]==eating ->
    philosophers[i] = thinking;
    forks[i] = available;
    forks[(i+1)%NumOfForks] = available;
    };
od;
}

proctype Philosopher_3(int i) {
do
  ::atomic{
    ((philosophers[i]==thinking)&&(forks[i]==available)&&(forks[(i+1)%NumOfForks]==available)) ->
    philosophers[i] = eating;
    forks[i] = nonavailable;
    forks[(i+1)%NumOfForks] = nonavailable;
    };
  ::atomic{
    philosophers[i]==eating ->
    philosophers[i] = thinking;
    forks[i] = available;
    forks[(i+1)%NumOfForks] = available;
    };
od;
}

proctype Philosopher_4(int i) {
do
  ::atomic{
    ((philosophers[i]==thinking)&&(forks[i]==available)&&(forks[(i+1)%NumOfForks]==available)) ->
    philosophers[i] = eating;
    forks[i] = nonavailable;
    forks[(i+1)%NumOfForks] = nonavailable;
    };
  ::atomic{
    philosophers[i]==eating ->
    philosophers[i] = thinking;
    forks[i] = available;
    forks[(i+1)%NumOfForks] = available;
    };
od;
}

init {
int p0 = 0;
int p1 = 1;
int p2 = 2;
int p3 = 3;
int p4 = 4;
 atomic{
 run Philosopher_0(p0);
 run Philosopher_1(p1);
 run Philosopher_2(p2);
 run Philosopher_3(p3);
 run Philosopher_4(p4);
 };
}