uppaal - 有没有办法为 UPPAAL 全局中的每个状态指定最长时间？

Question

我想指定所有状态不应长于指定时间。我可以通过逐个州指定它来做到这一点，但人类可以忘记一个。我需要一个全球解决方案。我的意思是“每个州的最大时间”属性。

Answer 1

只需在一个位置再添加一个进程，然后将所有全局不变量放在那里。

您还可以有一个边界数组，例如：

声明：

typedef int[1,5] id_t;
clock c[id_t]; // clocks
const int b[id_t] = { 10, 20, 30, 40, 50 }; // bounds

不变的：

forall(i:id_t) c[i]<=b[i]