UPPAAL模實施例

Question

我想的邊緣的保護配置爲：

(turn % 4) == me 

其中又是時鐘變量和我是代表一個進程的int。

請給我如何做一個後衛上述謂詞的例子。

感謝， 凱文

Answer 1

我的答案是沒有完全完成（所以我不會把它標記爲完成）。

但是，如果你有一個「時鐘X」，並希望時鐘從n個繞到 - > 0，則此守護添加到邊緣。

if (x == n) ? 0 : x