如何限制PROMELA使用的內存？

我想通過使用-DMEMLIMIT標誌來限制PROMELA使用的最大內存，就像這樣。如何限制PROMELA使用的內存？

./spin -a -DMEMLIMIT=1024 code.pml

但是，仍然記憶力不斷增加。任何想法，爲什麼是這樣？

那'-DMEMLIMIT = 1024'標誌看起來像它可能是一個編譯器標誌，而不是你傳遞給程序的標誌。你有這個_spin_程序的任何文檔嗎？ – tangrs

實際上，自旋產生用於模型檢查的C代碼。該C代碼包含MEMLIMIT標誌，其目的是限制內存使用情況。但從我所看到的，記憶不受限制。 – MetallicPriest

我正在查看_spin_手冊，但沒有提及'-D'標誌。也許你打算用'-DMEMLIMIT = 1024'標誌來編譯生成的C文件？ – tangrs

-DMEMLIM = N是一個傳遞給gcc的編譯器標誌。它的工作原理是這樣：

./spin -a code.pml GCC -DMEMLIM = 1024 -o泛pan.c ./pan

您還可以添加更多的標誌強制執行狀態的更好的壓縮，例如-DCOLLAPSE，這是一種減少所需內存量的非常快速的方法。

2014-01-30 07:39:12 rindPHI

另外''-w'選項'pan'：「-wN 2^N條目的哈希表（默認爲-w24）」。 –

回答