#define ROOM 3
byte fork0, fork1, fork2, fork3, fork4;
byte count=0;

#define PHIL_ROOM(NAME, FORK_ONE, FORK_TWO)\
active proctype NAME()\
{\
think: if\
::  atomic {count<ROOM;count = count+1;}  goto inside;\
fi;\
inside: if\
:: count = count-1; goto think;\
:: atomic {FORK_ONE==0;FORK_ONE = 1;}  goto one;\
fi;\
one: if\
::  atomic {FORK_TWO==0;FORK_TWO = 1;}  goto eat;\
fi;\
eat: if\
:: FORK_ONE = 0; goto finish;\
fi;\
finish: if\
:: FORK_TWO = 0; goto inside;\
fi;\
}


PHIL_ROOM(phil0, fork0, fork1)

PHIL_ROOM(phil1, fork1, fork2)

PHIL_ROOM(phil2, fork2, fork3)

PHIL_ROOM(phil3, fork3, fork4)

PHIL_ROOM(phil4, fork4, fork0)

never
{
again:
  if
  :: true;goto again;
  :: fork0 && fork1 && fork2 && fork3 && fork4;
  fi;
}

