【发布时间】：2023-03-07 04:31:01
【问题描述】：
我想在检查模型时打印所有状态。当发生断言违规时，我们确实会得到一个跟踪文件，但即使没有断言违规，我也想查看状态。我该怎么做？
【问题讨论】：
-
这样做的动机是什么？确认模型“达到”某些点？
标签： multicore spin promela model-checking
【发布时间】：2023-03-07 04:31:01
【问题描述】：
一种选择是使用gcc 标志-DVERBOSE 编译pan 并观察验证运行的完整细节。当然，运行会花费一些时间并且会输出过多的输出，但是您会在访问所有状态时看到它们（格式不是很容易阅读，但可能足以满足您的目的）。
查看各个进程的状态图的另一个选项是
./pan -D | dot -Tps | ps2pdf - pan.pdf
这将创建一个多页 PDF，其中每一页都是一个进程（包括 never 声明）。
【讨论】：
-
答案的第二部分（每个进程图）可能不是 OP 想要的。