uppaal - 类似 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”上是同步的，应该至少迈出一步，不是吗？

score 1 · Accepted Answer

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

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

system P1, P2;

IO P1 {a}
IO P2 {a}

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

还有“Modest”选项可以启用不同的更新语义，例如：

x=y+z

y使用and的旧值z（在同步之前）以防y和z被同时修改。

1 回答 1