如何在promela中绘制过渡系统？

Question

我是promela的新手。我有一个用promela写的程序：

bit signal [2];
active [2] proctype proc() {
l1: signal[_pid]=1;
l2: !signal[1-_pid] -> 
l3: signal[_pid]=0;
}
#define sig0 (signal[0]==0)
#define sig1 (signal[0]==1)

有人知道怎么画这个程序的过渡系统吗？

Answer 1

你必须计算你的promela模型的所有可能的交错。在您的示例中，有两个活动进程，因此这仍然是可行的；但是，您仍然可以看到20个节点的图像。为了获得一些灵感，我建议使用spinspider工具：

spinspider -p2 -vsignal[0] -vsignal[1] yourProgram.pml

结果如下图所示：Transition System

spinspider是JSpin distribution的一部分，尽管JSpin现在已经被弃用，但它应该仍然可以使用。