Gibt es eine Möglichkeit, eine maximale Zeit für jeden Zustand in UPPAAL global anzugeben?

Question

Ich möchte angeben, dass alle Zustand nicht länger als eine angegebene Zeit sein sollte. Ich kann es tun, indem ich es von Staat zu Staat benenne, aber der Mensch kann einen vergessen. Ich brauche eine globale Lösung. Ich meine etwas wie "maximale Zeit in jedem Staat" Eigenschaft.

Answer 1

Fügen Sie einfach einen weiteren Prozess mit einem einzigen Ort hinzu und legen Sie alle Ihre globalen Invarianten dort hin.

Sie können auch eine Reihe von Grenzen, beispiels haben:

Erklärungen:

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

invariant:

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