queue - 範囲外の値を持つ Promela システム

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();
}

このシステム (単なる例) は、リーダーがフレームの特定のスパンを要求するリーダー/ライター キューをモデル化する必要が[rq_begin,rq_end]あり、ライターは少なくともこのスパンを利用可能にする必要があります。[av_begin,av_end]利用可能なフレームのスパンです。

4 つの値は絶対フレーム インデックスでrq_beginあり、リーダーがフレームの次のスパンを読み取ると、無限にインクリメントされます。

値が範囲外であるため、システムを直接検証することはできません (無限に多くの状態が生成されます)。Promela/Spin (または同様のソフトウェア) は、このようなシステムを検証し、有限になるように自動的に変換する機能をサポートしていますか?

たとえば、4 つの値がすべて同じ量だけ増分された場合でも、状況は同じです。または、代わりにこれらの値の差の変数を持つモデルに再定式化することもできますav_end - rq_end。

私は Promela/Spin を使用して、このような絶対フレーム インデックスを使用するより複雑なキューイング システムを検証しています。