verification - 切勿声称在 promela 模型中不起作用

Question

考虑这个简单的 PROMELA 模型:

#define p (x!=4)

int x = 0;

init {
    do
    :: x < 10 ->
        x++;
    od
}

我想用这个简单的声明来验证这个模型，该声明是使用 spin -f 生成的:

never {    /* []p */
accept_init:
T0_init:
    do
    :: ((p)) -> goto T0_init
    od;
}

但是，验证使用

spin -a model.pml
cc -o pan pan.c
./pan

没有结果。尝试 -a 选项也不会产生结果。 任何随机模拟都表明，显然 p 在某些时候是错误的，那么为什么 never 声明不起作用，尽管我用 spin 生成了它？

我是否遗漏了一些基本的东西？

Answer 1

如果您想检查[]p，则需要为![]p构造一个never声明。

来自reference :

To translate an LTL formula into a never claim, we have to consider first whether the formula expresses a positive or a negative property. A positive property expresses a good behavior that we would like our system to have. A negative property expresses a bad behavior that we claim the system does not have. A never claim is normally only used to formalize negative properties (behaviors that should never happen), which means that positive properties must be negated before they are translated into a claim.