c - 如何限制 PROMELA 使用的内存？

Question

我试图通过使用 -DMEMLIMIT 标志来限制 PROMELA 使用的最大内存，就像这样。

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

但是，内存仍在不断增加。任何想法，为什么会这样？

Answer 1

-DMEMLIM=N 是传递给 gcc 的编译器标志。它是这样工作的：

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

您还可以添加更多标志来强制更好地压缩状态，例如 -DCOLLAPSE 这是一种减少所需内存量的非常快速的方法。