module SupermarketSystem {
  var BCR_state: integer;
  var BP_state: integer;
  var Printer_state: integer;

  init {
    BCR_state = 0;
    BP_state = 0;
    Printer_state = 0;

  }
  procedure step()
    modifies BCR_state;
    modifies BP_state;
    modifies Printer_state;
  {
    if (BCR_state == 0) {
      BCR_state = 1;
    } else {
      if (BCR_state == 1) {
        BCR_state = 0;
        BP_state = 1;
      }
    }
    if (BP_state == 1) {
      BP_state = 0;
      Printer_state = 1;
    }
    if (Printer_state == 1) {
      Printer_state = 0;
    }
  }

  next {
    call step();
  }
  invariant spec: !(((BCR_state == 1) && (BP_state == 1)) || ((Printer_state == 1) && (BP_state == 1)));

}
