Language equivalence is slow for models with many initial states #648
Description
We compute the state space resulting from synthesis in CIF and from the final UML model. If they have 'm' and 'n' initial states, we check 'm * n' pairs of states to match them and find initial pairs to start the language equivalence check. With many initial states (like 10K or so), this gives 100M possible pairs, making this very slow.
It would be better to only check initial states for matches that have a chance of being matches. For instance, we could make a map from the relevant state information that we're comparing for the states, to the actual states. Then, we'd likely get for each state information a list with two states, one from the first model and one from the second model. The insertion into the map is near linear. The construction of the pairs would be near-linear as well.