This lesson explains the concepts of deadlock and livelock.
If no event transitions are possible, and also no time transitions are possible (time may not progress), then no transitions are possible. This is called deadlock. No behavior is possible, or will ever become possible. As an example, consider the following CIF specification:
automaton use_case: location wait3: initial; urgent; edge tau when time > 3 goto done; location done; end
wait3 is the initial location. Initially,
time is zero. Time can not progress, as the location is urgent. Since the guard of the edge also does not hold, event
tau is also not possible. No transitions are possible, and the specification is in deadlock.
As long as an event is possible, no time may pass. If by mistake always an event is possible, this prevents all passage of time. Consider the following CIF specification:
automaton car: event increase, decrease, arrived; disc real speed = 0; cont pos = 0 der speed; location underway: initial; edge increase when speed < 100 do speed := speed + 1; edge decrease when speed > 0 do speed := speed - 1; edge arrived when pos = 850 goto done; location done; end
This specification models a
car that can
decrease its speed, so that it is at least
0 and at most
100. It keeps track of its position (continuous variable
pos) that increases more quickly as the speed increases. When position
850 is reached, the car has
arrived and is
The car will be increasing and decreasing it speed, using the
decrease events. As always at least one of them is enabled at any moment, time can never progress, and
pos remains zero. This effect is called livelock. While behavior is still possible, the model does not truly progress with useful behavior. The model gets 'stuck' repeating one or a few events.