Version: [release notes]

Module 5.4: Urgency

We now have timed models, which make use of variable time or continuous variables. And we have hybrid models that combine these timing aspects with discrete events. Hybrid models thus combine discrete event behavior and timed behavior. The behavior of a system then consists of both discrete transitions for events (event transitions) and the passage of time (time transitions). But, this begs the question: which of these takes priority?

That is determined by urgency. CIF has event urgency and location urgency. There is also edge urgency, but we recommend not using it, so it is not discussed in this course. Event urgency was briefly mentioned earlier in the module, and we'll revisit it here in more detail. After that, we'll look at location urgency.

Event urgency

Earlier in this module, the concept of urgency, and in particular event urgency, was already mentioned. In CIF, transitions for events take priority over passage of time. Thus, if any event is enabled and a transition can be taken for it, time will not pass and the event transition will be taken instead. If then another event is enabled, a transition is taken for it as well, and so on. Only once no event is enabled anymore, and thus no event transitions can be taken, will time start to pass. And while time is passing, as soon as another event becomes enabled, time passage will stop and the event transition will be taken. This is why a guard time >= 10 still ensures that a transition can take place at the moment that time has reached value 10 (or very soon thereafter).

Location urgency

Besides event urgency, there is also location urgency. Think back to the stopwatch example from earlier in the module. Its state space was as follows:

Once the automaton reaches location Three, time can progress infinitely. To prevent time from progressing, the location can be made urgent. Just like events being urgent prevents passage of time if they are enabled, being in an urgent location also prevents passage of time. That is, if any automaton is an urgent location, time may not pass. Note that you need only one automaton to be in an urgent location to prevent passage of time. That is different from marked locations, where all automata must be in a marked location, in order to reach a marked state for the (entire) system.

The CIF model of the stopwatch can be adapted as follows, to make the location urgent:

                        
                            automaton Stopwatch:
                                event time_passed;

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

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

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

                                location Three:
                                    urgent;
                            end
                        
                    

Location Three is specified as being urgent, similar to how locations can be marked. Time may not progress while that location is the current location of the automaton. This changes the state space of the model, which is then:

Deadlock and livelock

In a discrete event model, a state is a deadlock state if no events are enabled and thus no event transitions are possible. In a hybrid model, a state is a deadlock if no event transitions are possible, but also no time transitions are possible (time may not pass). We're then stuck in the state and can't leave it.

You may also recall that in a discrete event model, a state is a livelock state if progress is possible by taking event transitions, but never a marked state can be reached. In other words, it is a blocking state that is not a deadlock state. Progress can be made, but it does not lead to the desired result of reaching a marked state. In a hybrid model, we may additionally have a timed livelock if event transitions are always possible and thus time may never progress. Progress can then still be made by event transitions, but this does not lead to ever allowing the passage of time again.

Consider for instance the following CIF model, which has a timed livelock:

                        
                            automaton WaterLevel:
                                event rise, drop;
                                cont level der velocity;
                                disc real velocity = 0;

                                location:
                                    initial;
                                    marked;
                                    edge rise when level <= 0 do velocity := velocity + 0.2;
                                    edge drop when level >= 3 do velocity := velocity - 0.2;
                            end
                        
                    

This models the water level, for instance the water in the chamber of a water lock. The water level may rise and drop, depending on the current water level. That is, if the water level drops to zero, it rises (again). And if it rises above 3 meters, it drops (again).

At least, that is the idea. Initially, the water level is zero. The edge for event rise is then enabled, and the velocity can be increased. However, the edge remains enabled and the velocity can be increased again. And again, and again, and again. The event remains enabled, and velocity keeps increasing towards infinity. But, as time may never pass, the level never actually raises above 0. And thus the drop event is never enabled. The model thus has a timed livelock.

And there are more such situations where event urgency can lead to undesired effects. Consider for instance a button that may be pressed and released by a user. If we don't constrain the two events, and allow them to alternatingly occur one after the other, then time may never progress. We don't know when the user presses or releases the button, so we can't specify the time after which the button press and release events become enabled. And we don't even want to specify it, as we want the user to be able to press and release the button at any time.

Event urgency in practice

We thus want to allow certain events to happen at any time, but without specifying the time at which they may occur we have a timed livelock. So, how do we solve this then?

In essence, since in the model we want to leave it open when the events occur, this must be decided somewhere else. The model allows an event to happen at any time, but something else decides when it actually does occur. We call this an open model. Often, this moment when for instance a user presses the button, is decided by a person. In CIF, we do not model this. Instead, we consider it part of the environment of the model. The exact times at which certain events occur is something that then becomes known only when the model is put together with its environment. For instance, it may become known when we simulate a model and make explicit choices ourselves, or when we implement a controller in an actual system and connect it to a physical button that a user can press.

In a way, certain events may then have additional conditions that are imposed by the environment. You could see this as the environment being another model, that has automata that also synchronize over these events, and impose additional conditions through their own guards. When the open model is put together with its environment, the events get additional constraints, making it a closed model. In practice however, the environment is typically not modeled, but something else acts as the environment. As already mentioned, examples of practical environments are an actual physical system or a simulator.

One typical use case for this is when we simulate a model and connect some of the events to SVG input mappings. Then the click on an element of the image leads to an event becoming enabled. That way, the image is the environment, and a click determines the actual moment that the corresponding event occurs.

Quiz

[ { type: 'single-choice', question: "Which of the following statements is true?", answers: [ "If no events are enabled, time may always progress.", "If some events are enabled and others are not, time may progress.", "If any event is enabled, time may not progress.", "If all events are enabled, time may progress.", "If no events are enabled, time may not progress.", ], correctAnswer: '3' }, { type: 'single-choice', question: "Which of the following statements is true?", answers: [ "If all automata are in urgent locations, time may progress.", "If no automaton is in an urgent location, time may always progress.", "If none of the automata are in an urgent location, time may not progress.", "If any automaton is in an urgent location, time may not progress.", "If some automata are in urgent locations and others are not, time may progress.", ], correctAnswer: '4' }, { type: 'single-choice', question: "Is it true that time may only progress if no events are enabled and none of the automata is in an urgent location?", answers: [ "Yes.", "No.", ], correctAnswer: '1' }, { type: 'multiple-choice', question: "Which of the following statements are true for the original version of the stopwatch mentioned above?", answers: [ "It has a deadlock.", "It has no deadlock.", "It has a timed livelock.", "It has no timed livelock.", ], correctAnswer: '2, 4' }, { type: 'multiple-choice', question: "Which of the following statements are true for the adapted version of the stopwatch mentioned above?", answers: [ "It has a deadlock.", "It has no deadlock.", "It has a timed livelock.", "It has no timed livelock.", ], correctAnswer: '1, 4' }, { type: 'multiple-choice', question: "Does the water level model shown above have a deadlock?", answers: [ "Yes.", "No.", ], correctAnswer: '2' }, ];