model-checking - 如何更改频道中消息的顺序?
问题描述
我有这个代码需要修改,以便频道可以重新排序消息,我必须添加机制来应对这个
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)
}
我创建的新进程重新排序有一个通道参数(linkC) 在重新排序过程中,通道将接收两个变量(字节 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 }
为了应对重新排序,我补充说!(排序发送操作)
但是代码不能按我的意愿工作,我不知道问题出在哪里。
解决方案
您的解决方案有一个问题,即消息最初sender
按其创建的确切顺序排序,这也对应于递增的值顺序。实际上,模型示例中的reorder
过程并没有多大作用。它从队列中取出第一条消息,并将其放在队列的末尾。如果队列包含k
消息,则在k
步骤之后,消息将根据初始顺序再次排序。
我看到了三种可能的方法来处理这个问题:
直接按随机顺序生成消息,这样以后就不需要重新排序了
在每条消息的第一个字段中放置一个随机生成的种子,并将执行推迟到所有消息都在队列中时,以便在使用排序发送
receiver
时将消息随机放入消息队列中使用random receive和
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 linkA\n", idx, n*n);
linkA!!idx,n*n;
n = n + 1;
select(idx:0..255);
printf("Sender: <%d, %d> to linkB\n", 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
值。
推荐阅读
- python - 在 Python 中从 PDF 中提取文本时出现 UnicodeEncodeError
- html - ejs编译错误
- html - 如何在 Bootstrap 4 中将此表单居中?
- etl - CDC 映射的实现不是使用映射变量。
- java - 通过从 JAVA 开始的 C++ 应用程序运行 Shell 脚本
- javascript - 反应 onClick 属性未呈现
- webgl-globe - 更改 WebGL Earth Globe 的颜色?
- ios - 错误:表达式解析为未使用的函数(带闭包的数组)
- mysql - 我应该包括什么来防止 MYSQL 中显示的弹出错误?
- ruby-on-rails - 我可以在我的路由中自定义 `resources` 助手以使用 \:id 以外的参数吗?