diff --git a/ChangeLog b/ChangeLog index 056f51295..7b454d56e 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,24 @@ +2009-11-20 Alexandre Duret-Lutz + + Strip useless acceptance conditions in scc_filter(). + + A useless acceptance conditions is one that is always implied by + another. + + * src/misc/bddop.hh, src/misc/bddop.cc + (compute_neg_acceptance_conditions): New function. + * src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc + (set_acceptance_conditions): New function. + * src/tgbaalgos/scc.cc (build_map, build_scc_stats, dump_scc_dot): + Keep track of useful acceptance conditions. + (useful_acc_of): New function. + * src/tgbaalgos/scc.hh (scc_stats, scc_map::scc::useful_scc): New + attributes. + * src/tgbaalgos/sccfilter.cc (filter_iter): Adjust to filter + useless acceptance conditions. + (scc_filter): Compute useful acceptance conditions and pass them + to filter_iter. + 2009-11-20 Alexandre Duret-Lutz * src/tgbaalgos/sccfilter.cc (scc_filter): Merge transitions diff --git a/src/misc/bddop.cc b/src/misc/bddop.cc index 325e33003..7077c05e5 100644 --- a/src/misc/bddop.cc +++ b/src/misc/bddop.cc @@ -48,4 +48,19 @@ namespace spot return all; } + + bdd + compute_neg_acceptance_conditions(bdd all_acceptance_conditions) + { + bdd cur = bdd_support(all_acceptance_conditions); + bdd neg = bddtrue; + while (cur != bddtrue) + { + neg &= bdd_nithvar(bdd_var(cur)); + assert(bdd_low(cur) != bddtrue); + cur = bdd_high(cur); + } + return neg; + } + } diff --git a/src/misc/bddop.hh b/src/misc/bddop.hh index 571354e83..f865e51bd 100644 --- a/src/misc/bddop.hh +++ b/src/misc/bddop.hh @@ -29,6 +29,10 @@ namespace spot /// \brief Compute all acceptance conditions from all neg acceptance /// conditions. bdd compute_all_acceptance_conditions(bdd neg_acceptance_conditions); + + /// \brief Compute neg acceptance conditions from all acceptance + /// conditions. + bdd compute_neg_acceptance_conditions(bdd all_acceptance_conditions); } #endif // SPOT_MISC_BDDOP_HH diff --git a/src/tgba/tgbaexplicit.cc b/src/tgba/tgbaexplicit.cc index 279bca058..4d572adcf 100644 --- a/src/tgba/tgbaexplicit.cc +++ b/src/tgba/tgbaexplicit.cc @@ -159,6 +159,17 @@ namespace spot neg_acceptance_conditions_ = f; } + void + tgba_explicit::set_acceptance_conditions(bdd acc) + { + assert(neg_acceptance_conditions_ == bddtrue); + assert(all_acceptance_conditions_computed_ == false); + dict_->register_acceptance_variables(bdd_support(acc), this); + neg_acceptance_conditions_ = compute_neg_acceptance_conditions(acc); + all_acceptance_conditions_computed_ = true; + all_acceptance_conditions_ = acc; + } + bool tgba_explicit::has_acceptance_condition(const ltl::formula* f) const { diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh index 2eb03278c..3bfb28e7b 100644 --- a/src/tgba/tgbaexplicit.hh +++ b/src/tgba/tgbaexplicit.hh @@ -69,6 +69,9 @@ namespace spot /// transition. void copy_acceptance_conditions_of(const tgba *a); + /// The the acceptance conditions. + void set_acceptance_conditions(bdd acc); + bool has_acceptance_condition(const ltl::formula* f) const; void add_acceptance_condition(transition* t, const ltl::formula* f); /// This assumes that all acceptance conditions in \a f are known from dict. diff --git a/src/tgbaalgos/scc.cc b/src/tgbaalgos/scc.cc index d36b1770d..038d19be8 100644 --- a/src/tgbaalgos/scc.cc +++ b/src/tgbaalgos/scc.cc @@ -259,13 +259,17 @@ namespace spot cond_set conds; conds.insert(cond); bdd supp = bdd_support(cond); + bdd all = aut_->all_acceptance_conditions(); + bdd useful = all - acc; while (threshold > root_.front().index) { assert(!root_.empty()); assert(!arc_acc_.empty()); assert(arc_acc_.size() == arc_cond_.size()); acc |= root_.front().acc; - acc |= arc_acc_.top(); + bdd lacc = arc_acc_.top(); + acc |= lacc; + useful |= (all - lacc) | root_.front().useful_acc; states.splice(states.end(), root_.front().states); succs.insert(root_.front().succ.begin(), root_.front().succ.end()); @@ -292,6 +296,7 @@ namespace spot root_.front().supp &= supp; // This SCC is no longer trivial. root_.front().trivial = false; + root_.front().useful_acc |= useful; } // recursively update supp_rec @@ -347,6 +352,13 @@ namespace spot return scc_map_.size(); } + bdd + scc_map::useful_acc_of(unsigned n) const + { + assert(scc_map_.size() > n); + return scc_map_[n].useful_acc; + } + namespace { struct scc_recurse_data @@ -422,8 +434,14 @@ namespace spot res.dead_paths = d.dead_paths[init]; res.useless_scc_map.reserve(res.scc_total); + bdd useful_acc = bddfalse; for (unsigned n = 0; n < res.scc_total; ++n) - res.useless_scc_map[n] = !d.acc_paths[n]; + { + res.useless_scc_map[n] = !d.acc_paths[n]; + if (m.accepting(n)) + useful_acc |= m.useful_acc_of(n); + } + res.useful_acc = useful_acc; return res; } @@ -481,7 +499,10 @@ namespace spot m.ap_set_of(state))); ostr << "]\\n APrec=["; escape_str(ostr, bdd_format_sat(m.get_aut()->get_dict(), - m.aprec_set_of(state))) << "]"; + m.aprec_set_of(state))); + ostr << "]\\n useful=["; + escape_str(ostr, bdd_format_accset(m.get_aut()->get_dict(), + m.useful_acc_of(state))) << "]"; } std::cout << " " << state << " [shape=box," diff --git a/src/tgbaalgos/scc.hh b/src/tgbaalgos/scc.hh index ced5a2e9e..458f28f3f 100644 --- a/src/tgbaalgos/scc.hh +++ b/src/tgbaalgos/scc.hh @@ -59,6 +59,11 @@ namespace spot /// A map of the useless SCCs. std::vector useless_scc_map; + /// The set of useful acceptance conditions (i.e. acceptance + /// conditions that are not always implied by other acceptance + /// conditions). + bdd useful_acc; + std::ostream& dump(std::ostream& out) const; }; @@ -129,6 +134,12 @@ namespace spot /// \pre This should only be called once build_map() has run. bdd acc_set_of(unsigned n) const; + /// \brief Return the set of useful acceptance conditions if SCC \a n. + /// + /// Useless acceptances conditions are always implied by other acceptances + /// conditions. This returns all the other acceptance conditions. + bdd useful_acc_of(unsigned n) const; + /// \brief Return the set of states of an SCC. /// /// The states in the returned list are still owned by the scc_map @@ -154,7 +165,7 @@ namespace spot public: scc(int index) : index(index), acc(bddfalse), supp(bddtrue), supp_rec(bddfalse), - trivial(true) {}; + trivial(true), useful_acc(bddfalse) {}; /// Index of the SCC. int index; /// The union of all acceptance conditions of transitions which @@ -172,6 +183,8 @@ namespace spot succ_type succ; /// Trivial SCC have one state and no self-loops. bool trivial; + /// Useful acceptance conditions. + bdd useful_acc; }; const tgba* aut_; // Automata to decompose. diff --git a/src/tgbaalgos/sccfilter.cc b/src/tgbaalgos/sccfilter.cc index 1c7aa2968..3144e0ffd 100644 --- a/src/tgbaalgos/sccfilter.cc +++ b/src/tgbaalgos/sccfilter.cc @@ -33,14 +33,16 @@ namespace spot public: filter_iter(const tgba* a, const scc_map& sm, - const std::vector& useless) + const std::vector& useless, + bdd useful, bdd strip) : tgba_reachable_iterator_depth_first(a), out_(new tgba_explicit_string(a->get_dict())), sm_(sm), - useless_(useless) - + useless_(useless), + useful_(useful), + strip_(strip) { - out_->copy_acceptance_conditions_of(a); + out_->set_acceptance_conditions(useful); } tgba_explicit_string* @@ -73,14 +75,17 @@ namespace spot // the destination state do not belong to an accepting state. if (sm_.accepting(sm_.scc_of_state(in_s)) && sm_.accepting(sm_.scc_of_state(out_s))) - out_->add_acceptance_conditions(t, - si->current_acceptance_conditions()); + out_->add_acceptance_conditions + (t, (bdd_exist(si->current_acceptance_conditions(), strip_) + & useful_)); } private: tgba_explicit_string* out_; const scc_map& sm_; const std::vector& useless_; + bdd useful_; + bdd strip_; }; } // anonymous @@ -91,7 +96,33 @@ namespace spot sm.build_map(); scc_stats ss = build_scc_stats(sm); - filter_iter fi(aut, sm, ss.useless_scc_map); + bdd useful = ss.useful_acc; + if (useful == bddfalse) + // Even if no acceptance conditions are useful in a SCC, + // we need to keep at least one acceptance conditions + useful = bdd_satone(aut->all_acceptance_conditions()); + + bdd positive = bddtrue; + bdd cur = useful; + while (cur != bddfalse) + { + bdd a = bdd_satone(cur); + cur -= a; + for (;;) + { + if (bdd_low(a) == bddfalse) + { + positive &= bdd_ithvar(bdd_var(a)); + break; + } + a = bdd_low(a); + } + } + + bdd strip = bdd_exist(bdd_support(aut->all_acceptance_conditions()), + positive); + useful = bdd_exist(useful, strip); + filter_iter fi(aut, sm, ss.useless_scc_map, useful, strip); fi.run(); tgba_explicit_string* res = fi.result(); res->merge_transitions();