Document that CIF explorer does not produce minimal state spaces

Consider the following specification:

event e;

automaton a:
  disc int[0..2] x in any;

  location:
    initial;
    marked;
    edge e;
end

The CIF explorer will produce the following statespace:

event e;

automaton statespace:
  alphabet e;

  location loc1:
    initial;
    marked;
    edge e;

  location loc2:
    initial;
    marked;
    edge e;

  location loc3:
    initial;
    marked;
    edge e;
end

This is not a minimal representation of the state space. For more information on minimal DFAs and DFA minimization, see:

The CIF explorer considers the state of the CIF model, and since variable a.x is part of the CIF model's state, indeed there are 3 states for this CIF model. However, for the state space, these can no longer be distinguished as such. All three states have the exact same behavior, the same language. The minimal result would be:

event e;

automaton statespace:
  alphabet e;

  location loc1:
    initial;
    marked;
    edge e;
end

Note that you can minimize the state space resulting from the CIF explorer using the CIF event-based DFA minimization tool. This does however have several preconditions, such as not having tau events and having exactly one initial location. As such, it does not apply to the example above.

We could potentially automatically minimize the computed state space. However, this could be expensive. So, if we were to go this way, we should make it a configurable option. But, given that the CIF event-based DFA minimization tool has various restrictions, we couldn't apply that in its current form to perform the minimization.

I therefore think we should for now just document the non-minimal result in the CIF explorer documentation.