module DiningPhilosophersModule {
  var phil1: boolean;
  var phil2: boolean;
  var phil3: boolean;
  var phil4: boolean;
  var phil5: boolean;
  var chopstick1: boolean;
  var chopstick2: boolean;
  var chopstick3: boolean;
  var chopstick4: boolean;
  var chopstick5: boolean;

  init {
    phil1 = false;
    phil2 = false;
    phil3 = false;
    phil4 = false;
    phil5 = false;
    chopstick1 = true;
    chopstick2 = true;
    chopstick3 = true;
    chopstick4 = true;
    chopstick5 = true;

  }
  next {
    if ((!phil1 && chopstick1) && chopstick5) {
      phil1' = true;
      chopstick1' = false;
      chopstick5' = false;
    } else {
      if (phil1) {
        phil1' = false;
        chopstick1' = true;
        chopstick5' = true;
      }
    }

  }
}
