From 96cc3a3f67003e14e9b8764a9a52e55c7bc4b4cb Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 3 Mar 2010 10:52:38 +0100 Subject: [PATCH] Optimize tgba_tba_proxy and tgba_sba_proxy for states that share an acceptance condition on all outgoing transitions. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This was motivated by experiments from Rüdiger Ehlers, showing that "ltl2ba -f 'a U (b U c)'" outperformed "ltl2tgba -f -N -R3 'a U (b U c)'". With this change and the previous one, it is no longer the case. * src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator::aut_): Store a pointer to the source automaton and... (tgba_tba_proxy_succ_iterator::sync_): ... use it in an extra optimization step to gather the acceptance conditions common to all outgoing transitions of the destination state, and pretend they are on the current (ingoing) transition. (tgba_tba_proxy::succ_iter): Pass the source automaton to the constructed iterator. * src/tgbatest/spotlbtt.test: Test -f -N -R3 -r7. * src/tgbatest/ltl2tgba.test: Add a test case for 'a U (b U c)'. --- ChangeLog | 21 +++++++++++++++++++++ src/tgba/tgbatba.cc | 31 +++++++++++++++++++++++++------ src/tgbatest/ltl2tgba.test | 9 +++++++++ src/tgbatest/spotlbtt.test | 8 ++++++++ 4 files changed, 63 insertions(+), 6 deletions(-) diff --git a/ChangeLog b/ChangeLog index 27bdd8e41..5cf219b2d 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,24 @@ +2010-03-03 Alexandre Duret-Lutz + + Optimize tgba_tba_proxy and tgba_sba_proxy for states that share + an acceptance condition on all outgoing transitions. + + This was motivated by experiments from Rüdiger Ehlers, showing + that "ltl2ba -f 'a U (b U c)'" outperformed "ltl2tgba -f -N -R3 'a + U (b U c)'". With this change and the previous one, it is no + longer the case. + + * src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator::aut_): Store + a pointer to the source automaton and... + (tgba_tba_proxy_succ_iterator::sync_): ... use it in an extra + optimization step to gather the acceptance conditions common + to all outgoing transitions of the destination state, and pretend + they are on the current (ingoing) transition. + (tgba_tba_proxy::succ_iter): Pass the + source automaton to the constructed iterator. + * src/tgbatest/spotlbtt.test: Test -f -N -R3 -r7. + * src/tgbatest/ltl2tgba.test: Add a test case for 'a U (b U c)'. + 2010-03-03 Alexandre Duret-Lutz ltl2tgba: apply -R3 before -D or -DS. diff --git a/src/tgba/tgbatba.cc b/src/tgba/tgbatba.cc index 575b3731d..a17bdd867 100644 --- a/src/tgba/tgbatba.cc +++ b/src/tgba/tgbatba.cc @@ -1,6 +1,8 @@ -// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// Copyright (C) 2010 Laboratoire de Recherche et Développement de +// l'Epita. +// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris +// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Université Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -114,9 +116,10 @@ namespace spot tgba_tba_proxy_succ_iterator(tgba_succ_iterator* it, iterator expected, const list& cycle, - bdd the_acceptance_cond) + bdd the_acceptance_cond, + const tgba* aut) : it_(it), expected_(expected), cycle_(cycle), - the_acceptance_cond_(the_acceptance_cond) + the_acceptance_cond_(the_acceptance_cond), aut_(aut) { } @@ -203,6 +206,20 @@ namespace spot // month = {December} // } + + // As an extra optimization step, gather the acceptance + // conditions common to all outgoing transitions of the + // destination state, and pretend they are already present + // on this transition. + bdd common = aut_->all_acceptance_conditions(); + state* dest = it_->current_state(); + tgba_succ_iterator* dest_it = aut_->succ_iter(dest); + for (dest_it->first(); !dest_it->done(); dest_it->next()) + common &= dest_it->current_acceptance_conditions(); + acc |= common; + delete dest_it; + delete dest; + next_ = expected_; while (next_ != cycle_.end() && (acc & *next_) == *next_) ++next_; @@ -226,6 +243,7 @@ namespace spot bool accepting_; const list& cycle_; const bdd the_acceptance_cond_; + const tgba* aut_; friend class ::spot::tgba_tba_proxy; }; @@ -281,7 +299,8 @@ namespace spot global_state, global_automaton); return new tgba_tba_proxy_succ_iterator(it, s->acceptance_iterator(), - acc_cycle_, the_acceptance_cond_); + acc_cycle_, the_acceptance_cond_, + a_); } bdd_dict* diff --git a/src/tgbatest/ltl2tgba.test b/src/tgbatest/ltl2tgba.test index fa2341bfb..3be074a71 100755 --- a/src/tgbatest/ltl2tgba.test +++ b/src/tgbatest/ltl2tgba.test @@ -50,3 +50,12 @@ check 'a R (b R c)' check '(a U b) U (c U d)' check '((Xp2)U(X(1)))&(p1 R(p2 R p0))' + + +# Make sure 'a U (b U c)' has 3 states and 6 transitions, +# before and after degeneralization. +for opt in '' -D -DS; do + ../ltl2tgba -k -f -R3 $opt 'a U (b U c)' > stdout + grep 'transitions: 6$' stdout + grep 'states: 3$' stdout +done diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test index b0b926d72..829f3946f 100755 --- a/src/tgbatest/spotlbtt.test +++ b/src/tgbatest/spotlbtt.test @@ -270,6 +270,14 @@ Algorithm Enabled = yes } +Algorithm +{ + Name = "Spot (Couvreur -- FM), pre + post reduction, via never claim" + Path = "${LBTT_TRANSLATE}" + Parameters = "--spin '../ltl2tgba -F -f -N -R3 -r7'" + Enabled = yes +} + Algorithm { Name = "Spot (Tauriainen -- TAA)"