Hi Nikos,
On Wed, Oct 5, 2011 at 4:44 PM, Nikos Gorogiannis nikos.gorogiannis@eecs.qmul.ac.uk wrote:
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).
It's good you found Spot, then. So far, most people contacting us have been using only it's LTL->Büchi translator. So I'll be very interested to get any kind of feedback about your use case.
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?
Do you mean
1) that you want to reuse part of the information that have already been computed by the emptiness check during the first run, and just invalidate anything related to the SCC that has been altered afterwards?
2) that you want the start a fresh emptiness check from scratch, but just without deleting and re-building a new the emptiness_check instance?
I believe none of the emptiness_checks presently support either scenarios. The second one could be achieved by adding a reset() method to all emptiness_check sub classes (should be easy), but that reset() method would not bring a huge speed-up over the delete/new approach. The first approach would require much more invasive changes, and it might not be suitable with all emptiness check algorithms. Maybe an emptiness-check could be tuned to support such a "partial restart" ; it seems worth a though. Has anybody done such a thing before?
Best regards,