如何限制 PROMELA 使用的内存？答案

【问题标题】：How to limit the memory used by PROMELA?如何限制 PROMELA 使用的内存？
【发布时间】：2014-01-17 11:18:15
【问题描述】：

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

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

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

【问题讨论】：

-DMEMLIMIT=1024 标志看起来可能是编译器标志，而不是您传递给程序的标志。你有这个spin程序的文档吗？
实际上 SPIN 生成 C 代码用于模型检查。该 C 代码包含该 MEMLIMIT 标志，其目的是限制内存使用。但据我所见，内存并没有受到限制。
我正在查看 spin 的手册，但没有提到 -D 标志。也许您打算用-DMEMLIMIT=1024 标志编译生成的C 文件？
spinroot.com/spin/Man/Roadmap.html。实际上，如果您将标志与 spin 一起使用或在使用 gcc 编译时使用相同的东西。我都做了，结果是一样的。
您链接到的文档使用 MEMLIM 而不是 MEMLIMIT。

【解决方案1】：

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

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

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

【讨论】：