model-checking - 如何在 SPIN 中显示状态空间

Question

iSpin (v. 1.1.4) 中的“自动机视图”显示......究竟是什么？它似乎只是一个进程的控制流图。

我将如何获得系统的完整状态空间？

例如，在 Ben-Ari：自旋模型检查器的原理中，我想要图 4.1。或在Overview中，我想要图 1。

Answer 1

这本书提到（在附录 2 中）一个工具spinSpider，它是 jspin的一部分。我可以从源代码编译它，但没有成功运行它（错误消息没有帮助，本书没有解释用法）

无论如何， spinSpider 似乎已被Erigone中的 VMC 弃用。目前尚不清楚它是否具有相同的功能（绘制完整的状态图）。

我可以编译它但不能运行，因为 VMC 似乎是 Erigone 特有的，并且与 Spin 不兼容，例如它说“找不到文件 check.pml.trc” - 这是“.trail”文件吗？

Answer 2

生成的pan程序支持-d和-D命令行参数，它们分别以 ASCII 格式打印状态表。点。