module Module {
  var count: integer;

  input arrival: boolean;
  input departure: boolean;

  output counter: integer;

  init {
    count = 0;

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

  next {
    call step();
  }
}
