如何更改频道中消息的顺序

Question

我有这个代码需要修改，以便通道可以重新排序消息，我必须添加机制来处理这个

chan linkA = [10] of {byte};
chan linkB = [10] of {byte};
proctype sender ()
{ byte n;
do
:: n<10 -> linkA!n*n; n++;
linkB!n*n; n++
:: else -> break
od
}
proctype receiver (chan link)
{ byte m,i; byte result[5];
do
:: i<5 -> link?m -> result[i]=m; i++
:: else -> break
od
}
init
{
run sender ();
run receiver (linkA);
run receiver (linkB)
}

我创建的新流程重新排序有一个通道参数(链接C)在重新排序过程中，通道将接收两个变量(字节x)，表示数据字节，(字节s)表示结果的索引。因此，对接收器的通道声明已更改为接收{byte，byte}

此外，我更改了接收器进程

1   chan linkA = [10] of {byte , byte};
2   chan linkB = [10] of {byte, byte};
3   
4   proctype sender ()
5   { byte n;
6   do
7   :: n<10 -> linkA!!n*n; n++;
8              linkB!!n*n; n++
9   :: else -> break
10  od
11  }
12  proctype reorder (chan linkC)
13  {
14  byte x;
15  byte s;
16  end1:
17  do
18  :: linkC ? x,s -> linkC !x,s
19  od
20  }
21  proctype receiver (chan link)
22  { byte m,i; 
23  byte result[5];
24  byte from_proc;
25  do
26  :: i<5 -> link?from_proc,m -> result[i]=from_proc; i++
27  :: else -> break
28  od
29  }
30  init
31  {
32  run sender ();
33  run reorder (linkA);
34  run reorder (linkB);
35  run receiver (linkA);
36  run receiver (linkB)
37  }

为了应付重新订购，我补充道！！(分拣发送操作)

但代码并没有像我希望的那样工作，我不知道问题出在哪里。

Answer 1

您的解决方案存在的问题是，消息最初由sender按创建的确切顺序排序，这也对应于递增的值顺序。实际上，模型示例中的reorder过程并没有起到多大作用。它从队列中获取第一条消息，并将其放置在队列的末尾。如果队列包含k消息，则在k步骤之后，将根据初始顺序再次对消息进行排序。

我认为有三种可能的方法来处理这个问题：

• 直接以随机顺序生成消息，这样以后就不需要重新排序

• 在每条消息的第一个字段中放置一个随机生成的种子，并推迟receiver的执行，直到所有消息都在队列中，以便在使用排序发送时将消息随机放置在消息队列中

• 使用随机接收和eval(idx)，使receiver按随机顺序读取消息，即使队列中的消息已完全排序。这消除了receiver与sender同步的问题，但它要求receiver了解更多关于消息内容的信息，例如每个消息的idx。

---

采用上述第二种方法的解决方案如下：

chan linkA = [10] of {byte, byte};
chan linkB = [10] of {byte, byte};
bool synch = false;
proctype sender ()
{
byte i;
byte idx;
for (i : 0 .. 5) {
int n = 2*i;
select(idx:0..255);
printf("Sender: <%d, %d> to linkAn", idx, n*n);
linkA!!idx,n*n;
n = n + 1;
select(idx:0..255);
printf("Sender: <%d, %d> to linkBn", idx, n*n);
linkB!!idx,n*n;
}
synch = true;
}
proctype receiver (chan link)
{
byte i, idx;
byte result[6];
/* wait until all messages in the queue */
synch;
for (i : 0 .. 5) {
link?idx,result[i];
printf("Receiver(%d): <%d, %d>n", _pid, idx, result[i]);
}
}
init
{
run sender ();
run receiver (linkA);
run receiver (linkB)
}

输出为：

~$ spin test.pml 
Sender: <0, 0> to linkA
Sender: <3, 1> to linkB
Sender: <2, 4> to linkA
Sender: <1, 9> to linkB
Sender: <1, 16> to linkA
Sender: <0, 25> to linkB
Sender: <0, 36> to linkA
Sender: <0, 49> to linkB
Sender: <4, 64> to linkA
Sender: <2, 81> to linkB
Sender: <0, 100> to linkA
Sender: <0, 121> to linkB
Receiver(3): <0, 25>
Receiver(3): <0, 49>
Receiver(2): <0, 0>
Receiver(3): <0, 121>
Receiver(2): <0, 36>
Receiver(3): <1, 9>
Receiver(3): <2, 81>
Receiver(2): <0, 100>
Receiver(3): <3, 1>
Receiver(2): <1, 16>
Receiver(2): <2, 4>
Receiver(2): <4, 64>
4 processes created

请注意，idx是随机生成的，并且模型允许执行每个消息具有不同idx值的执行。