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.