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

Question

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

Answer 1

一般来说，这是不可能的，因为合理规模的系统能够产生无限多这样的反例。想一想您的系统有一个 "bad cycle" 可以任意频繁输入或在有限但任意延迟之后输入：每个这样的延迟都会产生一个新的反例。

Answer 2

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

基本上，这称为 CEGAR——反例引导的抽象细化，只是它不是抽象模型，而是在每次迭代中细化规范。