module main {
    // Define input signals from detectors
    input arrival : boolean;
    input departure : boolean;

    // Define the counter variable
    var counter : integer;

    // Initialize the counter with an initial value i
    init {
        counter = 0;
    }

    // Update the counter based on the arrival and departure inputs
    next {
        if (arrival) {
            counter' = counter + 1;
        } else if (departure) {
            counter' = counter - 1;
        } else {
            counter' = counter;
        }
    }

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

    // Control block for simulation and checking
    control {
        v = simulate(10);  // Simulate for 10 steps
        print_trace;
        check;
    }
}
