## Eliminate `tau` event

This CIF to CIF transformation eliminates the `tau` event.

### Supported specifications

This transformation supports all CIF specifications.

### Preprocessing

n/a

### Implementation details

This transformation introduces new events for the `tau` event, one per automaton where a `tau` event is used. The new events are named `tau_` (if that name is not already in use).

If the alphabet is explicit specified, it is extended as well.

The new events are neither controllable nor uncontrollable, and don’t have a data type.

For instance, the following specification:

    automaton p:
      event e;

      location l1:
        initial;
        edge when true goto l2;

      location l2:
        edge e, tau goto l1;
    end

is transformed to the following specification:

    automaton p:
      event e;
      event tau_;

      location l1:
        initial;
        edge tau_ when true goto l2;

      location l2:
        edge e, tau_ goto l1;
    end

### Renaming

The newly introduced `tau_` events are renamed to `tau_2`, `tau_3`, etc, if they conflict with other declarations with the same name, that already exist in the automata. If renaming is needed, a warning is printed to the console.

### Size considerations

New events may be added, the alphabet may be extended, and an explicit event may be added to edges. Therefore, the size of the specification may increase.

### Optimality

n/a

### Annotations

This transformation does not process, add, or remove any annotations. The newly added events do not have any annotations.