I'm looking into Spot's purge_unreachable_states function to get rid of some states after merging two automata in composition. It's got a weird way of returning a vector that says which states were removed (you have to pass a pointer to a function pointer that is then called with this vector). @gaperez64 remembered that this function might have been used at some point and so someone might remember the right way to use this? I found a similar function purge_dead_states being used in the surely losing states preprocessing which doesn't return this vector in any way, but it's also not needed in this code.
Otherwise, it should be simple to not use purge_unreachable_states as there are only two states (the initial states of the automata before merging) that could become unreachable if they have no incoming transitions, but it'd make more sense to try and use Spot functionality where possible.
I'm looking into Spot's
purge_unreachable_statesfunction to get rid of some states after merging two automata in composition. It's got a weird way of returning a vector that says which states were removed (you have to pass a pointer to a function pointer that is then called with this vector). @gaperez64 remembered that this function might have been used at some point and so someone might remember the right way to use this? I found a similar functionpurge_dead_statesbeing used in the surely losing states preprocessing which doesn't return this vector in any way, but it's also not needed in this code. Otherwise, it should be simple to not usepurge_unreachable_statesas there are only two states (the initial states of the automata before merging) that could become unreachable if they have no incoming transitions, but it'd make more sense to try and use Spot functionality where possible.