module ParkingGarageSystem
{
  // Define the variables
  var arrival : boolean;
  var departure : boolean;
  var counter : integer;

  // Initial conditions
  init {
    counter = 0; // Starting with an initial count of 0 cars
  }

  // Transition relation describing how the system state updates
  next {
    if (arrival) {
      counter' = counter + 1; // Increment counter on arrival
    } else if (departure) {
      counter' = counter - 1; // Decrement counter on departure
    } else {
      counter' = counter; // No change if no events
    }
  }

  // Safety property: the counter should never be negative
  invariant non_negative_counter : (counter >= 0);

  control {
    // Perform bounded model checking
    v = unroll(10);
    check;
    print_results;
  }
}
