Как получить сообщение с любого канала в PROMELA / SPIN

Question

Я моделирую алгоритм в Spin.У меня есть процесс, который имеет несколько каналов, и в какой-то момент я знаю, что придет сообщение, но не знаю, с какого канала.Поэтому хочется дождаться (заблокировать) процесс, пока не придет сообщение с любого из каналов.как я могу это сделать?

Answer 1

Думаю, вам нужна конструкция Promela if (см. http://spinroot.com/spin/Man/if.html).

. В процессе, на который вы ссылаетесь, вам, вероятно, понадобится следующее:

byte var;
if
:: ch1?var -> skip
:: ch2?var -> skip
:: ch3?var -> skip
fi

Если ни один из каналовимейте что-нибудь на них, затем «конструкцию выбора как целые блоки» (цитируя руководство), что в точности соответствует желаемому поведению.

Чтобы процитировать соответствующую часть руководства более полно: «Опция [каждая из :: lines] может быть выбрана для выполнения только в том случае, если ее оператор охраны является исполняемым [оператор охраны является частью перед ->]. Если выполняется более одного оператора охраны, один из них будет выбран недетерминированно. Если ни один из охранников не является исполняемым, конструкция выбора целиком блокируется. "

Кстати, я не проверял синтаксис и не симулировал вышеизложенное в Spin. Надеюсь, это правильно. Я новичокк Промеле и самому Вращайся.

Answer 2

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

#define NUMCHAN 4

chan channels[NUMCHAN];

init {
    chan ch1 = [1] of { byte };
    chan ch2 = [1] of { byte };
    chan ch3 = [1] of { byte };
    chan ch4 = [1] of { byte };

    channels[0] = ch1;
    channels[1] = ch2;
    channels[2] = ch3;
    channels[3] = ch4;
    // Add further channels above, in
    // accordance with NUMCHAN

    // First let the producer write
    // something, then start the consumer
    run producer();
    atomic { _nr_pr == 1 ->
        run consumer();
    }
}

proctype consumer() {
    byte var, i;
    chan theChan;

    i = 0;
    do
        :: i == NUMCHAN -> break
        :: else ->
             theChan = channels[i];
             if
               :: skip // non-deterministic skip
               :: nempty(theChan) ->
                  theChan ? var;
                  printf("Read value %d from channel %d\n", var, i+1)
             fi;
             i++
    od
}

proctype producer() {
    byte var, i;
    chan theChan;

    i = 0;
    do
        :: i == NUMCHAN -> break
        :: else ->
             theChan = channels[i];
             if
               :: skip;
               :: theChan ! 1;
                  printf("Write value 1 to channel %d\n", i+1)
             fi;
             i++
    od
}

Цикл do в потребительском процессе недетерминированно выбирает индекс между 0 и NUMCHAN-1 и читает из соответствующего канала, если есть что прочитать, иначе этот канал всегда пропускается. Естественно, во время моделирования с помощью Spin вероятность чтения из канала NUMCHAN намного меньше, чем у канала 0, но это не имеет никакого значения при проверке модели, где исследуется любой возможный путь.