5 Mar
2021
5 Mar
'21
10:24 a.m.
Hi Tobias,
Tobias John <tobias.john(a)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.