boost - 是否有选项可以增加 NuSMV 在规范运行期间可以使用的内存量？

Question

在 nusmv 中运行规范期间，需要几个小时并最终给出“killed 9”的结果。如何加快执行速度？是否有选项可以增加 NuSMV 在规范运行期间可以使用的内存量？

Answer 1

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

总的来说，这取决于 NuSMV 内存不足的原因。大多数情况下，它无法构建模型，这意味着您必须减小模型大小。为此，您可能想查看某些状态变量是否可以成为没有状态的布尔信号，或者您是否需要减少某些变量的范围。

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