如何在没有超时/死锁的情况下在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
};