Convert uncontrollable events to controllable

This CIF to CIF transformation converts uncontrollable events to controllable.

As tau is neither controllable nor uncontrollable, it is not touched by this transformation.

Supported specifications

This transformation supports a subset of CIF specifications. The following restrictions apply:

  • Component definitions and component instantiations are not supported.

Preprocessing

No preprocessing is currently performed by this CIF to CIF transformation. To increase the subset of specifications that can be transformed, apply the following CIF to CIF transformations (in the given order):

Implementation details

Each uncontrollable event in the CIF specification is converted to controllable. For instance, the following specification:

uncontrollable a;
controllable b;

automaton aut:
  location l1:
    initial;
    marked;
    edge a goto l2;
  location l2:
    edge b goto l1;
end

is transformed to the following specification:

controllable a;
controllable b;

automaton aut:
  location l1:
    initial;
    marked;
    edge a goto l2;
  location l2:
    edge b goto l1;
end

Renaming

Event names with the special prefix u_ are renamed to preserve the event naming convention, see Event controllability. The prefix u_ is replaced by c_. In case the new global name is already in use in the specification, a suffix is also added.

Size considerations

Uncontrollable events are modified, the size of the specification neither grows nor shrinks.

Optimality

n/a

Annotations

This transformation does not process, add, or remove any annotations.