spin - SPIN 中的格式验证

Question

我学习了 Promela 和 Spin，但是当我尝试验证模型时，这些行会返回给我。

他们的意思是什么？

谢谢

Answer 1

这意味着您运行了 Spin 验证并且您的验证发现了一个错误。下一步是确定错误是如何发生的。您可以通过生成和检查“跟踪文件”来做到这一点。

如果您执行验证为：

$ spin -a model.pml
$ gcc -o pan pan.c
$ ./pan

然后使用 model.pml 文件检查轨迹：

$ spin -p -t model.pml

Answer 2

您的模型中可能存在死锁或其他错误。

如果您发布完整的控制台输出，我可能会更新此答案以提供更多信息！