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] 

또한 경계의 배열, 예컨대을 가질 수 있습니다