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

Question

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

Answer 1

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

Answer 2

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

基本上，这称为 CEGAR - 反例引导的抽象细化，除了它不是抽象模型，而是在每次迭代时对规范进行细化。