我在使用PROMELA编写的代码时出现错误

Question

我正在使用ispin，并且出现错误提示自旋：在10个步骤之后结束并且转换失败。

如何防止发生此错误？

Answer 1

您防止错误两种方式之一发生：

1. 解决您的PROMELA模式 - 你有你的PROMELA需要被移除
2. 你发现一个错误的一个bug 您正在建模的系统。恭喜。您现在将错误报告给您正在建模的系统负责人。

在实践中，当你有一个线索指示错误，你接下来做

spin -p -t <name of the model>.pml 

将打印出步步模型执行导致的错误。你冲他们确认他们是正确的 - 如果是这样，见上面的＃2;如果不正确，请参阅＃1。在核查高级参数设置窗口

tab.I也增加物理内存为2048：

Answer 2

我有同样的问题，它是把-DVECTORSZ后固定。