从不声明在普罗梅拉模型中不起作用

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 声明不起作用，尽管我用 sping 生成了它？

我错过了一些基本的东西吗？

Answer 1

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

参考资料：

要将 LTL 公式转换为永不声明，我们必须首先考虑该公式是表达正属性还是负属性。积极的属性表达了我们希望我们的系统拥有的良好行为。负属性表示我们声称系统没有的不良行为。永不声明通常仅用于形式化负属性(不应该发生的行为(，这意味着在将正属性转换为声明之前必须否定它们。

Answer 2

将声明放在源代码中(例如，check.pml(

int x = 0;
init {
    do
    :: x < 10 ->
        x++;
    od
}
ltl  { [] (x != 4) }

然后

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

这给了

pan:1: assertion violated  !( !((x!=4))) (at depth 16)
pan: wrote check.pml.trail

您可以观看小径

./pan -r -v

恕我直言，使用额外的工具从声明中构建自动机非常不方便，而且经常令人困惑。