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.