Convert controllable events to uncontrollable

This CIF to CIF transformation converts controllable events to uncontrollable.

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 controllable event in the CIF specification is converted to uncontrollable. 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:

uncontrollable a;
uncontrollable 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 c_ are renamed to preserve the event naming convention, see Event controllability. The prefix c_ is replaced by u_. In case the new global name is already in use in the specification, a suffix is also added.

Size considerations

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

Optimality

n/a

Annotations

This transformation does not process or add any annotations. If the specification has a controller properties annotation, it is removed.