如何在沒有超時/死鎖的情況下在PROMELA進程中發送和接收？

Question

我無法繞過這個PROMELA問題：我有N個進程（「pc」）可能通過通道（「to_pc」）發送和接收消息。每個進程都有自己的通道，通過它可以接收消息。 對於一個能夠接收的進程，我必須將它保存在一個循環中，該循環檢查傳入消息的通道。作爲第二個循環選項，該過程向所有其他渠道發送消息。

但是，在仿真模式下，這總是會導致超時，根本沒有發送任何內容。到目前爲止，我的理論是我創建了一個死鎖，所有進程都希望一次發送，導致它們都無法接收（因爲它們被卡在代碼的「發送」部分）。

到目前爲止，我一直無法解決這個問題。我曾嘗試使用全局變量作爲信號來「禁止」發送，因此只有一個通道可以發送。但是，這並沒有改變結果。我唯一的想法是使用超時作爲發送的觸發器，但這對我來說似乎並不正確。

任何想法？提前致謝！

#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

我可以寫你的源代碼一個全面工作版本，如果你想要的，但也許就足夠了亮點你正在處理的問題的根源，讓你玩得開心解決它。

---

分支規則

• 與可執行條件的任何分支可以採取，非確定性
• 如果沒有分支與可執行條件，其他分支取
• 如果沒有分支與可執行條件和沒有別的分支，那麼該過程將掛起時的條件之一爲真，直到

---

考慮這個

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

其中in和out都是同步通道（尺寸爲0）。

然後

• 如果有人上的in另一端則in?stuff是可執行的發送，否則就不是
• 如果有人上的out另一端接收然後out!stuff被否則它不是
• 該過程塊在線1:直到兩個條件中至少有一個是可執行文件。

該代碼比較此

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

in哪裏和out再次是同步通道（大小爲0）。

然後

• 兩個分支有可執行條件（true）
• 過程立即致力於要麼發送或收到東西，非確定性地選擇執行在線2:或3:的分支
• 如果進程選擇2:那麼塊如果in?stuff是不可執行，即使out!stuff將可執行
• 如果進程選擇3:那麼塊如果out!stuff是不可執行，即使in!stuff會可執行

您的代碼落在後一種情況下，由於內d_step { }所有的指令都是executable你r進程提交到發送方式太早。

---

綜上所述：爲了解決您的模型，您應該重構你的代碼，以便它總是能夠跳從發送到接收模式，反之亦然。 提示：擺脫那個內聯代碼，分開實際發送的決定。