arraysuppaal

How to select array of integers in UPPAAL?


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. :-)


Solution

  • 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.