5 Oct
2011
5 Oct
'11
4:44 p.m.
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
6 Oct
6 Oct
2:30 p.m.
Hi Nikos,
On Wed, Oct 5, 2011 at 4:44 PM, Nikos Gorogiannis
<nikos.gorogiannis(a)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,
--
Alexandre Duret-Lutz
7 Oct
7 Oct
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
4870
days inactive
4872
days old
2 comments
2 participants
participants (2)
-
Alexandre Duret-Lutz -
Nikos Gorogiannis