Hi Tobias, Tobias John <tobias.john@tu-dresden.de> writes:

Is there some way to get the original state numbers from the reduced automaton? My intuition is that the property "original-states" would be suitable to store the original state numbers but the function "purge_dead_states()" does not set this property.

It does not set it, however it updates it if it is present. So if you call it with a identity mapping in original-states, you should be good. Try this: auto orig = new std::vector<unsigned>(aut->num_states()); std::iota(orig->begin(), orig->end(), 0); aut->set_named_prop("original-states", orig); aut->purge_dead_states(); for (unsigned s = 0, n = aut->num_states(); s < n; ++s) std::cout << "orig[" << s << "]=" << (*orig)[s] << '\n';

In my opinion, the function "purge_dead_states()" setting the property "original-states" would be a useful feature to be included in future releases of Spot.

What if Spot would provide a function that fills original-states as in the first 3 lines of the above snippet? Maybe set_default_original_states()? This way we don't have to update this property in situations where it's not needed.