module main {
    // Define the initial value of the counter
    const i : int;

    // Define inputs for arrival and departure events
    input arrival : boolean;
    input departure : boolean;

    // Define the counter variable
    var counter : int;

    // Initialization of the counter
    init {
        counter = i;
    }

    // Transition rules for the counter
    next {
        if (arrival) {
            counter' = counter + 1;
        } else if (departure && counter > 0) {
            counter' = counter - 1;
        } else {
            counter' = counter;
        }
    }

    // Output logic: Assume there's an external function to update the display
    procedure updateDisplay(new_count : int) {
        // This would interface with the display hardware/software
        // Placeholder for actual implementation
    }

    // Call updateDisplay whenever the counter changes
    next {
        if (counter' != counter) {
            call updateDisplay(counter');
        }
    }

    // Safety invariant to ensure the counter never falls below zero
    invariant non_negative_counter : (counter >= 0);

    // Model checking control block
    control {
        // Define the verification sequence
        v = unroll(10);
        check;
        print_results;
    }
}
