byte fork0, fork1, fork2, fork3;

#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, fork0)

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

