Example extended with Clocks

We extend our previous example of the electronically controlled door with some clocks as follows (cf. figure 5.4):

Figure 5.4: Example Problem: electronically controlled door with clock x

1. If in state $1$ the keys $B$ or $C$ ar keyed in, the systems stays in state $1$
2. If in state $1$ the key $A$ is keyed in, then the system will evaluate whether the enabling condition/ the guard $x < 3$ is satisfied by the actual clock value. If this is the case, then the action $x := 0$ is realized and the system enters state $2$. Otherwise the system will not transit to state $2$ and it will not realize the action $x := 0$.
3. States 2 and 3 are to handle analogously to the case of state $1$.
4. If the system reaches state $4$ it stops because state $4$ is a final state.

This example shows for the transitions between states a label which can be described as a pattern having three 'compartements': an input part, an enabling part, and an action part.

The input part represents the input strings $s \in \Sigma^{*}$ representing events from the environment $ENV$. The enabling part represents conditions on clocks having the format $X_{i} \sim n$ or $X_{i} - X_{j} \sim m$ with $n,m \in \cal{N}$ and $\sim = \{=, <, >, \le, \ge\}$ and $X_{i}, X_{j} \in \cal{C}$ with $\cal{C}$ := set of clocks. The action part has expressions like $X_{i} := 0$ (or other actions).

The input and enabling parts are separated from the action part by a colon ':' . Thus we have input; enabling:action.