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 
...