multicore - 如何在 Promela/SPIN 中打印所有状态

Question

检查我的模型时，我想打印所有状态。当发生断言违规时，我们确实会得到一个跟踪文件，但即使没有断言违规，我也想查看状态。我怎样才能做到这一点？

Answer 1

一种选择是pan使用gcc标志编译-DVERBOSE并观察验证运行的全部细节。当然，运行会花费一些时间并且会产生过多的输出，但是您会在访问所有状态时看到它们（格式不是很容易阅读，但可能足以满足您的目的）。

查看各个进程的状态图的另一个选项是

./pan -D | dot -Tps | ps2pdf - pan.pdf

这将创建一个多页 PDF，其中每一页都是一个过程（包括never声明）。