module ArrivalDetector
{
    output arrival : boolean;

    init {
        arrival = false;
    }

    next {
        arrival' = nondet(); // Non-deterministically generate arrival events
    }
}

module DepartureDetector
{
    output departure : boolean;

    init {
        departure = false;
    }

    next {
        departure' = nondet(); // Non-deterministically generate 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 && !departure) {
            counter' = counter + 1;
        } else if (!arrival && departure) {
            counter' = counter - 1;
        } else {
            counter' = counter;
        }
    }
}

module main
{
    instance arr_det : ArrivalDetector;
    instance dep_det : DepartureDetector;
    instance count : Counter(arrival: arr_det.arrival, departure: dep_det.departure);

    init {
        // Initialize system
    }

    next {
        next(arr_det);
        next(dep_det);
        next(count);
    }

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