我想知道是否有一种方法可以为 NuSMV 中的给定 LTL 公式生成不同的可能反例。如果我们需要为 LTL 公式生成反例，它会为我们生成一个。但是由 NuSMV 生成的那个可能不是最令人兴奋或最有见地的，因为对于相同的 LTL 公式可能还有其他反例。
你能建议一些一般的方法来让 NuSMV 产生一些与其产生的反例不同的反例吗？
一种方法是修改 LTL 公式本身，以便 NuSMV 一次性生成的反例对我们来说很有趣。但我相信系统的操纵过多，无法获得您想要的结果。
另外，您需要事先知道有趣的结果。但如果我已经知道有趣的反例，我为什么要让 NuSMV 再次向我确认呢？那么为什么还要麻烦设计一个 LTL 表达式来给出所需的反例呢？我希望 NuSMV 生成其他我没有想到的有趣的反例，从而增加价值。
如果在 NuSMV 中不可能，您能否建议任何其他可能的 LTL 模型检查器？