В SPIN/Promela, как правильно получить MSG из канала?

Я прочитал руководство по спину, но нет ответа на следующий вопрос:

У меня есть строка в моем коде следующим образом:

Ch?x

где Ch — это канал, а x — тип канала (для получения MSG). Что произойдет, если Ch пуст? будет ли он ждать прибытия MSG или нет? Нужно ли сначала проверять, не пуст ли Ch?

в основном все, что я хочу, это то, что если Ch пуст, подождите, пока не прибудет MSG, и когда он прибудет, продолжите...


promela spin
person Junior Fasco    schedule 16.06.2013    source источник

Ответы (2)


arrow_upward
1
arrow_downward

Да, текущий proctype будет заблокирован, пока сообщение не придет на Ch. Такое поведение описано в руководстве Promela под оператором receive. [Поскольку вы предоставляете переменную x (как в Ch?x), любое сообщение в Ch сделает оператор исполняемым. То есть аспект сопоставления с образцом receive не применяется.]

person GoZoner    schedule 18.06.2013

arrow_upward
2
arrow_downward

Итог: семантика Promela гарантирует желаемое поведение, а именно блокировку операции приема до тех пор, пока не будет получено сообщение.

На справочной странице получения

ВЫПОЛНЯЕМАЯ ВОЗМОЖНОСТЬ
Первая и третья формы оператора, записанные с одним вопросительным знаком, являются исполняемыми, если первое сообщение в канале соответствует шаблону из оператора получения.

Это сообщает вам, когда операция приема выполняется.

Затем семантика Promela объясняет, почему исполняемость имеет значение:

Пока есть исполняемые переходы (соответствующие базовым операторам Promela), механизм семантики выберет один из них случайным образом и выполнит его.

Конечно, цитата не делает это очень явным, но это означает, что оператор, который в настоящее время не является исполняемым, будет блокировать исполняемый процесс, пока он не станет исполняемым.


Вот небольшая программа, которая демонстрирует поведение операции приема.

chan ch = [1] of {byte};
  /* Must be a buffered channel. A non-buffered, i.e., rendezvous channel,
   * won't work, because it won't be possible to execute the atomic block
   * around ch ! 0 atomically since sending over a rendezvous channel blocks
   * as well.
   */

short n = -1;

proctype sender() {
  atomic  {
    ch ! 0;
    n = n + 1;
  }
}

proctype receiver() {
  atomic  {
    ch ? 0;
    n = -n;
  }
}

init {
  atomic {
    run sender();
    run receiver();
  }

  _nr_pr == 1;

  assert n == 0;
    /* Only true if both processes are executed and if sending happened
     * before receiving.
     */
}
person Malte Schwerhoff    schedule 17.06.2013