是否有選項可以提高NuSMV在規範運行期間可以使用的內存量？

Question

在nusmv規範運行過程中，它需要幾個小時，最終導致「死亡9」的結果。如何加快執行速度？ 是否有選項可以提高NuSMV在規範運行期間可以使用的內存量？

Answer 1

您可能想使用nuSMV的後繼者nuXmv https://es-static.fbk.eu/tools/nuxmv/。它提供了更新的基於SAT的模型檢查算法，這些算法通常使用的內存少於基於BDD的模型檢測算法，並且它允許與NuSMV相同的模型規格。

總的來說，這取決於NuSMV爲什麼耗盡內存。大多數時候，它不會設法建立模型，這意味着您必須減少模型大小。爲此，您可能需要查看某些狀態變量是否可以成爲沒有狀態的布爾信號，或者如果您減少了某些變量的範圍。

如果您有參數化模型，例如，使用可變數量的模塊或某些變量的位寬可以更改，您可以嘗試獲得更簡單的變量以運行，然後找出哪個部分使內存需求增長。這部分應該以不同的方式建模。