Version:
v6.0
[release notes]

# Module 5.5: The 'tau' event

So far, all edges had events on them, and these events were explicitly declared in the model. This is an important aspect of discrete models, where events play a key role in automaton interaction. It is also mandatory when the model is used for supervisory controller synthesis, as we need to indicate for each event whether it is controllable or uncontrollable.

But, we don't always care what event is on an edge. Especially when making hybrid models, it is not always relevant. We may just want to wait for some time and then we go to the next location. In these cases, the event of such an edge is local, doesn't synchronize with any other automaton, and is used on only one edge.

For such occasions, the `tau` event is available. This event is implicitly always present in every CIF model, and therefore doesn't have to be declared. The `tau` event is not controllable, nor uncontrollable, and it does not synchronize with any event, not even with other uses of the `tau` event.

To use the `tau` event, either specify it explicitly as the event of the edge, or just leave out the event on the edge, such that it is implicitly uses the `tau` event.

## Example

As an example, consider again the stopwatch model from earlier in the module. We can leave out `time_passed` event, and use the `tau` event implicitly:

                                automaton Stopwatch:
                                    location Zero:
                                        initial;
                                        edge when time >= 60  goto One;

                                    location One:
                                        edge when time >= 120 goto Two;

                                    location Two:
                                        edge when time >= 180 goto Three;

                                    location Three:
                                        urgent;
                                end

## Quiz

[ { type: 'multiple-choice', question: "Which of the following statements is true?", answers: [ "The `tau` event is declared as any other event.", "Two automata with `tau` edges can only take their edges together, as they must synchronize.", "There are no declarations for `tau` events, since the event is implicitly always present.", "The `tau` can't be used in plant and requirement models for synthesis, since the event is neither controllable nor uncontrollable.", ], correctAnswer: '3, 4' } ];