//////////////////////////////////////////////////////////////////////////////
// Copyright (c) 2010, 2026 Contributors to the Eclipse Foundation
//
// See the NOTICE file(s) distributed with this work for additional
// information regarding copyright ownership.
//
// This program and the accompanying materials are made available
// under the terms of the MIT License which is available at
// https://opensource.org/licenses/MIT
//
// SPDX-License-Identifier: MIT
//////////////////////////////////////////////////////////////////////////////

include::../_part_attributes.asciidoc[]

:leveloffset: -2

[[tools-cif2cif-chapter-elim-tau-event]]
== Eliminate `tau` event

indexterm:[CIF to CIF transformer,eliminate tau event]
indexterm:[eliminate tau event]
indexterm:[tau event,eliminate]
This CIF to CIF transformation eliminates the `tau` event.

=== Supported specifications

This transformation supports all CIF specifications.

=== Preprocessing

n/a

indexterm:[eliminate tau event,implementation]

=== 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:

[source, cif]
----
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:

[source, cif]
----
automaton p:
  event e;
  event tau_;

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

  location l2:
    edge e, tau_ goto l1;
end
----

indexterm:[eliminate tau event,renaming]

=== 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.

indexterm:[eliminate tau event,size considerations]

=== 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.
