类CSP同步

Question

我正在尝试使用类似于CSP的同步机制，但我不明白为什么以下模型的初始状态是死锁：

const int N = 2;
chan a;

process Processes(int [1,N] pid) {
    state A, B;
    init A;
    trans A -> B { sync a; };
}

system Processes;

在我看来，这两个进程是在通道'a‘上同步的，应该至少走一步，不是吗？

Answer 1

系统声明需要包含IO声明：

P1=Processes(1);
P2=Processes(2);

system P1, P2;

IO P1 {a}
IO P2 {a}

不幸的是，IO声明不理解模板参数，因此我使用了带有具体名称的完整实例化。

还有“适度”选项来启用不同的更新语义，例如：

x=y+z

使用y和z的旧值(同步前)，以防同时修改y和z。