## Deadlock and livelock

This lesson explains the concepts of deadlock and livelock.

### Deadlock

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

Location `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.

### Livelock

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 `increase` and `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 `done`.

The car will be increasing and decreasing it speed, using the `increase` and `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.