Промела случайным образом выбирает два элемента одновременно - PullRequest
Новая
       68

Промела случайным образом выбирает два элемента одновременно

0 голосов
/ 26 февраля 2019

Недавно я начал изучать Promela и хочу смоделировать выбор двух шаров из коробки, в которой у меня есть 10 черных и 4 белых шара, я могу смоделировать коробку как массив, но я не знаю, как выбрать 2 шара одновременно,Выбор одного, а затем другого из тех, которые остались, изменяет вероятность.У вас есть идеи?

1 Ответ

0 голосов
/ 27 февраля 2019

Когда вам нужно извлечь только пару значений idx и idy из непрерывного интервала [LOW, UPP] из N = UPP - LOW + 1 чисел, вы можете легко обойти проблему гарантирования idx != idy по:

  • выбор idx в [LOW, UPP]
  • выбор idy в [LOW, UPP - 1]

  • регулировка значения idyWRT.значение idx выглядит следующим образом: 

    idy = LOW + (((idx - LOW) + 1 + (idy - LOW)) % N)

, то есть вы интерпретируете idy как фиксированное смещение относительно.idx.Обратите внимание, что этот подход не влияет на распределение вероятностей idy и, в частности, он не делает idy зависимым от idx с вероятностной точки зрения.

Пример: 

#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();
}

Вывод: 

~$ 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

Примечание № 1: при обычных обстоятельствах я быЯ использовал оператор select вместо того, чтобы писать свою собственную функцию my_select(var, upper).Однако select не гарантирует, что значение, присвоенное var, будет выбрано с равномерным распределением , и я подумал, что это может быть проблемой для вас.

Примечание # 2: когда вам нужно извлечь больше пары индексов, приведенное выше математическое выражение не поможет.Тем не менее, вы можете применить тот же принцип в механическом смысле: поддерживать used_indexes в качестве вспомогательного массива bools, причем расположение k равно true, если оно используется каким-либо индексом.Каждый раз, когда вы выбираете новый индекс i, вы начинаете считать пустые ячейки с начала массива и уменьшаете i на единицу.Как только i = 0 у вас есть "реальный индекс" j, который должен использоваться в исходном массиве, вы помечаете это местоположение как используемое в used_indexes.

...