diff --git a/src/saba/sabacomplementtgba.cc b/src/saba/sabacomplementtgba.cc index ddb8fd5da..1ded578de 100644 --- a/src/saba/sabacomplementtgba.cc +++ b/src/saba/sabacomplementtgba.cc @@ -24,6 +24,7 @@ #include #include #include "misc/hash.hh" +#include "tgbaalgos/degen.hh" #include "tgbaalgos/bfssteps.hh" #include "misc/hashfunc.hh" #include "ltlast/formula.hh" @@ -149,7 +150,7 @@ namespace spot typedef std::map bdd_list_t; - saba_complement_tgba_succ_iterator(const tgba_sba_proxy* automaton, + saba_complement_tgba_succ_iterator(const tgba_digraph* automaton, bdd the_acceptance_cond, const saba_state_complement_tgba* origin); @@ -166,7 +167,7 @@ namespace spot void state_conjunction(); void delete_condition_list(); - const tgba_sba_proxy* automaton_; + const tgba_digraph* automaton_; bdd the_acceptance_cond_; const saba_state_complement_tgba* origin_; bdd_list_t condition_list_; @@ -176,12 +177,13 @@ namespace spot }; saba_complement_tgba_succ_iterator:: - saba_complement_tgba_succ_iterator(const tgba_sba_proxy* automaton, + saba_complement_tgba_succ_iterator(const tgba_digraph* automaton, bdd the_acceptance_cond, const saba_state_complement_tgba* origin) : automaton_(automaton), the_acceptance_cond_(the_acceptance_cond), origin_(origin) { + assert(automaton->get_bprop(tgba_digraph::SBA)); // If state not accepting or rank is even if (((origin_->get_rank() & 1) == 0) || !automaton_->state_is_accepting(origin_->get_state())) @@ -364,13 +366,13 @@ namespace spot } // end namespace anonymous. saba_complement_tgba::saba_complement_tgba(const tgba* a) - : automaton_(new tgba_sba_proxy(a)) + : automaton_(degeneralize(a)) { get_dict()->register_all_variables_of(automaton_, this); int v = get_dict() ->register_acceptance_variable(ltl::constant::true_instance(), this); the_acceptance_cond_ = bdd_ithvar(v); - nb_states_ = count_states(automaton_); + nb_states_ = automaton_->num_states(); } saba_complement_tgba::~saba_complement_tgba() diff --git a/src/saba/sabacomplementtgba.hh b/src/saba/sabacomplementtgba.hh index 23f35319a..7b25404ab 100644 --- a/src/saba/sabacomplementtgba.hh +++ b/src/saba/sabacomplementtgba.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2009, 2010, 2013 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2010, 2013, 2014 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -66,7 +66,7 @@ namespace spot virtual std::string format_state(const saba_state* state) const; virtual bdd all_acceptance_conditions() const; private: - const tgba_sba_proxy* automaton_; + const tgba_digraph* automaton_; bdd the_acceptance_cond_; unsigned nb_states_; }; // end class tgba_saba_complement. diff --git a/src/tgba/tgbatba.cc b/src/tgba/tgbatba.cc index 6c019613b..f814096ac 100644 --- a/src/tgba/tgbatba.cc +++ b/src/tgba/tgbatba.cc @@ -169,19 +169,17 @@ namespace spot typedef tgba_tba_proxy::cycle_list list; typedef tgba_tba_proxy::cycle_list::const_iterator iterator; public: - tgba_tba_proxy_succ_iterator(const state* rs, - tgba::succ_iterable&& iterable, + tgba_tba_proxy_succ_iterator(tgba::succ_iterable&& iterable, iterator expected, const list& cycle, bdd the_acceptance_cond, const tgba_tba_proxy* aut) : the_acceptance_cond_(the_acceptance_cond) { - recycle(rs, std::move(iterable), expected, cycle, aut); + recycle(std::move(iterable), expected, cycle, aut); } - void recycle(const state* rs, - tgba::succ_iterable&& iterable, + void recycle(tgba::succ_iterable&& iterable, iterator expected, const list& cycle, const tgba_tba_proxy* aut) @@ -204,110 +202,43 @@ namespace spot bdd otheracc = aut->common_acceptance_conditions_of_original_state(odest); - iterator next; - // 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 automaton - // does not use acceptance conditions. In that case, all - // states 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 to 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; + // Consider both the current acceptance sets, and the + // acceptance sets common to the outgoing transition of + // the destination state. + acc |= otheracc; + while (next != cycle.end() && bdd_implies(*next, acc)) + ++next; + if (next != cycle.end()) { - // When degeneralizing to SBA, ignore the last - // expected acceptance set (the value of *prev below) - // if it is common to all other outgoing transitions (of the - // current state) AND if it is not used by any outgoing - // transition of the destination state. - // - // 1) It's correct to do that, because this acceptance - // set is common to other outgoing transitions. - // Therefore if we make a cycle to this state we - // will eventually see that acceptance set thanks - // to the "pulling" of the common acceptance sets - // of the destination state (cf. "odest"). - // - // 2) It's also desirable because it makes the - // degeneralization idempotent (up to a renaming of - // states). Consider the following automaton where - // 1 is initial and => marks accepting transitions: - // 1=>1, 1=>2, 2->2, 2->1 This is already an SBA, - // with 1 as accepting state. However if you try - // degeralize it without ignoring *prev, we'll get - // two copies of states 2, depending on whether we - // reach it using 1=>2 or from 2->2. If this - // example was not clear, uncomment this following - // "if" block, and play with the "degenid.test" - // test case. - // - // 3) Ignoring all common acceptance sets would also - // be correct, but it would make the - // degeneralization produce larger automata in some - // cases. The current condition to ignore only one - // acceptance set if is this not used by the next - // state is a heuristic that is compatible with - // point 2) above while not causing more states to - // be generated in our benchmark of 188 formulae - // from the literature. - if (expected != cycle.begin()) - { - iterator prev = expected; - --prev; - bdd common = aut-> - common_acceptance_conditions_of_original_state(rs); - if (bdd_implies(*prev, common)) - { - bdd u = aut-> - union_acceptance_conditions_of_original_state(odest); - if (!bdd_implies(*prev, u)) - acc -= *prev; - } - } - // Use the acceptance sets common to all outgoing - // transition of the destination state. In case of a - // self-loop, we will be adding back the acceptance - // set we removed. This is what we want. - acc |= otheracc; + accepting = false; } else { - // 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 to 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; - // Consider both the current acceptance sets, and the - // acceptance sets common to the outgoing transition of - // the destination state. - acc |= otheracc; - while (next != cycle.end() && bdd_implies(*next, acc)) + // The transition is accepting. + accepting = true; + // Skip as much acceptance conditions as we can on our cycle. + next = cycle.begin(); + while (next != expected && bdd_implies(*next, acc)) ++next; - if (next != cycle.end()) - { - accepting = false; - goto next_is_set; - } } - // The transition is accepting. - accepting = true; - // Skip as much acceptance conditions as we can on our cycle. - next = cycle.begin(); - while (next != expected && bdd_implies(*next, acc)) - ++next; - next_is_set: state_tba_proxy* dest = down_cast(aut->create_state(odest, next)); // Is DEST already reachable with the same value of ACCEPTING? @@ -508,12 +439,12 @@ namespace spot { tgba_tba_proxy_succ_iterator* res = down_cast(iter_cache_); - res->recycle(rs, a_->succ(rs), + res->recycle(a_->succ(rs), s->acceptance_iterator(), acc_cycle_, this); iter_cache_ = nullptr; return res; } - return new tgba_tba_proxy_succ_iterator(rs, a_->succ(rs), + return new tgba_tba_proxy_succ_iterator(a_->succ(rs), s->acceptance_iterator(), acc_cycle_, the_acceptance_cond_, this); @@ -608,64 +539,4 @@ namespace spot return a_->support_conditions(s->real_state()); } - //////////////////////////////////////////////////////////////////////// - // tgba_sba_proxy - - tgba_sba_proxy::tgba_sba_proxy(const tgba* a) - : tgba_tba_proxy(a) - { - if (a->number_of_acceptance_conditions() > 0) - { - cycle_start_ = acc_cycle_.insert(acc_cycle_.end(), bddtrue); - - bdd all = a->all_acceptance_conditions(); - - state* init = a->get_init_state(); - for (auto it: a->succ(init)) - { - // Look only for transitions that are accepting. - if (all != it->current_acceptance_conditions()) - continue; - // Look only for self-loops. - state* dest = it->current_state(); - if (dest->compare(init) == 0) - { - // The initial state has an accepting self-loop. - // In that case it is better to start the accepting - // cycle on a "acceptance" state. This will avoid - // duplication of the initial state. - // The cycle_start_ points to the right starting - // point already, so just return. - dest->destroy(); - init->destroy(); - return; - } - dest->destroy(); - } - init->destroy(); - } - - // If we arrive here either because the number of acceptance - // condition is 0, or because the initial state has no accepting - // self-loop, start the acceptance cycle on the first condition - // (that is a non-accepting state if the number of conditions is - // not 0). - cycle_start_ = acc_cycle_.begin(); - } - - state* - tgba_sba_proxy::get_init_state() const - { - return create_state(a_->get_init_state(), cycle_start_); - } - - bool - tgba_sba_proxy::state_is_accepting(const state* state) const - { - const state_tba_proxy* s = - down_cast(state); - assert(s); - return bddtrue == s->acceptance_cond(); - } - } diff --git a/src/tgba/tgbatba.hh b/src/tgba/tgbatba.hh index ebd5aac92..075f742b2 100644 --- a/src/tgba/tgbatba.hh +++ b/src/tgba/tgbatba.hh @@ -47,8 +47,6 @@ namespace spot /// If the input automaton uses N acceptance conditions, the output /// automaton can have at most max(N,1) times more states and /// transitions. - /// - /// \see tgba_sba_proxy class SPOT_API tgba_tba_proxy : public tgba { public: @@ -120,47 +118,5 @@ namespace spot tgba_tba_proxy& operator=(const tgba_tba_proxy&) SPOT_DELETED; }; - /// \ingroup tgba_on_the_fly_algorithms - /// \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 seen 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.) - /// - /// If you want to degeneralize an automaton once for all, and not - /// on-the-fly, consider using degeneralize() instead because it is - /// usually faster. Also the degeneralize() function implements - /// several SCC-based optimizations that are not implemented in this - /// one. - /// - /// \see degeneralize - class SPOT_API 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; - - virtual state* get_init_state() const; - protected: - cycle_list::iterator cycle_start_; - }; - } #endif // SPOT_TGBA_TGBATBA_HH diff --git a/src/tgbaalgos/degen.hh b/src/tgbaalgos/degen.hh index 9d9d39d6b..2255c4112 100644 --- a/src/tgbaalgos/degen.hh +++ b/src/tgbaalgos/degen.hh @@ -31,9 +31,6 @@ namespace spot /// This algorithms will build a new explicit automaton that has /// at most (N+1) times the number of states of the original automaton. /// - /// If you want to build a degeneralized automaton on-the-fly, see - /// spot::tgba_sba_proxy or spot::tgba_tba_proxy. - /// /// When \a use_z_lvl is set, the level of the degeneralized /// automaton is reset everytime an accepting SCC is exited. If \a /// use_cust_acc_orders is set, the degeneralization will compute a @@ -48,7 +45,7 @@ namespace spot /// Any of these three options will cause the SCCs of the automaton /// \a a to be computed prior to its actual degeneralization. /// - /// \see tgba_sba_proxy, tgba_tba_proxy + /// \see tgba_tba_proxy SPOT_API tgba_digraph* degeneralize(const tgba* a, bool use_z_lvl = true, bool use_cust_acc_orders = false, diff --git a/src/tgbatest/complementation.cc b/src/tgbatest/complementation.cc index 2a6a1648d..61a6042bf 100644 --- a/src/tgbatest/complementation.cc +++ b/src/tgbatest/complementation.cc @@ -31,6 +31,7 @@ #include "ltlast/unop.hh" #include "tgbaalgos/stats.hh" #include "tgbaalgos/emptiness_stats.hh" +#include "tgbaalgos/degen.hh" #include "tgba/tgbatba.hh" #include "tgba/tgbasafracomplement.hh" @@ -215,11 +216,10 @@ int main(int argc, char* argv[]) << a->number_of_acceptance_conditions() << std::endl; - spot::tgba *buchi = new spot::tgba_sba_proxy(a); - a_size = spot::stats_reachable(buchi); + auto buchi = spot::degeneralize(a); std::cout << "Buchi: " - << a_size.states << ", " - << a_size.transitions << ", " + << buchi->num_states() + << buchi->num_transitions() << buchi->number_of_acceptance_conditions() << std::endl; delete buchi; diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 815473602..c8df4f274 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -1660,7 +1660,7 @@ main(int argc, char** argv) case 8: { assert(degeneralize_opt == DegenSBA); - if (assume_sba || dynamic_cast(a)) + if (assume_sba) spot::never_claim_reachable(std::cout, a, f, spin_comments); else {