module ArrivalDetector {
    output arrival : boolean;

    init {
        arrival = false;
    }

    next {
        arrival' = nondet(); // non-deterministic generation of arrival events
    }
}

module DepartureDetector {
    output departure : boolean;

    init {
        departure = false;
    }

    next {
        departure' = nondet(); // non-deterministic generation of departure events
    }
}

module Counter {
    input arrival : boolean;
    input departure : boolean;
    var counter : integer;

    init {
        counter = 0; // Initial count of cars in the garage
    }

    next {
        if (arrival) {
            counter' = counter + 1;
        } else if (departure) {
            counter' = counter - 1;
        } else {
            counter' = counter;
        }
    }

    output display : integer = counter; // Output to update display
}

module main {
    instance arrivalDetector : ArrivalDetector;
    instance departureDetector : DepartureDetector;
    instance counter : Counter(arrival: arrivalDetector.arrival, departure: departureDetector.departure);

    init {
        assume(counter.counter == 0); // Assume garage starts empty
    }

    next {
        next(arrivalDetector);
        next(departureDetector);
        next(counter);
    }

    invariant no_negative_count : (counter.counter >= 0);
}

control {
    v = unroll(10);
    check;
    print_results;
}
