如何解释NuXMV的msat命令的结果

Question

我使用NuXMV在一个相当大的模型上使用msat_check_ltlspec_bmc命令检查LTL属性。结果显示，在给定的边界内没有发现反例。我是否把它解释为那个属性是真的。或者，这也意味着分析不完整。

这是因为，通过将属性命题更改为true或false，结果总是没有反例。大多数结果都是违反直觉的。

从基于实变量的属性开始，但由于无法理解结果，因此使用相同的命令转移到基于布尔的属性上。

Answer 1

有界模型检验是一种面向bug的技术，它在执行时检查属性的有效性，跟踪到给定的长度k。

• 当执行跟踪违反属性时，很好:发现了一个bug。
• 否则，(在一般情况下)模型检查结果没有提供有用的信息，因此应该将其视为有用的信息。

在某些情况下，了解有关模型的其他信息会有所帮助。特别是，如果知道长度为k的每个执行跟踪必须循环回k-1状态之一，那么就有可能从缺少长度小于或等于k的反示例中得出更强的结论。