promela - 如何在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

结果如下图：过渡系统

spinspider是JSpin 发行版的一部分，尽管 JSpin 现在已被弃用，但它应该仍然可用。