Promela:将数组传递给新的proctype
在Promela中，我需要从父进程传递一个数组到子进程，但是它不允许我这样做。而且，我在使这个数组成为全局数组时也有一些限制，所以也不能这样做。这是如何做到的呢？
例如：
proctype B(int hg)
{
..
}
proctype A()
{
int hg[n];
run B(hg);
}回答 1
Stack Overflow用户
发布于 2017-10-12 12:01:33
run的文档显示：
DESCRIPTION run操作符使用以前声明的proctype的名称作为参数，以及必须与该proctype的形式参数的数量和类型相匹配的实际参数的空列表。..。 如果proctype声明指定了非空形式参数列表，run运算符必须将实际参数值传递给新进程。只能将消息通道和基本数据类型的实例作为参数传递。不能传递变量数组。 重点是我的
您应该考虑使用全局变量。
在下面的示例中，我们将数组封装在http://spinroot.com/spin/Man/typedef.html中--连同进程可能需要的任何其他参数--并声明此类记录的全局向量。然后，我们不直接传递array参数，而是交换包含其他进程参数的记录的index。
#define m 10
#define n 10
typedef Record {
int hg[n];
// ...
// other parameters
// ...
};
Record data[m];
active proctype A ()
{
int idx = 1;
data[idx].hg[0] = 12;
// ...
run B(idx);
}
proctype B (int idx)
{
assert(data[idx].hg[0] == 12);
data[idx].hg[0] = 17;
// ...
}这将允许您生成一个验证器：
~$ spin -search -bfs test.pml
...
State-vector 424 byte, depth reached 6, errors: 0
...Alternatively，，而且只有在不需要生成验证器的情况下，您才可以简单地传递记录实例。(例如)
#define n 10
typedef Record {
int hg[n];
// ...
// other parameters
// ...
};
active proctype A ()
{
Record my_record;
my_record.hg[0] = 12;
// ...
run B(my_record);
}
proctype B (Record data)
{
assert(data.hg[0] == 12);
data.hg[0] = 17;
// ...
}但是，只有才能在模拟模式下工作，特别是它将使而不是允许您生成验证器：
~$ spin -search -bfs test.pml
spin: test.pml:18, Error: hidden array in parameter data事实上，typedef的文档明确提到
在run语句中也可以使用typedef对象作为参数，但在本例中，可能不包含任何数组。 重点是我的
https://stackoverflow.com/questions/46708169
复制相似问题
腾讯云开发者
Copyright © 2013 - 2026 Tencent Cloud. All Rights Reserved. 腾讯云 版权所有
深圳市腾讯计算机系统有限公司 ICP备案/许可证号：粤B2-20090059 
粤公网安备44030502008569号
腾讯云计算（北京）有限责任公司 京ICP证150476号 | 京ICP备11018762号