是否有选项可以提高NuSMV在规范运行期间可以使用的内存量？

Question

在nusmv规范运行过程中，它需要几个小时，最终导致“死亡9”的结果。如何加快执行速度？ 是否有选项可以提高NuSMV在规范运行期间可以使用的内存量？

Answer 1

您可能想使用nuSMV的后继者nuXmv https://es-static.fbk.eu/tools/nuxmv/。它提供了更新的基于SAT的模型检查算法，这些算法通常使用的内存少于基于BDD的模型检测算法，并且它允许与NuSMV相同的模型规格。

总的来说，这取决于NuSMV为什么耗尽内存。大多数时候，它不会设法建立模型，这意味着您必须减少模型大小。为此，您可能需要查看某些状态变量是否可以成为没有状态的布尔信号，或者如果您减少了某些变量的范围。

如果您有参数化模型，例如，使用可变数量的模块或某些变量的位宽可以更改，您可以尝试获得更简单的变量以运行，然后找出哪个部分使内存需求增长。这部分应该以不同的方式建模。