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