[Spot] self-modifying automaton

Hi,

I've been looking for a library that would allow me to provide a (lazy) interface for enumerating the states of an automaton and doing on-the-fly model checking. Spot looks like exactly what I need! (which is great; I couldn't find any other tool supporting custom model checking like this).

What I will need on top of this, is when the emptiness check fails, I'd like to modify the automaton using the information provided by the check and re-run the check. Changes to the automaton will be localized, so destroying and rebuilding the objects relating to the emptiness check seems unnecessarily expensive. Is there any way around this?

Best regards Nikos Gorogiannis