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

可能，您的模型中有死锁或其他错误。

如果您想发布完整的控制台输出，我可能会更新这个答案，给您更多的信息！