byte fork0, fork1, fork2, fork3, fork4, fork5, fork6, fork7, fork8, fork9, fork10, fork11;

#define PHIL(NAME, FORK_ONE, FORK_TWO)\
active proctype NAME()\
{\
think: if\
::  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 think;\
fi;\
}

PHIL(phil0, fork0, fork1)

PHIL(phil1, fork1, fork2)

PHIL(phil2, fork2, fork3)

PHIL(phil3, fork3, fork4)

PHIL(phil4, fork4, fork5)

PHIL(phil5, fork5, fork6)

PHIL(phil6, fork6, fork7)

PHIL(phil7, fork7, fork8)

PHIL(phil8, fork8, fork9)

PHIL(phil9, fork9, fork10)

PHIL(phil10, fork10, fork11)

PHIL(phil11, fork11, fork0)

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