arrays - Promela：将数组传递给新的proctype

Question

我需要在Promela中将一个数组从父进程传递给子进程，但它不允许我这样做。另外，我在使这个数组全局化方面有一些限制，所以也不能这样做。如何才能做到这一点？

例如：

proctype B(int hg)
{
 ..
}

proctype A()
{
    int hg[n];
    run B(hg);
}

Answer 1

的文档run说：

描述 run 运算符将先前声明的 proctype 的名称和一个可能为空的实际参数列表作为参数，该列表必须与该 proctype 的形式参数的数量和类型相匹配。[...]

如果 proctype 声明指定了非空的形式参数列表，则 run 运算符必须将实际参数值传递给新进程。只有消息通道和基本数据类型的实例可以作为参数传递。 不能传递变量数组。

[重点是我的]

---

您应该考虑改用全局变量。

在下面的示例中，我们将数组包含在用户定义的结构化数据类型 中——连同进程可能需要的任何其他参数——并声明此类Records的全局向量。然后，我们不是直接传递参数，而是将包含参数的Record交换给另一个进程。arrayindex

#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
...

---

或者，只有当您不需要生成验证器时，您才可以简单地传递您的Record实例。例如

#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明确提到

typedef 对象也可以用作 run 语句中的参数，但在这种情况下，它可能不包含任何数组。

[重点是我的]