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:
- https://en.wikipedia.org/wiki/DFA_minimization
- https://www.eclipse.org/escet/cif/tools/eventbased/dfa-minimize.html
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.