Как выбрать массив целых чисел в UPPAAL?

Question

Я использую Uppaal для класса, и я хотел бы создать массив целых чисел в пределах диапазона, используя оператор выбора.

Для фона я моделирую модифицированную игру nim с 3 игроками и 3 кучами, где игрок может выбрать до 3 матчей из одной кучи или выбрать одинаковое количество матчей из ВСЕХ куч (при условии, что достаточно во всех них осталось совпадений.)

До сих пор у меня, по-видимому, есть рабочая (согласно некоторым основным запросам для верификатора) игра nim с 3 игроками, берущая матчи из одной кучи, но мне нужно расширить игроков, чтобы иметь возможность брать из всех куч, и я предпочел бы не жестко закодировать переменные, такие как heap1Taken, heap1TakenAmount, heap2Taken, heap2TakenAmount и т. д.:-)

Answer 1

Я закончил тем, что создал массив int[0, MAX] beru[3]; и две функции, set_beru а также beru_init,

void set_beru(int[0, MAX]& beru[3], int[0, 2] index, int[1, MAX] value){
    for (i : int[0, 2]){
        if (i == index){
            beru[i] = value;
        } else {
            beru[i] = 0;
        }
    }
}

void beru_init(int[0, MAX]& beru[3], int[1, MAX] init_value){
    for (i : int[0, 2]){
        beru[i] = init_value;
    }
}

Игрок в игре имеет два возможных перехода от ready_to_play в playing, один из них выбирает индекс кучи и сумму, затем вызывает set_beruдругой выбирает сумму и звонит beru_init, У обоих из них есть охранники, которые, конечно, следят, чтобы ход был законным.

Когда игрок находится в playing состояние, он сигнализирует на канале, и игровое поле обновляет кучи, используя beru массив. Это позволяет игрокам играть в соответствии с полным набором правил.