是否可以使用SPIN打印状态空间？

我想打印出计算出的状态空间，以便我可以进行可视化，然后手动探索它。那可能吗？是否可以使用SPIN打印状态空间？

我已经检查这样的标志作为-dcheck和-Dverbose，但我想，那些是不是我期待的...

从未使用过它，看起来Spin的这种变体内置了对您可能感兴趣的可视化类型的支持：https://code.google.com/p/erigone/ – Gian 2013-05-07 07:25:28

我想使可视化我自己出于某些原因，这就是为什么内置工具对我来说不是一个好选择。 – 2013-05-07 07:41:01

您正在寻找整个状态空间还是仅仅在特定执行点处的状态向量？你对状态矢量中的状态感兴趣，这些状态是SPIN内部的状态，例如每个事件类型的控制状态（如程序计数器）或者你定义的全局和本地状态？ – GoZoner 2013-05-10 02:27:53

无，目前有搜索到的状态空间的无图形输出在spin。可以使用graphviz dot绘制程序图，如here所述。

2014-09-16 01:32:46

回答