スピンを使ったプロメラモデリング

Question

私はかなり簡単なプロメラモデルで作業しています。 2つの異なるモジュールを使用して、横断歩道/交通信号機として機能します。最初のモジュールは、現在の信号（緑色、赤色、黄色、保留中）を出力する信号灯です。このモジュールはまた、「歩行者」と呼ばれる信号を入力として受け取り、これは交差する歩行者があることを示す指標となる。第2のモジュールは横断歩道として機能する。信号機モジュールからの出力信号（緑、黄、緑）を受信します。歩行者信号を信号機モジュールに出力する。このモジュールは、歩行者が横断しているのか、待っているのか、存在していないのかを単に定義します。私の問題は、カウント値が60になると、タイムアウトが発生するということです。 "SigG_out！1"というステートメントはエラーを引き起こしていると思いますが、理由はわかりません。コマンドラインから受け取ったトレースのイメージを添付しました。私はSpinとPromelaについて全く新しいので、コード内で私の問題を見つけるために情報フォームをどのように使用するのか分かりません。どんな助けでも大歓迎です。ここで

は完全なモデルのコードです：あなたは間違ってchannelsを使用している

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

、特にこの行は、私もそれをどのように解釈するかを知ることはできません。

:: (sigG_in == 1) -> 

---

1. の

   あなたのチャンネルは、いつでもプロセスは、片側にメッセージを配信するために、チャンネルのもう一方の端にを聞く必要があります別のプロセスを何かを送ることを意味し、同期です。それ以外の場合は、状況が変わるまでプロセスはをブロックします。 のチャネルは、0と宣言したので、という同期です。チャネルからの読み取りに

2. 、あなたは正しい構文を使用する必要があります。

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

---

を別の信号を送信するために3つの異なるチャネルを使用するように少し無意味であるように思わ 。 3つの異なる値を使うのはどうですか？

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