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.
In addition, stop-watches are supported and they are declared with invariants. Clock rate expressions are specified and they are part of the conjunction in the invariant. Furthermore, the forall construct is accepted in invariants to ease use of arrays.
Statistical model checker supports any integer expression as a clock rate which allows modeling costs.
The rate of exponential is a ratio expression which specifies the rate of exponential probability distribution. The rate expression can be a simple integer expression or two integer expressions separated by a colon like r:q where the rate is determined as ratio r/q.
The rate of exponential is used in a statistical model checking. If the location does not have an invariant over time, then it is assumed that the probability of leaving the location is distributed according to the exponential distribution: Pr(leaving after t)=1−e−λt, where e=2.718281828…, t is time and λ is the fixed rate. Probability density of the exponential distribution is λe−λt and thus intuitively λ means the probability density of leaving at time zero, i.e. as soon as some edge is enabled. The smaller the rate is specified, the longer the delay is preferred.
The generation of exact delay relies on pseudo random number generator and on 32-bit architectures the longest possible delay is rather limited: ln(231)/λ ≈ 21.49/λ.
The following are valid invariants. Here x and y are clocks and i is an integer array.
x <= 2x is less than or equal to 2.x < yx is (strictly) less than y.forall(i:int[0,2]) x[i] <= 3x[0], x[1] and x[2] of the clock array x are less or equal to 3.forall(i:int[0,2]) y[i]' == b[i]y[0]', y[1]', and y[2]' are set to, respectively, b[0], b[1] and b[2]. Note that for symbolic queries the only valid values are 0 and 1. Setting the rate to 0 effectively stops a clock (makes it a stop-watch). In statistical model checking the rate is allowed to be any floating point value. hybrid clock can be interpreted as a continuous cost and abstracted away in symbolic queries while maintaining concrete values in statistical queries.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:
x, that is reset on every incomming edge, andx <= 0 to the location.Like urgent locations, committed locations also 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.