Мне нужно передать массив из родительского процесса в дочерний процесс в Promela, но он не позволяет мне это сделать. Кроме того, у меня есть некоторые ограничения в том, чтобы сделать этот массив глобальным, поэтому я не могу этого сделать. Как это может быть сделано?
например:
proctype B(int hg)
{
..
}
proctype A()
{
int hg[n];
run B(hg);
}
В документации run говорится, что:
ОПИСАНИЕ Оператор run принимает в качестве аргументов имя ранее объявленного proctype и, возможно, пустой список фактических параметров, которые должны совпадать с количеством и типами формальных параметров этого proctype. [...]
Оператор запуска должен передать фактические значения параметров новому процессу, если в объявлении proctype указан непустой список формальных параметров. В качестве параметров можно передавать только каналы сообщений и экземпляры базовых типов данных. Невозможно передавать массивы переменных.
[выделено мной]
Вместо этого вам следует рассмотреть возможность использования глобальных переменных.
В следующем примере мы заключаем массив в определяемый пользователем структурированный тип данных --вместе с любым другим параметром, который может понадобиться процессу--, и объявить глобальный вектор таких записей. Затем, вместо прямой передачи аргумента 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
...
В качестве альтернативы и только если вам не нужно создавать верификатор, вы можете просто передать свой экземпляр 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 также можно использовать в качестве параметра в операторе запуска, но в этом случае он не может содержать никаких массивов.
[выделено мной]
