PROMELA/SPIN의 'any'채널에서 메시지를 수신하는 방법

Question

나는 Spin에서 알고리즘을 모델링하고 있습니다. 여러 채널이있는 프로세스가 있는데 어떤 시점에서 메시지가 올 것이지만 어떤 채널을 알지는 못합니다. 따라서 메시지가 어느 채널에서 나올 때까지 프로세스를 대기 (차단)하려고합니다. 내가 어떻게 할 수 있니?

Answer 1

Promela 's construct가 필요하다고 생각합니다 (http://spinroot.com/spin/Man/if.html 참조). (채널 아무도 그들에 아무것도없는 경우

이

byte var; 
if 
:: ch1?var -> skip 
:: ch2?var -> skip 
:: ch3?var -> skip 
fi 

은 다음 "선택이 전체 블록으로 구성"설명서를 인용 : 당신이 참조하고있는 과정에서

, 당신은 아마 다음과 같은 필요), 이는 정확히 원하는 행동입니다.

더 완벽 설명서의 관련 부분을 인용하면 "는 옵션 [:: 라인의 각이]의 가드 문이 실행 파일 만 실행을 선택할 수 있습니다 [가드 문은 부분은 이전 -> ] 하나 이상의 가드 명령문이 실행 가능한 경우, 그 중 하나는 비 결정적으로 선택되고, 가드가 실행 가능하지 않으면 전체 선택 사항 구성이 차단됩니다. "

덧붙여서, 위의 스핀에서는 구문을 점검하거나 시뮬레이트하지 않았습니다. 잘하면 그것은 옳다. 나는 Promela와 Spin에 새로운 경험을했습니다.

Answer 2

이 부분을 송신의 구현을 변경하고받을 필요없이 채널 변수의 번호를 가지고 싶다면, 다음과 같은 생산자 - 소비자 예제의 접근 사용할 수 있습니다 :

#define NUMCHAN 4 

chan channels[NUMCHAN]; 

init { 
    chan ch1 = [1] of { byte }; 
    chan ch2 = [1] of { byte }; 
    chan ch3 = [1] of { byte }; 
    chan ch4 = [1] of { byte }; 

    channels[0] = ch1; 
    channels[1] = ch2; 
    channels[2] = ch3; 
    channels[3] = ch4; 
    // Add further channels above, in 
    // accordance with NUMCHAN 

    // First let the producer write 
    // something, then start the consumer 
    run producer(); 
    atomic { _nr_pr == 1 -> 
     run consumer(); 
    } 
} 

proctype consumer() { 
    byte var, i; 
    chan theChan; 

    i = 0; 
    do 
     :: i == NUMCHAN -> break 
     :: else -> 
      theChan = channels[i]; 
      if 
       :: skip // non-deterministic skip 
       :: nempty(theChan) -> 
        theChan ? var; 
        printf("Read value %d from channel %d\n", var, i+1) 
      fi; 
      i++ 
    od 
} 

proctype producer() { 
    byte var, i; 
    chan theChan; 

    i = 0; 
    do 
     :: i == NUMCHAN -> break 
     :: else -> 
      theChan = channels[i]; 
      if 
       :: skip; 
       :: theChan ! 1; 
        printf("Write value 1 to channel %d\n", i+1) 
      fi; 
      i++ 
    od 
} 

do 루프 소비자 프로세스에서 비 결정적으로 0과 NUMCHAN-1 사이의 색인을 선택하고 읽을 채널이 있으면 해당 채널에서 읽습니다. 그렇지 않으면이 채널은 항상 건너 뜁니다. 당연히 Spin을 사용한 시뮬레이션 중에 채널 NUMCHAN에서 읽을 확률은 채널 0의 것보다 훨씬 작지만 가능한 모든 경로를 탐색하는 모델 검사에는 차이가 없습니다.