timeout - タイムアウト/デッドロックなしで PROMELA プロセスで送受信する方法は?

Question

この PROMELA の問題に頭を悩ませることはできません。チャネル ("to_pc") を介してメッセージを送受信できる N 個のプロセス ("pc") があります。各プロセスには、メッセージを受信するための独自のチャネルがあります。プロセスが受信できるようにするには、受信メッセージのチャネルをチェックするループにプロセスを保持する必要があります。2 番目のループ オプションとして、プロセスは他のすべてのチャネルにメッセージを送信します。

ただし、シミュレーション モードでは、何も送信されずに常にタイムアウトが発生します。これまでの私の理論では、すべてのプロセスが一度に送信しようとするデッドロックが発生し、すべてのプロセスが受信できなくなりました (コードの「送信」部分でスタックしているため)。

これまでのところ、この問題を解決できませんでした。グローバル変数をセマフォとして使用して送信を「禁止」し、1 つのチャネルのみが送信できるようにしました。しかし、これは結果を変えませんでした。私の他の唯一のアイデアは、タイムアウトを送信のトリガーとして使用することですが、これは私にはまったく正しくないようです。

何か案は？前もって感謝します！

#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
};