如何 select UPPAAL 中的整数数组？

Question

我正在为 class 使用 uppaal，我想使用 select 语句创建范围内的整数数组。

作为背景，我正在模拟一个修改后的 nim 游戏，有 3 个玩家和 3 个堆，玩家可以从一个堆中选择最多 3 个匹配项，或者从所有堆中选择相同数量的匹配项（假设所有这些都剩下足够的火柴。）

到目前为止，我显然已经（根据验证者的一些基本查询）与 3 名玩家一起玩 nim 游戏，从一个堆中获取匹配项，但我需要扩展玩家以便能够从所有堆中获取并且我不希望对 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 数组更新堆。这样可以让玩家按照全套规则进行比赛。

如何 select UPPAAL 中的整数数组？

How to select array of integers in UPPAAL?

arrays

uppaal