7 Oct
2011
7 Oct
'11
2:24 p.m.
Hi Alexandre and thanks for your response.
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.
I will let you know if I manage to put something together!
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?
I believe I want to do (1), but I stil exploring ideas and options so
it's not entirely clear how this would be done and what restrictions
there will be on the modifications of the automaton. Briefly, the
automaton will be a proof in some system that allows cyclic proofs
(think induction) and the soundness of the proof depends on some
"infinitely often" style of property. So I thought that (a) real
on-the-fly model checking can be combined with proof search quite nicely
and (b) when the checker comes up with a counterexample, use it to
modify the proof and carry on.
I have no idea if anyone has done the partial restart before; it does
not fit the standard use case for model checking, so I would not be
surprised if it's never been done.
Thanks!
Nikos