1

我无法解决这个 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
};
4

1 回答 1

0

如果您愿意，我可以为您的源代码编写一个完整的工作版本，但也许它足以突出您正在处理的问题的根源并让您享受解决它的乐趣。

分支规则

  • 任何具有可执行条件的分支都可以被非确定性地采用
  • 如果没有具有可执行条件的分支，则采用else分支
  • 如果没有具有可执行条件的分支且没有 else分支，则进程挂起，直到其中一个条件为真

考虑这个

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

其中in和out都是同步通道（大小为0）。

然后

  • 如果有人在另一端发送inthenin?stuff是可执行的，否则不是
  • 如果有人在另一端接收outthenout!stuff是可执行的，否则不是
  • 进程在队列中阻塞1:，直到两个条件中的至少一个是可执行的。

将该代码与此进行比较

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

其中in和out再次是同步通道（大小为0）。

然后

  • 两个分支都有一个可执行条件 ( true)
  • 该过程立即通过不确定地选择在line或2:3:
  • 如果进程选择2:然后它阻塞如果in?stuff不可执行，即使out!stuff是可执行的
  • 如果进程选择3:然后它阻塞如果out!stuff不可执行，即使in!stuff是可执行的

您的代码属于后一种情况，因为其中的所有指令d_step { }都是可执行的，并且您的进程提交太早发送。

总结一下：为了修复您的模型，您应该重构代码，以便始终可以从发送模式跳转到接收模式，反之亦然。提示：摆脱那些内联代码，将发送的决定与实际发送分开。

于 2017-01-24T09:19:06.737 回答