Можно ли указать максимальное время для каждого состояния в UPPAAL global?

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]