This CIF to CIF transformation converts uncontrollable events to controllable.
tau is neither controllable nor uncontrollable, it is not touched by this transformation.
This transformation supports a subset of CIF specifications. The following restrictions apply:
Component definitions and component instantiations are not supported.
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):
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
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.
Uncontrollable events are modified, the size of the specification neither grows nor shrinks.