module ParkingCounter {
  var arrival: boolean;
  var departure: boolean;
  var counter: integer;
  var display_count: integer;

  init {
    counter = 0;
    display_count = 0;

  }
  procedure step()
    modifies counter;
    modifies display_count;
  {
    if (arrival) {
      counter = (counter + 1);
    }
    if (departure && (counter > 0)) {
      counter = (counter - 1);
    }
    display_count = counter;
  }

  next {
    call step();
  }
  invariant spec: (counter >= 0);

}
