我正在尝试使用 NuSMV 作为 LTL 公式的可满足性检查器,即我想知道给定公式是否存在模型。我知道 NuSMV 也可以用于此目的,既因为它在理论上是可能的,也因为我看到它在许多处理可满足性的论文中被引用(其中一篇还声称 NuSMV 是最快的可满足性检查器之一那里)。
我看到 NuSMV 附带了一个名为的工具,该工具ltl2smv
显然将 LTL 公式转换为 SMV 模块,但后来我不知道如何使用输出。将它直接提供给 NuSMV 会返回一条关于“主”未定义的错误消息,所以我想我必须定义一个主模块并以某种方式使用另一个模块。由于我从未将 NuSMV 用作模型检查器,因此我不知道它的语言是如何工作的,而且鉴于我只需要这个特定的用例,用户指南是压倒性的,顺便说一下,该指南中的任何地方都没有提到它。
那么如何使用 NuSMV 来检查 LTL 公式的可满足性呢?是否有记录此用例的地方?