diff --git a/NEWS b/NEWS index 6961859db..d0a637131 100644 --- a/NEWS +++ b/NEWS @@ -24,6 +24,12 @@ New in spot 1.1a (not yet released): Some illustrations of this point and the previous one can be found in the man page for ltl2tgba(1). + - There is a new function scc_filter_states() that removes all + useless states from a TGBA. It is actually an abbridged version + of scc_filter() that does not alter the acceptance conditions of + the automaton. scc_filter_state() should be used when + post-processing TGBAs that actually represent BAs. + * Bug fixes: - genltl --gh-r generated the wrong formulas due to a typo. diff --git a/src/tgbaalgos/postproc.cc b/src/tgbaalgos/postproc.cc index 5c77324e8..0d636c915 100644 --- a/src/tgbaalgos/postproc.cc +++ b/src/tgbaalgos/postproc.cc @@ -110,12 +110,20 @@ namespace spot scc_filter_ = 1; // Remove useless SCCs. - if (scc_filter_ > 0 || type_ == Monitor) - { - const tgba* s = scc_filter(a, scc_filter_ > 1); - delete a; - a = s; - } + if (type_ == Monitor) + { + // Do not bother about acceptance conditions, they we be + // ignored. + const tgba* s = scc_filter_states(a); + delete a; + a = s; + } + else if (scc_filter_ > 0) + { + const tgba* s = scc_filter(a, scc_filter_ > 1); + delete a; + a = s; + } if (type_ == Monitor) { diff --git a/src/tgbaalgos/sccfilter.cc b/src/tgbaalgos/sccfilter.cc index ee5a2e4ac..ae8f0cc72 100644 --- a/src/tgbaalgos/sccfilter.cc +++ b/src/tgbaalgos/sccfilter.cc @@ -65,6 +65,53 @@ namespace spot return out_aut->create_transition(in_f, out_f); } + template + class filter_iter_states: public tgba_reachable_iterator_depth_first + { + public: + typedef T output_t; + + filter_iter_states(const tgba* a, + const scc_map& sm, + const std::vector& useless) + : tgba_reachable_iterator_depth_first(a), + out_(new T(a->get_dict())), + sm_(sm), + useless_(useless) + { + a->get_dict()->register_all_variables_of(a, out_); + out_->set_acceptance_conditions(a->all_acceptance_conditions()); + } + + T* + result() + { + return out_; + } + + bool + want_state(const state* s) const + { + return !useless_[sm_.scc_of_state(s)]; + } + + void + process_link(const state* in_s, int in, + const state* out_s, int out, + const tgba_succ_iterator* si) + { + typename output_t::state::transition* t = + create_transition(this->aut_, out_, in_s, in, out_s, out); + t->condition = si->current_condition(); + t->acceptance_conditions = si->current_acceptance_conditions(); + } + + protected: + T* out_; + const scc_map& sm_; + const std::vector& useless_; + }; + template class filter_iter: public tgba_reachable_iterator_depth_first { @@ -495,4 +542,55 @@ namespace spot return ret; } + tgba* scc_filter_states(const tgba* aut, scc_map* given_sm) + { + scc_map* sm = given_sm; + if (!sm) + { + sm = new scc_map(aut); + sm->build_map(); + } + scc_stats ss = build_scc_stats(*sm); + + tgba* ret; + + const tgba_explicit_formula* af = + dynamic_cast(aut); + if (af) + { + filter_iter_states fi(af, *sm, + ss.useless_scc_map); + fi.run(); + tgba_explicit_formula* res = fi.result(); + res->merge_transitions(); + ret = res; + } + else + { + const tgba_explicit_string* as = + dynamic_cast(aut); + if (as) + { + filter_iter_states fi(aut, *sm, + ss.useless_scc_map); + fi.run(); + tgba_explicit_string* res = fi.result(); + res->merge_transitions(); + ret = res; + } + else + { + filter_iter_states fi(aut, *sm, + ss.useless_scc_map); + fi.run(); + tgba_explicit_number* res = fi.result(); + res->merge_transitions(); + ret = res; + } + } + if (!given_sm) + delete sm; + return ret; + } + } diff --git a/src/tgbaalgos/sccfilter.hh b/src/tgbaalgos/sccfilter.hh index 791d04052..04f2167b9 100644 --- a/src/tgbaalgos/sccfilter.hh +++ b/src/tgbaalgos/sccfilter.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et +// Copyright (C) 2009, 2010, 2012, 2013 Laboratoire de Recherche et // Developpement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -56,10 +56,24 @@ namespace spot /// variable are also removed from transitions entering an accepting /// SCC. ignored is a conjunction of positive variables that should /// be removed everywhere. + /// + /// \warning Calling scc_filter on a TGBA that has the SBA property + /// (i.e., transitions leaving accepting states are all marked as + /// accepting) may destroy this property. Use scc_filter_states() + /// instead. tgba* scc_filter(const tgba* aut, bool remove_all_useless = false, scc_map* given_sm = 0, bdd susp = bddtrue, bool early_susp = false, bdd ignored = bddtrue); + /// \brief Prune unaccepting SCCs. + /// + /// This is an abridged version of scc_filter(), that only remove + /// useless states, without touching at the acceptance conditions. + /// + /// Especially, if the input TGBA has the SBA property, (i.e., + /// transitions leaving accepting states are all marked as + /// accepting), then the output TGBA will also have that property. + tgba* scc_filter_states(const tgba* aut, scc_map* given_sm = 0); } #endif // SPOT_TGBAALGOS_SCC_HH