I need to pass an array from parent process to child process in Promela but it is not allowing me to do so. Also, I have some constraints in making this array global, so can't do this also. How can this be done?
for e.g.:
proctype B(int hg)
{
..
}
proctype A()
{
int hg[n];
run B(hg);
}
The documentation of run
says that:
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]
You should consider using global variables instead.
In the following example, we enclose the array inside a user-defined structured data type --together with any other parameter which might be needed by the process--, and declare a global vector of such Records. Then, instead of directly passing around the array
argument, we exchange the index
of the Record containing the parameters for the other process.
#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;
// ...
}
This will allow you to generate a verifier:
~$ spin -search -bfs test.pml
...
State-vector 424 byte, depth reached 6, errors: 0
...
Alternatively, and only if you don't need to generate a verifier, you can simply pass-around your Record instance. e.g.
#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;
// ...
}
However, this only works in simulation mode and in particular it will not allow you to generate a verifier:
~$ spin -search -bfs test.pml
spin: test.pml:18, Error: hidden array in parameter data
In fact, the documentation of typedef
explicitly mentions that
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]