Что вызывает тайм-аут в Promela/SPIN?

У меня есть следующий промел-код:

chan level = [0] of {int};

proctype Sensor (chan levelChan) {
    int x;
    do
    :: true ->
            levelChan ? x;
            if 
            :: (x < 2) -> printf("low %d", x);
            :: (x > 8) -> printf("high %d", x);
            :: else -> printf("normal %d", x);
            fi
    od
}

init {
    run Sensor(level);  
    int lvl = 5;
    level ! lvl;
    lvl = 0;
    do 
    :: true ->
        level ! lvl; 
        lvl++;
        (lvl > 9) -> break;
    od
}

Я ожидаю отправки информации об уровне (0-9) в канал и выход датчика низкий | нормальный | высокий в зависимости от этого уровня. Это довольно просто. Но почему SPIN все время говорит о тайм-ауте?

  0:    proc  - (:root:) creates proc  0 (:init:)
Starting Sensor with pid 1
  1:    proc  0 (:init:) creates proc  1 (Sensor)
  1:    proc  0 (:init:) 1.pml:18 (state 1) [(run Sensor(level))]
  2:    proc  1 (Sensor) 1.pml:6 (state 11) [(1)]
  3:    proc  0 (:init:) 1.pml:20 (state 2) [lvl = 5]
  4:    proc  0 (:init:) 1.pml:20 (state 3) [level!lvl]
  4:    proc  1 (Sensor) 1.pml:8 (state 2)  [levelChan?x]
  5:    proc  1 (Sensor) 1.pml:9 (state 9)  [else]
  6:    proc  0 (:init:) 1.pml:21 (state 4) [lvl = 0]
normal 5  8:    proc  1 (Sensor) 1.pml:12 (state 8) [printf('normal %d',x)]
  9:    proc  0 (:init:) 1.pml:22 (state 10)    [(1)]
 12:    proc  1 (Sensor) 1.pml:6 (state 11) [(1)]
 13:    proc  0 (:init:) 1.pml:24 (state 6) [level!lvl]
 13:    proc  1 (Sensor) 1.pml:8 (state 2)  [levelChan?x]
 14:    proc  1 (Sensor) 1.pml:9 (state 9)  [((x<2))]
low 0 15:   proc  1 (Sensor) 1.pml:10 (state 4) [printf('low %d',x)]
 17:    proc  0 (:init:) 1.pml:25 (state 7) [lvl = (lvl+1)]
 19:    proc  1 (Sensor) 1.pml:6 (state 11) [(1)]
timeout
#processes: 2
 19:    proc  1 (Sensor) 1.pml:8 (state 2)
 19:    proc  0 (:init:) 1.pml:26 (state 8)
2 processes created

Кажется, почему выполняется только 1 итерация цикла do?


verification promela spin
person Jiew Meng    schedule 03.02.2013    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Операторы в цикле do процесса init выполняются последовательно.

do 
:: true ->
    level ! lvl; 
    lvl++;
    (lvl > 9) -> break;
od

При первом запуске цикла do он отправит lvl по каналу level, увеличит lvl (теперь оно равно 1), а затем проверит (lvl > 9). Это неверно, поэтому будет заблокировано и вызовет тайм-аут.

Чтобы иметь несколько опций в цикле do, вам нужно :: определить начало каждой опции:

do
 :: true ->
    level ! lvl; 
    lvl++;
 :: (lvl > 9) -> break;
od

Однако это все равно не будет работать так, как ожидалось. Когда lvl больше 9, оба варианта цикла do действительны, и можно выбрать любой из них, поэтому цикл не обязательно прервется, когда lvl > 9 он может выбрать продолжение отправки lvl по каналу level и увеличение lvl.

У вас должно быть условие для первой опции do, а также для второй:

do 
:: (lvl <= 9) ->
    level ! lvl; 
    lvl++;
:: (lvl > 9) -> break;
od

Для этого примера лучше использовать синтаксис цикла for:

init {
  run Sensor(level);  
  int lvl = 5;
  level ! lvl;

  for (lvl : 0..9){
    level ! lvl; 
  }
}

Обратите внимание, что в этом примере по-прежнему будет ошибка тайм-аута, вызванная циклом do Sensor, когда процесс init завершится, Sensor все равно попытается прочитать из канала level и истечет время ожидания.

person Crux    schedule 15.02.2013