From cac85dbcca47b82a3c8bf767a117efb42c010696 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 16 Nov 2004 18:38:19 +0000 Subject: [PATCH] * src/tgba/tgbatba.hh (tgba_sba_proxy): New class, with the functionality of the old tgba_tba_proxy. * src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator, tgba_tba_proxy): Rewrite to produce TBA with at most N copies of each state, skipping the `bddtrue' stage now used only in tgba_sba_proxy. Doing so removes approximately 6% of states in the degeneralized tests of spotlbtt.test. (tgba_sba_proxy): Implement it. * src/tgbaalgos/neverclaim.hh, src/tgbaalgos/neverclaim.cc: Adjust to take a tgba_sba_proxy. * src/tgbatest/ltl2tgba.cc: Add option -DS and adjust call to never_claim_reachable(). --- ChangeLog | 15 +++- src/tgba/tgbatba.cc | 146 +++++++++++++++++++++++------------- src/tgba/tgbatba.hh | 54 ++++++++----- src/tgbaalgos/neverclaim.cc | 6 +- src/tgbaalgos/neverclaim.hh | 2 +- src/tgbatest/ltl2tgba.cc | 32 +++++--- 6 files changed, 173 insertions(+), 82 deletions(-) diff --git a/ChangeLog b/ChangeLog index 72f48ee66..bea4e50e4 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,18 @@ 2004-11-16 Alexandre Duret-Lutz + * src/tgba/tgbatba.hh (tgba_sba_proxy): New class, with the + functionality of the old tgba_tba_proxy. + * src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator, + tgba_tba_proxy): Rewrite to produce TBA with at most N copies of + each state, skipping the `bddtrue' stage now used only in + tgba_sba_proxy. Doing so removes approximately 6% of states in + the degeneralized tests of spotlbtt.test. + (tgba_sba_proxy): Implement it. + * src/tgbaalgos/neverclaim.hh, src/tgbaalgos/neverclaim.cc: Adjust + to take a tgba_sba_proxy. + * src/tgbatest/ltl2tgba.cc: Add option -DS and adjust call to + never_claim_reachable(). + * src/tgba/tgbatba.cc (state_tba_proxy::hash): Use wang32_hash. * src/tgba/tgbaproduct.cc (state_product::hash): Likewise. @@ -8,7 +21,7 @@ * src/evtgba/product.cc (evtgba_product_state::hash): ... here. * src/misc/Makefile.am (misc_HEADERS): Add hashfunc.hh. -2004-11-15 Alexandre Duret-Lutz +2004-11-15 Alexandre Duret-Lutz * src/tgbatest/ltl2tgba.cc (main): For non-generalized emptiness check, degeneralize the automaton only if it has too much diff --git a/src/tgba/tgbatba.cc b/src/tgba/tgbatba.cc index 31553b6e1..04cc0bbff 100644 --- a/src/tgba/tgbatba.cc +++ b/src/tgba/tgbatba.cc @@ -112,9 +112,10 @@ namespace spot typedef tgba_tba_proxy::cycle_list::const_iterator iterator; public: tgba_tba_proxy_succ_iterator(tgba_succ_iterator* it, - iterator expected, iterator end, + iterator expected, + const list& cycle, bdd the_acceptance_cond) - : it_(it), expected_(expected), end_(end), + : it_(it), expected_(expected), cycle_(cycle), the_acceptance_cond_(the_acceptance_cond) { } @@ -131,12 +132,14 @@ namespace spot first() { it_->first(); + sync_(); } void next() { it_->next(); + sync_(); } bool @@ -150,27 +153,7 @@ namespace spot state_tba_proxy* current_state() const { - // A transition in the *EXPECTED acceptance set should be directed - // to the next acceptance set. If the current transition is also - // in the next acceptance set, then go the one after, etc. - // - // See Denis Oddoux's PhD thesis for a nice explanation (in French). - // @PhDThesis{ oddoux.03.phd, - // author = {Denis Oddoux}, - // title = {Utilisation des automates alternants pour un - // model-checking efficace des logiques temporelles - // lin{\'e}aires.}, - // school = {Universit{\'e}e Paris 7}, - // year = {2003}, - // address = {Paris, France}, - // month = {December} - // } - // - iterator next = expected_; - bdd acc = it_->current_acceptance_conditions(); - while ((acc & *next) == *next && next != end_) - ++next; - return new state_tba_proxy(it_->current_state(), next); + return new state_tba_proxy(it_->current_state(), next_); } bdd @@ -182,13 +165,66 @@ namespace spot bdd current_acceptance_conditions() const { - return the_acceptance_cond_; + return accepting_ ? the_acceptance_cond_ : bddfalse; } protected: + + void + sync_() + { + if (done()) + return; + + bdd acc = it_->current_acceptance_conditions(); + + // bddtrue is a special condition used for tgba_sba_proxy + // to denote the (N+1)th copy of the state, after all acceptance + // conditions have been traversed. Such state is always accepting, + // so do not check acc for this. + // bddtrue is also used by tgba_tba_proxy if the automata do not + // use acceptance conditions. In that cases, all state are accepting. + if (*expected_ != bddtrue) + { + // A transition in the *EXPECTED acceptance set should be + // directed to the next acceptance set. If the current + // transition is also in the next acceptance set, then go + // the one after, etc. + // + // See Denis Oddoux's PhD thesis for a nice explanation (in French). + // @PhDThesis{ oddoux.03.phd, + // author = {Denis Oddoux}, + // title = {Utilisation des automates alternants pour un + // model-checking efficace des logiques temporelles + // lin{\'e}aires.}, + // school = {Universit{\'e}e Paris 7}, + // year = {2003}, + // address= {Paris, France}, + // month = {December} + // } + + next_ = expected_; + while (next_ != cycle_.end() && (acc & *next_) == *next_) + ++next_; + if (next_ != cycle_.end()) + { + accepting_ = false; + return; + } + } + // The transition is accepting. + accepting_ = true; + // Skip as much acceptance conditions as we can on our cycle. + next_ = cycle_.begin(); + while (next_ != expected_ && (acc & *next_) == *next_) + ++next_; + } + tgba_succ_iterator* it_; const iterator expected_; - const iterator end_; + iterator next_; + bool accepting_; + const list& cycle_; const bdd the_acceptance_cond_; friend class tgba_tba_proxy; }; @@ -198,23 +234,26 @@ namespace spot tgba_tba_proxy::tgba_tba_proxy(const tgba* a) : a_(a) { - bdd all = a_->all_acceptance_conditions(); - // We will use one acceptance condition for this automata. // Let's call it Acc[True]. int v = get_dict() ->register_acceptance_variable(ltl::constant::true_instance(), this); the_acceptance_cond_ = bdd_ithvar(v); - // Now build the "cycle" of acceptance conditions. - - acc_cycle_.push_front(bddtrue); - - while (all != bddfalse) + if (a->number_of_acceptance_conditions() == 0) { - bdd next = bdd_satone(all); - all -= next; - acc_cycle_.push_front(next); + acc_cycle_.push_front(bddtrue); + } + else + { + // Build a cycle of expected acceptance conditions. + bdd all = a_->all_acceptance_conditions(); + while (all != bddfalse) + { + bdd next = bdd_satone(all); + all -= next; + acc_cycle_.push_front(next); + } } } @@ -241,13 +280,8 @@ namespace spot tgba_succ_iterator* it = a_->succ_iter(s->real_state(), global_state, global_automaton); - cycle_list::const_iterator j = s->acceptance_iterator(); - cycle_list::const_iterator i = j++; - if (j == acc_cycle_.end()) - return new tgba_tba_proxy_succ_iterator(it, acc_cycle_.begin(), - acc_cycle_.end(), - the_acceptance_cond_); - return new tgba_tba_proxy_succ_iterator(it, i, acc_cycle_.end(), bddfalse); + return new tgba_tba_proxy_succ_iterator(it, s->acceptance_iterator(), + acc_cycle_, the_acceptance_cond_); } bdd_dict* @@ -290,15 +324,6 @@ namespace spot return !the_acceptance_cond_; } - bool - tgba_tba_proxy::state_is_accepting(const state* state) const - { - const state_tba_proxy* s = - dynamic_cast(state); - assert(s); - return bddtrue == s->acceptance_cond(); - } - bdd tgba_tba_proxy::compute_support_conditions(const state* state) const { @@ -326,4 +351,23 @@ namespace spot return a_->transition_annotation(i->it_); } + //////////////////////////////////////////////////////////////////////// + // tgba_sba_proxy + + tgba_sba_proxy::tgba_sba_proxy(const tgba* a) + : tgba_tba_proxy(a) + { + if (a->number_of_acceptance_conditions() > 0) + acc_cycle_.push_back(bddtrue); + } + + bool + tgba_sba_proxy::state_is_accepting(const state* state) const + { + const state_tba_proxy* s = + dynamic_cast(state); + assert(s); + return bddtrue == s->acceptance_cond(); + } + } diff --git a/src/tgba/tgbatba.hh b/src/tgba/tgbatba.hh index 4353d29d7..cd3131569 100644 --- a/src/tgba/tgbatba.hh +++ b/src/tgba/tgbatba.hh @@ -29,13 +29,12 @@ namespace spot { - /// \brief Degeneralize a spot::tgba on the fly. + /// \brief Degeneralize a spot::tgba on the fly, producing a TBA. /// /// This class acts as a proxy in front of a spot::tgba, that should - /// be degeneralized on the fly. - /// - /// This automaton is a spot::tgba, but it will always have exactly - /// one acceptance condition. + /// be degeneralized on the fly. The result is still a spot::tgba, + /// but it will always have exactly one acceptance condition so + /// it could be called TBA (without the G). /// /// The degeneralization is done by synchronizing the input /// automaton with a "counter" automaton such as the one shown in @@ -43,8 +42,10 @@ namespace spot /// Couveur, FME99). /// /// If the input automaton uses N acceptance conditions, the output - /// automaton can have at most max(N,1)+1 times more states and + /// automaton can have at most max(N,1) times more states and /// transitions. + /// + /// \see tgba_sba_proxy class tgba_tba_proxy : public tgba { public: @@ -71,29 +72,48 @@ namespace spot virtual bdd all_acceptance_conditions() const; virtual bdd neg_acceptance_conditions() const; - /// \brief Whether the state is accepting. - /// - /// A particularity of a spot::tgba_tba_proxy automaton is that - /// when a state has an outgoing accepting arc, all its outgoing - /// arcs are accepting. The state itself can therefore be - /// considered accepting. This is useful to many algorithms - /// working on degeneralized automata with state acceptance - /// conditions. - bool state_is_accepting(const state* state) const; - typedef std::list cycle_list; protected: virtual bdd compute_support_conditions(const state* state) const; virtual bdd compute_support_variables(const state* state) const; + cycle_list acc_cycle_; private: const tgba* a_; - cycle_list acc_cycle_; bdd the_acceptance_cond_; // Disallow copy. tgba_tba_proxy(const tgba_tba_proxy&); tgba_tba_proxy& tgba_tba_proxy::operator=(const tgba_tba_proxy&); }; + /// \brief Degeneralize a spot::tgba on the fly, producing an SBA. + /// + /// This class acts as a proxy in front of a spot::tgba, that should + /// be degeneralized on the fly. + /// + /// This is similar to tgba_tba_proxy, except that automata produced + /// with this algorithms can also been see as State-based Büchi + /// Automata (SBA). See tgba_sba_proxy::state_is_accepting(). (An + /// SBA is a TBA, and a TBA is a TGBA.) + /// + /// This extra property has a small cost in size: if the input + /// automaton uses N acceptance conditions, the output automaton can + /// have at most max(N,1)+1 times more states and transitions. + /// (This is only max(N,1) for tgba_tba_proxy.) + class tgba_sba_proxy : public tgba_tba_proxy + { + public: + tgba_sba_proxy(const tgba* a); + + /// \brief Whether the state is accepting. + /// + /// A particularity of a spot::tgba_sba_proxy automaton is that + /// when a state has an outgoing accepting arc, all its outgoing + /// arcs are accepting. The state itself can therefore be + /// considered accepting. This is useful in algorithms working on + /// degeneralized automata with state acceptance conditions. + bool state_is_accepting(const state* state) const; + }; + } #endif // SPOT_TGBA_TGBATBA_HH diff --git a/src/tgbaalgos/neverclaim.cc b/src/tgbaalgos/neverclaim.cc index ad3c0b2fd..ab2c30437 100644 --- a/src/tgbaalgos/neverclaim.cc +++ b/src/tgbaalgos/neverclaim.cc @@ -37,7 +37,7 @@ namespace spot class never_claim_bfs : public tgba_reachable_iterator_breadth_first { public: - never_claim_bfs(const tgba_tba_proxy* a, std::ostream& os, + never_claim_bfs(const tgba_sba_proxy* a, std::ostream& os, const ltl::formula* f) : tgba_reachable_iterator_breadth_first(a), os_(os), f_(f), accept_all_(-1), fi_needed_(false) @@ -76,7 +76,7 @@ namespace spot state_is_accepting(const state *s) { return - dynamic_cast(automata_)->state_is_accepting(s); + dynamic_cast(automata_)->state_is_accepting(s); } std::string @@ -184,7 +184,7 @@ namespace spot } // anonymous std::ostream& - never_claim_reachable(std::ostream& os, const tgba_tba_proxy* g, + never_claim_reachable(std::ostream& os, const tgba_sba_proxy* g, const ltl::formula* f) { never_claim_bfs n(g, os, f); diff --git a/src/tgbaalgos/neverclaim.hh b/src/tgbaalgos/neverclaim.hh index c9aa6ef73..3804dd263 100644 --- a/src/tgbaalgos/neverclaim.hh +++ b/src/tgbaalgos/neverclaim.hh @@ -35,7 +35,7 @@ namespace spot /// \param f The (optional) formula associated to the automaton. If given /// it will be output as a comment. std::ostream& never_claim_reachable(std::ostream& os, - const tgba_tba_proxy* g, + const tgba_sba_proxy* g, const ltl::formula* f = 0); } diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index f55993f0b..7fca99320 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -58,7 +58,8 @@ syntax(char* prog) << std::endl << " -A same as -a, but as a set" << std::endl << " -d turn on traces during parsing" << std::endl - << " -D degeneralize the automaton" << std::endl + << " -D degeneralize the automaton as a TBA" << std::endl + << " -DS degeneralize the automaton as an SBA" << std::endl << " -e[ALGO] emptiness-check, expect and compute an " << "accepting run" << std::endl << " -E[ALGO] emptiness-check, expect no accepting run" @@ -134,7 +135,7 @@ main(int argc, char** argv) int exit_code = 0; bool debug_opt = false; - bool degeneralize_opt = false; + enum { NoDegen, DegenTBA, DegenSBA } degeneralize_opt = NoDegen; bool degeneralize_maybe = false; bool fm_opt = false; bool fm_exprop_opt = false; @@ -182,7 +183,11 @@ main(int argc, char** argv) } else if (!strcmp(argv[formula_index], "-D")) { - degeneralize_opt = true; + degeneralize_opt = DegenTBA; + } + else if (!strcmp(argv[formula_index], "-DS")) + { + degeneralize_opt = DegenSBA; } else if (!strncmp(argv[formula_index], "-e", 2)) { @@ -231,7 +236,7 @@ main(int argc, char** argv) } else if (!strcmp(argv[formula_index], "-N")) { - degeneralize_opt = true; + degeneralize_opt = DegenSBA; output = 8; } else if (!strcmp(argv[formula_index], "-p")) @@ -494,10 +499,14 @@ main(int argc, char** argv) spot::tgba_tba_proxy* degeneralized = 0; - if (degeneralize_maybe && a->number_of_acceptance_conditions() > 1) - degeneralize_opt = true; - if (degeneralize_opt) + if (degeneralize_maybe + && degeneralize_opt == NoDegen + && a->number_of_acceptance_conditions() > 1) + degeneralize_opt = DegenTBA; + if (degeneralize_opt == DegenTBA) a = degeneralized = new spot::tgba_tba_proxy(a); + else if (degeneralize_opt == DegenSBA) + a = degeneralized = new spot::tgba_sba_proxy(a); spot::tgba_reduc* aut_red = 0; if (reduc_aut != spot::Reduce_None) @@ -602,8 +611,13 @@ main(int argc, char** argv) spot::lbtt_reachable(std::cout, a); break; case 8: - spot::never_claim_reachable(std::cout, degeneralized, f); - break; + { + assert(degeneralize_opt == DegenSBA); + const spot::tgba_sba_proxy* s = + static_cast(degeneralized); + spot::never_claim_reachable(std::cout, s, f); + break; + } default: assert(!"unknown output option"); }