Отправить сообщение на множество каналов в недетерминированном порядке

Question

Я строю модель Promela, в которой один процесс отправляет запрос N другим процессам, ждет ответов и затем вычисляет значение. В основном типичный поток выполнения карты с уменьшением стилей. В настоящее время моя модель отправляет запросы в фиксированном порядке. Я хотел бы обобщить это, чтобы отправить недетерминированный заказ. Я посмотрел на select утверждение, но это, кажется, выбрать один элемент недетерминированно.

Есть ли хороший образец для достижения этой цели? Вот основная структура того, с чем я работаю:

#define NUM_OBJECTS 2
chan obj_req[NUM_OBJECTS] = [0] of { mtype, chan };

Это объектный процесс, который отвечает на msgtype сообщения с некоторым значением, которое он вычисляет.

proctype Object(chan request) {
  chan reply;

end:
  do
  :: request ? msgtype(reply) ->
    int value = 23
    reply ! value
  od;
}

Это клиент. Отправляет запрос каждому из объектов в порядке 0, 1, 2, ...и собирает все ответы и уменьшает значения.

proctype Client() {
  chan obj_reply = [0] of { int };
  int value

  // WOULD LIKE NON-DETERMINISM HERE
  for (i in obj_req) {
    obj_req[i] ! msgtype(obj_reply)
    obj_reply ? value
    // do something with value
  }
}

И я запускаю систему, как это

init {
  atomic {
    run Object(obj_req[0]);
    run Object(obj_req[1]);
    run Client();
  }
}

Answer 1

Из вашего вопроса я понимаю, что вы хотите назначить задачу данному процессу в случайном порядке, а не просто назначить случайную задачу упорядоченной последовательности процессов.

В общем, решение для обоих подходов очень похоже. Я не знаю, является ли тот, который я собираюсь предложить, наиболее элегантным подходом.

#define NUM_OBJECTS 10

mtype = { ASSIGN_TASK };
chan obj_req[NUM_OBJECTS] = [0] of { mtype, chan, int };

init
{
    byte i;
    for (i in obj_req) {
        run Object(i, obj_req[i]);
    }
    run Client();
};

proctype Client ()
{
    byte i, id;
    int value;
    byte map[NUM_OBJECTS];
    int data[NUM_OBJECTS];
    chan obj_reply = [NUM_OBJECTS] of { byte, int };

    d_step {
        for (i in obj_req) {
            map[i] = i;
        }
    }

    // scramble task assignment map
    for (i in obj_req) {
        byte j;
        select(j : 0 .. (NUM_OBJECTS - 1));
        byte tmp = map[i];
        map[i] = map[j];
        map[j] = tmp;
    }

    // assign tasks
    for (i in obj_req) {
        obj_req[map[i]] ! ASSIGN_TASK(obj_reply, data[i]);
    }

    // out-of-order wait of data
    for (i in obj_req) {
        obj_reply ? id(value);
        printf("Object[%d]: end!\n", id, value);
    }

    printf("client ends\n");
};


proctype Object(byte id; chan request)
{
  chan reply;
  int in_data;

end:
  do
    :: request ? ASSIGN_TASK(reply, in_data) ->
        printf("Object[%d]: start!\n", id)
        reply ! id(id)
  od;
};

Идея есть array который действует как map от набора индексов до начальной позиции (или, что то же самое, до назначенной задачи). map затем пробирается через конечное число swap операции. После этого каждый object параллельно назначается собственное задание, поэтому все они могут запускаться более или менее одновременно.

---

В следующем примере вывода вы можете увидеть это:

• Объектам назначается задача в случайном порядке
• Объекты могут выполнить задачу в другом случайном порядке

~$ spin test.pml
              Object[1]: start!
                                              Object[9]: start!
          Object[0]: start!
                                  Object[6]: start!
                  Object[2]: start!
                                          Object[8]: start!
                          Object[4]: start!
                              Object[5]: start!
                      Object[3]: start!
                                      Object[7]: start!
                                                  Object[1]: end!
                                                  Object[9]: end!
                                                  Object[0]: end!
                                                  Object[6]: end!
                                                  Object[2]: end!
                                                  Object[4]: end!
                                                  Object[8]: end!
                                                  Object[5]: end!
                                                  Object[3]: end!
                                                  Object[7]: end!
                                                  client ends
      timeout
#processes: 11
...

---

Если кто-то хочет назначить случайную задачу каждому object вместо случайного запуска их достаточно изменить:

        obj_req[map[i]] ! ASSIGN_TASK(obj_reply, data[i]);

в:

        obj_req[i] ! ASSIGN_TASK(obj_reply, data[map[i]]);

Очевидно, что data вначале следует инициализировать какой-либо значимый контент.