1

假设我在 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 处终止上面的反例呢？

有人可以解释吗？

4

1 回答 1

0

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

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

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

S1->S2->S3->S2

由两部分组成：

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

这是您的自动机的有效无限执行路径，这意味着程序始终从S3to跳转S2和从不转到是合法的S4，并且由于它从不接触S70它也是您属性的反例。

我不确定如何进一步帮助您解决问题，因为您没有说明您使用的是LTL还是CTL，也没有提供有关您的模型的任何进一步信息。可能需要更改您的模型、属性或两者。如果可以的话，我建议您查看本课程第二部分中的幻灯片NuSMV，nuXmv以更好地了解该工具。

编辑

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

那么，解决的办法就是从验证部分排除这种执行痕迹，使其不能作为反例出现。确切的解决方案可能取决于正在验证的模型，它对我不可用，但一个例子可能是：

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

此编码假定不存在到S2after的环回S70。否则，应使用其他方法。

于 2018-09-06T07:49:06.977 回答