스핀을 이용한 Promela 모델링

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 크기로 선언했기 때문에 인 입니다. 다른 신호을 보낼 것 같다

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