#define ROOM 9
byte fork0, fork1, fork2, fork3, fork4, fork5, fork6, fork7, fork8, fork9, fork10, fork11, fork12;
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, fork5)

PHIL_ROOM(phil5, fork5, fork6)

PHIL_ROOM(phil6, fork6, fork7)

PHIL_ROOM(phil7, fork7, fork8)

PHIL_ROOM(phil8, fork8, fork9)

PHIL_ROOM(phil9, fork9, fork10)

PHIL_ROOM(phil10, fork10, fork11)

PHIL_ROOM(phil11, fork11, fork12)

PHIL_ROOM(phil12, fork12, fork0)

never
{
again:
  if
  :: true;goto again;
  :: fork0 && fork1 && fork2 && fork3 && fork4 && fork5 && fork6 && fork7 && fork8 && fork9 && fork10 && fork11 && fork12;
  fi;
}

