Promela моделирование с помощью Spin

Question

Я работаю над моделью Promela, которая довольно проста. Используя два разных модуля, он действует как пешеходный переход / светофор. Первый модуль - это светофор, который выводит текущий сигнал (зеленый, красный, желтый, в ожидании). Этот модуль также получает на вход сигнал, называемый "пешеход", который служит индикатором того, что пешеходы хотят пересечь дорогу. Второй модуль действует как пешеходный переход. Он получает выходные сигналы от модуля светофора (зеленый, желтый, зеленый). Он выводит пешеходный сигнал на модуль светофора. Этот модуль просто определяет, пересекает ли пешеход (ы), ждет или нет. Моя проблема в том, что как только значение счетчика становится равным 60, возникает тайм-аут. Я считаю, что утверждение "SigG_out! 1" вызывает ошибку, но я не знаю, почему. Я приложил изображение следа, который я получаю из командной строки. Я совершенно новичок в Spin и Promela, и поэтому я не уверен, как использовать информацию из трассировки, чтобы найти мою проблему в коде. Любая помощь с благодарностью.

Вот код для полной модели:

mtype = {red, green, yellow, pending, none, crossing, waiting};
mtype traffic_mode;
mtype crosswalk_mode;
int count;
chan pedestrian_chan = [0] of {byte};

chan sigR_chan = [0] of {byte};

chan sigG_chan = [0] of {byte};

chan sigY_chan = [0] of {byte};

ltl l1 {!<> (pedestrian_chan[0] == 1) && (traffic_mode == green || traffic_mode == yellow || traffic_mode == pending)}
ltl l2 {[]<> (pedestrian_chan[0] == 1) -> crosswalk_mode == crossing }

proctype traffic_controller(chan pedestrian_in, sigR_out, sigG_out, sigY_out)

{

do
    ::if
      ::(traffic_mode == red) -> 
        count = count + 1;
        if
        ::(count >= 60) ->
            sigG_out ! 1;
            count = 0;
            traffic_mode = green;
        :: else -> skip;
        fi
      ::(traffic_mode == green) -> 
        if
        ::(count < 60) ->
            count = count + 1;
        ::(pedestrian_in == 1 & count < 60) ->
            count = count + 1;
            traffic_mode = pending;
        ::(pedestrian_in == 1 & count >= 60)
            count = 0;
            traffic_mode = yellow;
        fi
      ::(traffic_mode == pending) ->
        count = count + 1;
        if
        ::(count >= 60) ->
            sigY_out ! 1;
            count = 0;
            traffic_mode = yellow;
        ::else -> skip;
        fi  
      ::(traffic_mode == yellow) ->
        count = count + 1;
        if
        ::(count >= 5) ->
            sigR_out ! 1;
            count = 0;
            traffic_mode = red;
        :: else -> skip;
        fi
      fi
od  

}



proctype crosswalk(chan sigR_in, sigG_in, sigY_in, pedestrian_out)

{
do
    ::if
      ::(crosswalk_mode == crossing) ->
        if
        ::(sigG_in == 1) -> crosswalk_mode = none;
        fi
      ::(crosswalk_mode == none) ->
        if  
        :: (1 == 1) -> crosswalk_mode = none
        :: (1 == 1) -> 
            pedestrian_out ! 1
            crosswalk_mode = waiting
        fi
      ::(crosswalk_mode == waiting) ->
        if
        ::(sigR_in == 1) -> crosswalk_mode = crossing;
        fi
      fi
od   
}


init

{

    count = 0;

    traffic_mode = red;

    crosswalk_mode = crossing;


    atomic
    {
        run traffic_controller(pedestrian_chan, sigR_chan, sigG_chan, sigY_chan);
        run crosswalk(sigR_chan, sigG_chan, sigY_chan, pedestrian_chan);
    }

}

Answer 1

Ты используешь channels неправильно, в частности, эту строку я даже не знаю, как ее интерпретировать:

:: (sigG_in == 1) ->

---

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

2. Чтобы читать с канала, вам нужно использовать правильный синтаксис:

   int some_var;
   ...
   some_channel?some_var;
   // here some_var contains value received through some_channel
   

---

Кажется бессмысленным использование трех разных каналов для передачи разных сигналов. Как насчет использования трех разных значений?

mtype = { RED, GREEN, YELLOW };
chan c = [0] of { mtype };
...
c!RED
...
// (some other process)
...
mtype var;
c?var;
// here var contains RED
...