如何限制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，这是一种减少所需内存量的非常快速的方法。