永远不要声称在 promela 模型中不起作用答案

【问题标题】：Never claim does not work in promela model永远不要声称在 promela 模型中不起作用
【发布时间】：2016-02-16 09:12:06
【问题描述】：

考虑这个简单的 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 显然是错误的，那么尽管我使用 spin 生成了它，为什么 never 声明不起作用？

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

【问题讨论】：

【解决方案1】：

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

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

【讨论】：

【解决方案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

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

【讨论】：