NuSMV陷入了一个微不足道的死锁

Question

假设我在NuSMV中编写了一个以状态S1开头的模型。我想检查这个模型检查器中的条件，在所有情况下我是否最终到达状态S70。现在，将我编写的NuSMV模型可视化如下：

​

​

从上面看，很明显，最终会到达S70，但它可能需要70多个时间步骤。为什么？因为您可以转到S2，然后再转到S3，而不是再次返回到S2，这个模式重复了100次，比如100次。NuSMV软件也考虑到了这种可能性，以确认一定会达到S70。

问题是NuSMV说S70不会被触及，并产生了一个反例，就是这样的：-

S1->S2->S3->S2

反例就是这四个步骤。但我感到惊讶的是，NuSMV没有发现这种僵局最终会随着时间的推移而得到解决。为什么我会得到一个非直觉的结果？

我在图中显示的自动机可能是我希望我的NuSMV代码表示的，但我错误地编码了一两行，但我不这么认为。否则，NuSMV为什么会想到它可以从S2转到S3。如果它可以计算出可以从S2到S3，那么为什么在S2终止上面的反例呢？

有人能解释一下吗？

Answer 1

但是我很惊讶，NuSMV没有发现这个僵局最终会随着时间的推移而得到解决。

我不确定这种情况是否符合定义，定义。无论如何，NuSMV指出存在一个程序永远不会到达状态S70的执行是正确的。

可达性问题的反例(在没有死锁状态的适当模型中)总是无限执行跟踪。你得到的反例是：

S1->S2->S3->S2

由两部分组成：

• 前缀部件:状态序列，从初始状态开始，到达无限循环部分。在这种情况下，它只是S1。
• 循环部件:一个自循环的状态序列，它很容易识别，因为它以它启动的相同状态结束。在本例中，它是S2 -> S3 -> S2

这是您的自动机的一个有效的无限执行路径，这意味着程序总是从S3跳转到S2，而不跳转到S4，这是合法的，而且因为它从不触及S70，所以它也是您的属性的反例。

我不知道怎样才能在你的问题上进一步帮助你，因为你没有说明你是在使用LTL还是CTL，也没有给出任何关于你的模型的进一步信息。可能有必要更改您的模型、属性或两者。如果可以的话，我建议您查看这门课 on NuSMV/nuXmv第二部分中的幻灯片，以便更好地理解该工具。

编辑

让我们假设，在正在建模的现实世界场景中，这种无限执行在技术上是不可能发生的，即这种可能性是建模阶段引入的一些简化的结果，或者这种情况可能实际发生，但出于有文档的原因，我们对这种极端情况不感兴趣。

然后，解决方案是从验证部分排除这种执行跟踪，这样它就不能作为反示例出现。确切的解决方案可能取决于正在验证的模型，而我无法得到该模型，但一个例子可以是：

 (! (G (F S2))) -> (F S70)

这种编码假设在S70之后不存在返回到S70的循环。否则，应采用其他办法。