model-checking - UPPAALモジュロの例

Question

エッジのガードを次のように構成したいと思います。

(turn % 4) == me 

ここで、turnはクロック変数であり、meはプロセスを表すintです。

上記の述語をガードする方法の例を教えてください。

ありがとう、ケビン

Answer 1

私の回答は完全ではありません (そのため、完了としてマークしません)。

ただし、「クロック x」があり、クロックを n --> 0 からラップアラウンドさせたい場合は、このガードをエッジに追加します。

if (x == n) ? 0 : x