Uppaal 中来自同一个模板的多个进程的声明

问题描述

有没有办法在 Uppaal 中实例化从同一个模板获得的多个进程？

例如目前我写的（在 System declarations 文件中）：

// Template instantiations
P1 = Template(var1);
P2 = Template(var2);
P3 = Template(var3);
P4 = Template(var4);
// Processes into the system
system P1,P2,P3,P4;

但我想获得一个更紧凑的形式来这样做（也许是一个数组？），因为我实际上必须创建 50 个进程（不仅仅是 4 个）。我该怎么做？

注意：变量的类型为 int[0,1]，我目前在 Declarations 文件中定义它们如下：

int[0,1] var1,var2,var3,var4;

解决方法

是的，通过部分实例化，这里是一个例子：

const int N=50; // number of items
typedef int[1,N] id_t; // bounded integer type with values [1..N]
int[0,1] var[id_t]; // array of bounded integers indexed by id_t range [1..N]
P(const id_t id) = Template(var[id]); // template P with argument id
system P; // instantiate P(1)..P(N) by filling the constant values from id_t range

在最后一行，Uppaal 将自动填充常量整数参数，从而产生 N 个进程。

请注意，可以使用 bool 代替 int[0,1]。