modelpromelaspin

Promela randomly select two elements at the same time


Recently I started learning Promela and I want to model picking two balls from box where I have 10 black balls and 4 white balls, I can model box as array, but I have no idea how to select 2 balls at the same time. Picking one and then another one from those which are left changes probability. Do you have any ideas?


Solution

  • When you need to extract only a pair of values idx and idy from a contiguous interval [LOW, UPP] of N = UPP - LOW + 1 numbers, you can easily get around the problem of guaranteeing idx != idy by:

    that is, you interpret idy as a fixed displacement wrt. idx. Notice that this approach does not affect the probability distribution of idy and, in particular, it does not make idy dependent on idx from a probabilistic point of view.


    Example:

    #define BLACK_BALLS 4
    #define WHITE_BALLS 10
    #define TOTAL_BALLS 14
    
    bool box[TOTAL_BALLS];
    
    inline my_select(var, upper) {
        if
            ::  0 <= upper -> var =  0;
            ::  1 <= upper -> var =  1;
            ::  2 <= upper -> var =  2;
            ::  3 <= upper -> var =  3;
            ::  4 <= upper -> var =  4;
            ::  5 <= upper -> var =  5;
            ::  6 <= upper -> var =  6;
            ::  7 <= upper -> var =  7;
            ::  8 <= upper -> var =  8;
            ::  9 <= upper -> var =  9;
            :: 10 <= upper -> var = 10;
            :: 11 <= upper -> var = 11;
            :: 12 <= upper -> var = 12;
            :: 13 <= upper -> var = 13;
        fi;
    }
    
    proctype pick_two_balls() {
        byte idx;
        byte idy;
    
        my_select(idx, TOTAL_BALLS - 1);
        my_select(idy, TOTAL_BALLS - 2);
    
        printf("Initial picks:\n")
    
        printf("\tpicked %d in [0, %d]\n", idx, TOTAL_BALLS - 1);
        printf("\tpicked %d in [0, %d]\n", idy, TOTAL_BALLS - 2);
    
        idy = ((idx + 1) + idy) % (TOTAL_BALLS);
    
        printf("Adjusted picks:\n");
    
        printf("\tball #01 at index %d\n", idx);
        printf("\tball #02 at index %d\n", idy);
    
        printf("Final Balls:\n");
    
        if
            :: box[idx]  -> printf("\tbox[%d] = black\n", idx);
            :: !box[idx] -> printf("\tbox[%d] = white\n", idx);
        fi;
    
        if
            :: box[idy]  -> printf("\tbox[%d] = black\n", idy);
            :: !box[idy] -> printf("\tbox[%d] = white\n", idy);
        fi;
    }
    
    init {
        byte idx = 0;
        byte todo = BLACK_BALLS;
    
        do  // not guaranteed to terminate!
            :: todo > 0 ->
                my_select(idx, TOTAL_BALLS - 1) ->
                if
                    :: box[idx] ->
                        skip;
                    :: else ->
                        box[idx] = true;
                        todo = todo - 1;
                fi;
            :: else ->
                break;
        od;
    
        for (idx: 0 .. TOTAL_BALLS - 1) {
            if
                :: box[idx] ->
                    printf("box[%d] = black\n", idx);
                :: !box[idx] ->
                    printf("box[%d] = white\n", idx);
            fi;
        }
        run pick_two_balls();
    }
    

    Output:

    ~$ spin p.pml 
          box[0] = white
          box[1] = black
          box[2] = white
          box[3] = white
          box[4] = white
          box[5] = white
          box[6] = white
          box[7] = white
          box[8] = white
          box[9] = white
          box[10] = white
          box[11] = black
          box[12] = black
          box[13] = black
              Initial picks:
                picked 9 in [0, 13]
                picked 7 in [0, 12]
              Adjusted picks:
                ball #01 at index 9
                ball #02 at index 3
              Final Balls:
                box[9] = white
                box[3] = white
    2 processes created
    

    Note #1: in normal circumnstances, I would have used the select statement instead of writing my own my_select(var, upper) function. However, select does not guarantee that the value assigned to var is picked with a uniform distribution, and I thought this could be an issue for you.


    Note #2: when you need to extract more than a pair of indexes, the mathematical expression above is not helpful. However, you can apply the same principle in a mechanical sense: maintain used_indexes as a support array of bools, whereby location k is true if it is used by some index. Each time you pick a new index i, you start counting the empty cells from the beginning of the array, and decrease i by one. As soon as i = 0 you have the "real index" j that should be used in the original array, so you mark that location as used in used_indexes.