promela - 模拟用 PROMELA 编写的代码时出错

Question

我正在使用 ispin 并收到错误说明 spin: trails end after 10 steps and transition failed.

如何防止此错误发生？

Answer 1

您可以通过以下两种方式之一防止错误发生：

1. 修复您的 Promela 模型 - 您的 Promela 中有一个需要删除的错误
2. 您在正在建模的系统中发现了一个错误。恭喜。您现在将错误报告给您正在建模的系统的负责人。

在实践中，当您有指示错误的线索时，您接下来执行

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

这将打印出导致错误的逐步模型执行。你仔细检查它们以确认它们是正确的 - 如果是这样，请参阅上面的＃2；如果不正确，请参阅#1。

Answer 2

我遇到了同样的问题，并且在放置后解决了-DVECTORSZ：

在验证选项卡的高级参数设置窗口中。我也将物理内存增加到了2048。