From d8ba172e6d1660a4f8dd37e9def92f2baa8c3f05 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 25 Aug 2011 16:53:40 +0200 Subject: [PATCH] Running `ltl2tgba -R1q -R1t -N` would degeneralize before and after the simulation-reduction. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Report from Tomáš Babiak . * src/tgbaalgos/neverclaim.hh (never_claim_reachable): Take a tgba as input. * src/tgbaalgos/neverclaim.cc (never_claim_bfs): Call state_is_accepting() only if this tgba turns out to be a tgba_sba_proxy. Otherwise check the acceptance of one outgoing transition as we do in dotty_bfs since 2011-03-05. * src/tgbatest/ltl2tgba.cc: Do not redegeneralize before calling never_claim_reachable() if we know the automaton is degeneralized already. * src/tgbatest/ltl2tgba.test: Add a test case. --- ChangeLog | 18 ++++++++++++++++++ src/tgbaalgos/neverclaim.cc | 29 ++++++++++++++++++++++++----- src/tgbaalgos/neverclaim.hh | 9 ++++++--- src/tgbatest/ltl2tgba.cc | 8 +++----- src/tgbatest/ltl2tgba.test | 10 ++++++++++ 5 files changed, 61 insertions(+), 13 deletions(-) diff --git a/ChangeLog b/ChangeLog index 7a05cf594..343b54101 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,21 @@ +2011-08-25 Alexandre Duret-Lutz + + Running `ltl2tgba -R1q -R1t -N` would degeneralize before and + after the simulation-reduction. + + Report from Tomáš Babiak . + + * src/tgbaalgos/neverclaim.hh (never_claim_reachable): Take + a tgba as input. + * src/tgbaalgos/neverclaim.cc (never_claim_bfs): Call + state_is_accepting() only if this tgba turns out to be + a tgba_sba_proxy. Otherwise check the acceptance of one + outgoing transition as we do in dotty_bfs since 2011-03-05. + * src/tgbatest/ltl2tgba.cc: Do not redegeneralize before + calling never_claim_reachable() if we know the automaton is + degeneralized already. + * src/tgbatest/ltl2tgba.test: Add a test case. + 2011-08-17 Alexandre Duret-Lutz Please GCC 4.6. diff --git a/src/tgbaalgos/neverclaim.cc b/src/tgbaalgos/neverclaim.cc index 9ea937827..d44787fc3 100644 --- a/src/tgbaalgos/neverclaim.cc +++ b/src/tgbaalgos/neverclaim.cc @@ -38,11 +38,12 @@ namespace spot class never_claim_bfs : public tgba_reachable_iterator_breadth_first { public: - never_claim_bfs(const tgba_sba_proxy* a, std::ostream& os, + never_claim_bfs(const tgba* a, std::ostream& os, const ltl::formula* f, bool comments) : tgba_reachable_iterator_breadth_first(a), os_(os), f_(f), accept_all_(-1), fi_needed_(false), - comments_(comments) + comments_(comments), all_acc_conds_(a->all_acceptance_conditions()), + degen_(dynamic_cast(a)) { } @@ -77,8 +78,23 @@ namespace spot bool state_is_accepting(const state *s) { - return - dynamic_cast(automata_)->state_is_accepting(s); + // If the automaton is degeneralized on-the-fly, + // it's easier to just query the state_is_accepting() method. + if (degen_) + return degen_->state_is_accepting(s); + + // Otherwise, since we are dealing with a degeneralized + // automaton nonetheless, the transitions leaving an accepting + // state are either all accepting, or all non-accepting. So + // we just check the acceptance of the first transition. This + // is not terribly efficient since we have to create the + // iterator. + tgba_succ_iterator* it = automata_->succ_iter(s); + it->first(); + bool accepting = + !it->done() && it->current_acceptance_conditions() == all_acc_conds_; + delete it; + return accepting; } std::string @@ -185,13 +201,16 @@ namespace spot bool fi_needed_; state* init_; bool comments_; + bdd all_acc_conds_; + const tgba_sba_proxy* degen_; }; } // anonymous std::ostream& - never_claim_reachable(std::ostream& os, const tgba_sba_proxy* g, + never_claim_reachable(std::ostream& os, const tgba* g, const ltl::formula* f, bool comments) { + assert(g->number_of_acceptance_conditions() <= 1); never_claim_bfs n(g, os, f, comments); n.run(); return os; diff --git a/src/tgbaalgos/neverclaim.hh b/src/tgbaalgos/neverclaim.hh index eca8349b5..f082a4821 100644 --- a/src/tgbaalgos/neverclaim.hh +++ b/src/tgbaalgos/neverclaim.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -34,13 +34,16 @@ namespace spot /// \ingroup tgba_io /// /// \param os The output stream to print on. - /// \param g The degeneralized automaton to output. + /// \param g The (state-based degeneralized) automaton to output. + /// There should be only one acceptance condition, and + /// all the transitions of a state should be either all accepting + /// or all unaccepting. /// \param f The (optional) formula associated to the automaton. If given /// it will be output as a comment. /// \param comments Whether to comment each state of the never clause /// with the label of the \a g automaton. std::ostream& never_claim_reachable(std::ostream& os, - const tgba_sba_proxy* g, + const tgba* g, const ltl::formula* f = 0, bool comments = false); } diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 2afffc858..ba6d6d128 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -1142,16 +1142,14 @@ main(int argc, char** argv) case 8: { assert(degeneralize_opt == DegenSBA); - const spot::tgba_sba_proxy* s = - dynamic_cast(a); - if (s) - spot::never_claim_reachable(std::cout, s, f, spin_comments); + if (assume_sba || dynamic_cast(a)) + spot::never_claim_reachable(std::cout, a, f, spin_comments); else { // It is possible that we have applied other // operations to the automaton since its initial // degeneralization. Let's degeneralize again! - s = new spot::tgba_sba_proxy(a); + spot::tgba_sba_proxy* s = new spot::tgba_sba_proxy(a); spot::never_claim_reachable(std::cout, s, f, spin_comments); delete s; } diff --git a/src/tgbatest/ltl2tgba.test b/src/tgbatest/ltl2tgba.test index 3ba1920e4..94b5ced43 100755 --- a/src/tgbatest/ltl2tgba.test +++ b/src/tgbatest/ltl2tgba.test @@ -124,3 +124,13 @@ grep 'states: 3$' stdout run 0 ../ltl2tgba -R3 -Rm -ks -f "Gq|Gr|(G(q|FGp)&G(r|FG!p))" >stdout grep 'transitions: 5$' stdout grep 'states: 3$' stdout + +# Make sure FGa|GFb has the same number of states/transitions when +# output as a never claim or are a degeneralized BA in Spot's textual +# format. The option -R1q -R1t used to cause two degeneralizations to +# occur. +run 0 ../ltl2tgba -R1q -R1t -N 'FGa|FGb' > out.never +run 0 ../ltl2tgba -XN -kt out.never > count.never +run 0 ../ltl2tgba -R1q -R1t -DS -b 'FGa|FGb' > out.spot +run 0 ../ltl2tgba -X -kt out.spot > count.spot +cmp count.never count.spot