module BookingSystem {
  var BCR_state: bv1;
  var BP_state: bv1;
  var Printer_state: bv1;

  next {
    if (BCR_state == 0bv1) {
      BCR_state' = 1bv1;
    } else {
      if (BCR_state == 1bv1) {
        BCR_state' = 0bv1;
      }
    }
    if ((BP_state == 0bv1) && (BCR_state == 1bv1)) {
      BP_state' = 1bv1;
    } else {
      if ((BP_state == 1bv1) && (Printer_state == 0bv1)) {
        BP_state' = 0bv1;
      }
    }
    if (BP_state == 1bv1) {
      Printer_state' = 1bv1;
    } else {
      if (Printer_state == 1bv1) {
        Printer_state' = 0bv1;
      }
    }

  }
}
