NuSMV陷入了一个微不足道的僵局

Question

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

从上面可以看出，最终将达到S70，但可能需要超过70个时间步长。为什么？因为您可以转到S2然后转到S3，然后再转到S4再转回S2，这种模式重复，比如说100次。 NuSMV软件也考虑了这些可能性，以确认肯定会达到S70。

问题是NuSMV表示不会达到S70并产生一个反例，正是这样：

S1->S2->S3->S2

所以反例就是这4个步骤。但令我惊讶的是，NuSMV无法弄清楚这种僵局最终会随着时间的推移而得到解决。为什么我得到一个非直观的结果？

我在图中显示的自动机可能是我想要的NuSMV代码所代表的，但我错误地编写了一两行，但我不这么认为。否则NuSMV怎么会想到它可以从S2到S3。如果它可以确定一个人可以从S2到S3那么为什么在S2处终止上面的反例？

谁能解释一下？

Answer 1

但令我惊讶的是，NuSMV无法弄清楚这种僵局最终会随着时间的推移而得到解决

我不确定这种情况是否对应于definition of "deadlock"。无论如何，NuSMV指出存在一个程序将永远不会达到状态S70的执行是正确的。

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

S1->S2->S3->S2

由两部分组成：

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

这是你的自动机的一个有效的无限执行路径，这意味着程序始终从S3跳到S2并且永远不会去S4是合法的，并且因为它从不接触S70它也是你的财产的反例。

---

我不确定如何进一步帮助解决您的问题，因为您没有说明您使用的是LTL还是CTL，也没有提供有关您的模型的任何进一步信息。可能需要更改模型，属性或两者。如果可以的话，我会建议你看一下this course / NuSMV上nuXmv第二部分的幻灯片，以便更好地理解这个工具。

编辑

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

然后，解决方案是从验证部分中排除这样的执行跟踪，因此它不能作为反例出现。确切的解决方案可能取决于正在验证的模型，我无法使用，但一个例子可能是：

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

这种编码假设在S2之后没有回到S70的回送。否则，应使用其他方法。