modeling - UPPAAL で実装を設定する

Question

sプロセスがセットからランダムに要素を選択する必要があるモデルがありますS。選択部分は単一の操作です。UPPAAL で私が知っている唯一の同様のデータ構造は配列です。

UPPAAL には一定のデータ構造が存在しますか? そうでない場合は、どうすれば作成できますか?

Answer 1

セット S が有限で可算である場合は、有界整数型を使用してみてください。例えば：

const int N = 10; // size of the whole domain
typedef int[1,N] range_t; // range of possible elements: indexed 1..N
typedef int[0,N-1] crange_t; // C-programmers may prefer indexed 0..N-1
bool S[range_t]; // boolean array encoding of membership

次に、次のように S から任意の要素を選択してエッジを作成できます。

select: e:range_t
guard: S[e]
sync:  hey[e]!
update: chosen_one=e