This CIF to CIF transformation eliminates the
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
The newly introduced
tau_ events are renamed to
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.
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.