module Module {
  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 = false;
    chopstick2 = false;
    chopstick3 = false;
    chopstick4 = false;
    chopstick5 = false;

  }
  next {
    chopstick1' = ((!chopstick1 && phil1) && phil2);
    chopstick2' = ((!chopstick2 && phil2) && phil3);
    chopstick3' = ((!chopstick3 && phil3) && phil4);
    chopstick4' = ((!chopstick4 && phil4) && phil5);
    chopstick5' = ((!chopstick5 && phil1) && phil5);

  }
  invariant spec: !((((chopstick1 && chopstick2) && chopstick3) && chopstick4) && chopstick5);

}
