PROMELA 프로세스에서 시간 초과/교착 상태없이 송수신하는 방법은 무엇입니까?

Question

PROMELA 문제로 머리를 감쌀 수 없습니다. 채널 ("to_pc")을 통해 메시지를 보내고받을 수있는 N 개의 프로세스 ("pc")가 있습니다. 각 프로세스에는 메시지를 수신하는 자체 채널이 있습니다. 프로세스가 수신하려면 들어오는 메시지의 채널을 확인하는 루프를 유지해야합니다. 두 번째 루프 옵션으로 프로세스는 다른 모든 채널에 메시지를 전송합니다.

그러나 시뮬레이션 모드에서는 항상 아무것도 보내지 않고 시간 초과가 발생합니다. 지금까지의 이론은 모든 프로세스가 즉시 보내려고하는 교착 상태를 만들었 기 때문에 (코드의 "보내기"부분에 갇혀 있기 때문에) 모두 수신하지 못하게되었습니다.

지금까지이 문제를 해결할 수 없었습니다. 전역 변수를 세마포 (semaphore)로 사용하여 송신을 금지하고 있으므로 한 채널 만 보낼 수 있습니다. 그러나 이로 인해 결과가 변경되지 않았습니다. 나의 유일한 다른 아이디어는 송신을위한 트리거로서 타임 아웃을 사용하는 것이지만, 이것은 나에게 옳은 것처럼 보이지 않는다.

아이디어가 있으십니까? 미리 감사드립니다!

#define N 4 

mtype={request,reply} 

typedef message { 
    mtype type; 
    byte target; 
    byte sender; 
}; 

chan to_pc[N] = [0] of {message} 

inline send() { 
    byte j = 0; 
    for (j : 0 .. N-1) { 
     if 
     :: j != address -> 
      to_pc[j]!msg; 
     :: else; 
     fi 
    } 
} 

active [N] proctype pc(){ 
    byte address = _pid; 
    message msg; 

    do 
    :: to_pc[address]?msg -> /* Here I am receiving a message. */ 
     if 
     ::msg.type == request-> 
      if 
      :: msg.target == address -> 
       d_step { 
        msg.target = msg.sender 
        msg.sender = address; 
        msg.type = reply; 
       } 
       send(); 
      :: else 
      fi 
     :: msg.type == reply; 
     :: else; 
     fi 
    :: /* Here I want to send a message! */ 
     d_step { 
      msg.target = (address + 1) % N; 
      msg.sender = address; 
      msg.type = request; 
     } 
     send(); 
    od 
}; 

Answer 1

당신이 원한다면 나는 당신의 소스 코드의 본격적인 작업 버전을 쓸 수 있지만, 아마도 그것은 하이라이트 당신이 다루고있는 문제의 원인에 충분하고 당신에게 하자 재미를 해결하고 있습니다.

---

분기 규칙 실행 상태에있는 분기가 취할 수

, 비 결정적
• 이 경우 실행 상태에 더 지점 없습니다 , else 브랜치 실행 조건 더 지점 및 전혀 다른 지점이없는 경우
• 을 촬영, 프로세스는

---

이

을 고려 조건 중 하나에 해당 될 때까지 중단

1: if 
2: :: in?stuff -> ... 
3: :: out!stuff -> ... 
4: fi 

여기서 in 및 out은 모두 동기 채널 (크기는 0)누군가가 다음 out의 다른 쪽 끝에서 out!stuff을입니다받는 경우

그런 다음

• 는 그렇지 않은 경우는
• 아닌 사람이, in의 다른 쪽 끝을 다음 in?stuff는 실행 가능에를 전송 경우 실행 불가능, 그렇지 않은 경우
• 프로세스 블록 라인 1:이 될 때까지 두 조건 중 적어도 하나가 실행 파일 일 때까지.

는 in 및 out 다시 동기 채널 (크기 0이다)이있다

1: if 
2: :: true -> in?stuff; ... 
3: :: true -> out!stuff; ... 
4: fi 

해당 코드를 비교.

그런 다음

• 두 가지
  가 실행 조건이 (true)는
• 프로세스가 즉시 중 하나 또는 에 의해, 뭔가를받을 보내 자체을 저지른 비 결정적으로 실행 선택 줄에있는 지점 2: 또는 3:
• 프로세스가 실행하지입니다 3: 다음 블록out!stuff 경우 in!stuff가 될 때 프로세스도, 선택하는 경우 out!stuff는
• 실행 될 때 in?stuff도, 실행하지입니다 그것은 블록 경우 다음 2:을 선택하는 경우 d_step { } 내의 모든 지침이 executable 당신을 때문에 실행

코드는, 후자의 상황에 빠진다 r 프로세스가 으로 커밋하면을 너무 일찍 보내십시오.

---

이을 정리해 : 위해 모델을 해결하기 위해, 당신이해야 리팩토링 모드와 viceversa에받을에이 에서 점프 항상 가능성이 있음을 보낼 수 있도록 코드. 힌트 : 해당 인라인 코드를 제거하고 실제 보내는에서 보내는 결정을 분리하십시오.