class DiningServer{

   private static final int
      THINKING = 0, HUNGRY = 1, EATING = 2;
   private int numPhils = 0;
   private int[] state = null;
   private BinarySemaphore[] fork = null;
   private CountingSemaphore room = null;

   public DiningServer(int numPhils) {
      this.numPhils = numPhils;
      state = new int[numPhils];
      for (int i = 0; i < numPhils; i++) state[i] = THINKING;
      fork = new BinarySemaphore[numPhils];
      for (int i = 0; i < numPhils; i++) fork[i] = new BinarySemaphore(1);
      // NOTE: a room that only allows numPhils-1 prevents a deadlock.
      //       a room that allows numPhils admits a deadlocking schedule.
      //       It seems that the shortest deadlocking schedule is a little
      //       under 800 Spin transitions (around 98 steps in the Java code).
      //       Thus, the Spin options are set to limit that trace depth to
      //       800.
      // room = new CountingSemaphore(numPhils-1);
      room = new CountingSemaphore(numPhils);
      System.out.println("Dining room limited to " + (numPhils-1));
   }

   private final int left(int i) { return (numPhils + i - 1) % numPhils; }

   private final int right(int i) { return (i + 1) % numPhils; }

   public void takeForks(int i) {
      state[i] = HUNGRY;
      room.P(); fork[i].P(); fork[right(i)].P();
      state[i] = EATING;
      System.out.println("Phil "+i+" eating");
   }

   public void putForks(int i) {
      fork[i].V(); fork[right(i)].V(); room.V();
      state[i] = THINKING;
      System.out.println("Phil "+i+" thinking");
   }
}