Promela：将数组传递给新的 proctype

Question

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

例如：

proctype B(int hg)
{
 ..
}

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

Answer 1

run 的文档说：

DESCRIPTION The run operator takes as arguments the name of a previously declared proctype , and a possibly empty list of actual parameters that must match the number and types of the formal parameters of that proctype. [...]

The run operator must pass actual parameter values to the new process, if the proctype declaration specified a non-empty formal parameter list. Only message channels and instances of the basic data types can be passed as parameters. Arrays of variables cannot be passed.

[emphasis is mine]

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

在下面的示例中，我们将数组包含在 user-defined structured data type 中——连同进程可能需要的任何其他参数——，并声明此类记录的全局向量。然后，我们不直接传递 array 参数，而是交换包含其他进程参数的 Record 的 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
...

或者，并且仅当您不需要生成验证者时，您可以简单地传递您的记录实例。例如

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

A typedef object can also be used as a parameter in a run statement, but in this case it may not contain any arrays.

[emphasis is mine]

Promela：将数组传递给新的 proctype

Promela: passing array to new proctype

arrays

spin

promela