CIF to CIF transformation to eliminate state/event exclusion invariants to automata can increase the alphabet of the specfication

For the following CIF specification, the alphabet of the specification (union of the alphabets of the automata) is empty:

event e;
invariant e needs false;

If we apply the CIF to CIF transformation to it to eliminate state/event exclusion invariants, we get the following specification, which has event e in its alphabet:

event e;
automaton StateEvtExcls:
  location:
    initial;
    marked;
    edge e when false;
end

The transformation thus changes the alphabet. I wonder if this is a problem?

This could lead to tricky situations. For instance, in the CIF controller properties checker, we warn about specifications with an empty uncontrollable or controllable alphabet. Currently, that is done on the input specification. But, after preprocessing for MDD-based checks, the alphabet is actually not empty. I can imagine more subtleties like this in CIF tools.

We could:

• Document that the transformation changes the alphabet of the specification.
• Add a type checker warning for state/event exclusion invariants on events that are not in the alphabet of the specification.
• Change the definition of alphabet to include the events of state/event exclusion invariants.
• Disallow models like this for the transformation.