【发布时间】：2014-03-15 13:12:19
【问题描述】：
我学习了 Promela 和 Spin，但是当我尝试验证模型时，这些行 退还给我。
它们是什么意思？
谢谢
【问题讨论】：
【发布时间】：2014-03-15 13:12:19
【问题描述】：
这意味着您运行了 Spin 验证并且您的验证发现了一个错误。下一步是确定错误是如何发生的。您可以通过生成和检查“跟踪文件”来做到这一点。
如果您按照以下方式执行验证：
$ spin -a model.pml
$ gcc -o pan pan.c
$ ./pan
然后使用 model.pml 文件检查轨迹：
$ spin -p -t model.pml
【讨论】：
-
经过检查，跟踪文件。我确实得到了失败的场景或失败的断言文本。接下来我该怎么办？
-
我的目标是为失败的场景生成测试用例？如何生成反例？
-
跟踪文件告诉您通过代码/模型产生违反正确性约束的确切路径。您可以通过一步一步仔细追踪它来理解这条路径。接下来做什么取决于你的目标——例如，如果你的模型是一个真实世界的系统，那么你可能发现了一个真实的、实际的问题。或者，也许您在模型中发现了错误；如果是，请修复模型并重新运行验证。有时验证可能会非常很大；查看
-i和-I的pan选项；它们有助于减小失败场景跟踪文件的大小。 -
好的，谢谢。我已经尝试并做了所有的事情。跟踪中的失败场景帮助我找到错误的位置。在那里找到相同的反例。以及如何为失败的场景自动生成测试用例的任何想法？
您的模型中可能存在死锁或其他错误。
如果您发布完整的控制台输出，我可能会更新此答案以提供更多信息！
【讨论】：