1 
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 来验证一个更复杂的排队系统，它使用像这样的绝对帧索引。

4

0 回答 0