- UPPAAL Help
Locations of a timed automaton are graphically represented as circles. If a timed automaton is considered as a directed graph, then locations represent the vertices of this graph. Locations are connected by edges.
Locations can have an optional name. Besides serving as an identifier allowing you to refer to the location from the requirement specification language, named locations are useful when documenting the model. The name must be a valid identifier and location names share the name space with variables, types, templates, etc.
Locations are labelled with invariants. Invariants are expressions and thus follow the abstract syntax of expressions. However, the type checker restricts the set of possible expressions allowed in invariants.
An invariant must be a conjunction of simple conditions on clocks, differences between clocks, and boolean expressions not involving clocks. The bound must be given by an integer expression. Furthermore lower bounds on clocks are disallowed. It is important to understand that invariants influence the behaviour of the system -- they are distinctly different from specifying safety properties in the requirements specification language. States which violate the invariants are undefined; by definition, such states do not exist. This influences the interpretation of urgent channels and broadcast channels. Please see the section on synchronisations for a detailed discussion of this topic.
The following are valid invariants. Here x and y are clocks and i is an integer array.
- x <= 2
x is less than or equal to 2.
- x < y
x is (strictly) less than y.
- (i+1) != (i*10)
Each template must have exactly one initial location. The initial location is marked by a double circle.
Urgent locations freeze time; i.e. time is not allowed to pass when a process is in an urgent location.
Semantically, urgent locations are equivalent to:
- adding an extra clock, x, that is reset on every incomming edge, and
- adding an invariant x <= 0 to the location.
Like urgent locations, committed locations freeze time. Furthermore, if any process is in a committed location, the next transition must involve an edge from one of the committed locations.
Committed locations are useful for creating atomic sequences and for encoding synchronization between more than two components. Notice that if several processes are in a committed location at the same time, then they will interleave.