如何在Promela/SPIN中打印所有状态 [英] How to print all states in Promela/SPIN

问题描述

我想在检查模型时打印所有状态.当发生断言冲突时，我们确实获得了跟踪文件，但是即使没有断言冲突，我也想查看状态.我该怎么办?

I would like to print all states when checking my model. We do get a trail file when an assertion violation occurs but I want to see the states even when there are no assertion violations. How can I do that?

推荐答案

一个选项是使用gcc标志-DVERBOSE编译pan，并查看验证运行的全部详细信息.当然，运行需要一段时间，并且会吐出过多的输出，但是您会在访问它们时看到所有状态(格式不是很容易阅读，但可能足以满足您的目的).

One option is to compile pan with the gcc flag -DVERBOSE and watch the full details of the verification run. Of course the run will take a while and will spit excessive output, but you will see all the states as they are visited (the format is not very easy to read, but may sufficient for your purposes).

查看单个进程的状态图的另一种选择是

Another option to see the state graphs of individual processes is

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

这将创建一个多页PDF，其中每个页面都是一个过程(包括never声明).

This will create a multi-page PDF where each page is a process (including the never claim).

这篇关于如何在Promela/SPIN中打印所有状态的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！