I am using uppaal for a class and I would like to create array of integers within range, using select statement.
For background, I am modelling a modified game of nim, with 3 players and 3 heaps, where a player can either pick up to 3 matches from a single heap, or pick the same number of matches from ALL the heaps (Assuming there is enough matches left in all of them.)
So far I have apparently working (according to some basic queries for the verifier) nim game with 3 players, taking matches from a single heap, but I need to extend the players to be able to take from all the heaps and I would prefer not to hardcode variables like heap1Taken, heap1TakenAmount, heap2Taken, heap2TakenAmount etc. :-)
I ended up creating an array int[0, MAX] beru[3];
and two functions, set_beru
and 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;
}
}
A player of the game then has two possible transitions from ready_to_play
to playing
, one of them selecting a heap index and an amount, then calling set_beru
, the other one selecting an amount and calling beru_init
. Both o them have the guards that make sure the move is legal of course.
When a player is in the playing
state, he signals on a channel and the game board updates the heaps using the beru
array. This allows the players to play according to the full set of rules.