Promela system with unranged values

Question

int rq_begin = 0, rq_end = 0;
int av_begin = 0, av_end = 0;

#define MAX_DUR 10
#define RQ_DUR 5

proctype Writer() {
    do
    ::  (av_end < rq_end) -> av_end++;
        if
        :: (av_end - av_begin) > MAX_DUR -> av_begin = av_end - MAX_DUR;
        :: else -> skip;
        fi
        printf("available span: [%d,%d]\n", av_begin, av_end);
    od
}

proctype Reader() {
    do
    ::  d_step {
            rq_begin++;
            rq_end = rq_begin + RQ_DUR;
        }
        printf("requested span: [%d,%d]\n", rq_begin, rq_end);
        (rq_begin >= av_begin && rq_end <= av_end);
        printf("got requested span\n");
    od
}

init {
    run Writer();
    run Reader();
}

This system (only an example) should model a reader/writer queue where the reader requests a certain span of frames [rq_begin,rq_end], and the writer should then make at least this span available. [av_begin,av_end] is the span of available frames.

The 4 values are absolute frame indices, rq_begin gets incremented infinitley as the reader reads the next span of frames.

The system cannot be directly verified because the values are unranges (generating infinitely many states). Does Promela/Spin (or a similar software) has support to verify a system like this, and automatically transform it such that it becomes finite?

For example if all the 4 values were incremented by the same amount, the situation would still be the same. Or it could be reformulated into a model which instead has variables for the differences of these values, for example av_end - rq_end.

I'm using Promela/Spin to verify a more complex queuing system which uses absolute frame indices like this.