如何找出所有可能的反例Nusmv

Question

我在NuSMV中有一个模型，在检查了ltl规范后，NuSMV给我一个反例，有没有可能找出所有包含反例的路径，而不是其中之一？

Answer 1

您可以使用您的反例来改进您的LTL规范，然后再次使用改进后的规范进行模型检查。重复此操作，直到NuSMV找不到更多的反例，但在某些情况下，它可能永远不会结束。

基本上，这被称为CEGAR -反例指导的抽象细化，除了它不是抽象模型，但规范在每次迭代中都会得到改进。

Answer 2

一般来说，这是不可能的，因为合理规模的系统能够产生无限多的这样的反例。想象一下您的系统有一个“坏循环”，它可以经常或在有限但任意的延迟之后任意进入:每一个这样的延迟都会产生一个新的反例。