Data synthesis definition of uncontrolled system is not correct.

Consider the following CIF specification:

plant X:
  location l1:
    initial;
    marked;
end

requirement invariant not X.l1;

When performing synthesis, we get the following warning:

WARNING: The uncontrolled system has no states (taking into account only the state invariants).

That is incorrect, the uncontrolled system (i.e., plant X) has a state l1 that is also marked. In combination with the requirement, it has no state (the controlled system).

Notice that the warning says "state invariants". For synthesis, these are always "state requirement invariants" as we do not support plant invariants.

We should either change the warning message or apply the state requirements later such that we can differentiate between uncontrolled and controlled systems.