0

有没有办法实例化从 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;
4

1 回答 1

1

是的,通过部分实例化,这里有一个例子:

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

于 2021-07-14T15:45:53.863 回答