From 81e0872b5dba116a11ae95ade19e66b11413df64 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 23 Nov 2009 10:19:38 +0100 Subject: [PATCH] Specialize scc_filter when handling tgba_explicit_formula automata. If the input is a tgba_explicit_formula we can output a tgba_explicit_formula too, and we want to do that because it is more space efficient. * src/tgba/tgbaexplicit.hh (get_label): New method. * src/tgbaalgos/sccfilter.cc (create_transition): New function, to handle tgba_explicit_formula and tgba_explicit_string output differently. (filter_iter): Template it on the output tgba type, and adjust to call create_transition. (scc_filter): Use filter_iter or filter_iter depending on the input tgba type. --- ChangeLog | 18 +++++++++ src/tgba/tgbaexplicit.hh | 14 +++++++ src/tgbaalgos/sccfilter.cc | 76 +++++++++++++++++++++++++++++++------- 3 files changed, 94 insertions(+), 14 deletions(-) diff --git a/ChangeLog b/ChangeLog index 7b454d56e..461add2ab 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,21 @@ +2009-11-23 Alexandre Duret-Lutz + + Specialize scc_filter when handling tgba_explicit_formula automata. + + If the input is a tgba_explicit_formula we can output a + tgba_explicit_formula too, and we want to do that because it is + more space efficient. + + * src/tgba/tgbaexplicit.hh (get_label): New method. + * src/tgbaalgos/sccfilter.cc (create_transition): New function, + to handle tgba_explicit_formula and tgba_explicit_string output + differently. + (filter_iter): Template it on the output tgba type, and adjust + to call create_transition. + (scc_filter): Use filter_iter or + filter_iter depending on the input tgba + type. + 2009-11-20 Alexandre Duret-Lutz Strip useless acceptance conditions in scc_filter(). diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh index 3bfb28e7b..202441744 100644 --- a/src/tgba/tgbaexplicit.hh +++ b/src/tgba/tgbaexplicit.hh @@ -181,6 +181,20 @@ namespace spot return name_state_map_.find(name) != name_state_map_.end(); } + const label& get_label(const tgba_explicit::state* s) const + { + typename sn_map::const_iterator i = state_name_map_.find(s); + assert(i != state_name_map_.end()); + return i->second; + } + + const label& get_label(const spot::state* s) const + { + const state_explicit* se = dynamic_cast(s); + assert(se); + return get_label(se->get_state()); + } + /// Return the tgba_explicit::state for \a name, creating the state if /// it does not exist. state* add_state(const label& name) diff --git a/src/tgbaalgos/sccfilter.cc b/src/tgbaalgos/sccfilter.cc index 3144e0ffd..a749da501 100644 --- a/src/tgbaalgos/sccfilter.cc +++ b/src/tgbaalgos/sccfilter.cc @@ -28,6 +28,36 @@ namespace spot { namespace { + static + tgba_explicit::transition* + create_transition(const tgba* aut, tgba_explicit_string* out_aut, + const state* in_s, int in, + const state* out_s, int out) + { + std::ostringstream in_name; + in_name << "(#" << in << ") " << aut->format_state(in_s); + std::ostringstream out_name; + out_name << "(#" << out << ") " << aut->format_state(out_s); + return out_aut->create_transition(in_name.str(), out_name.str()); + } + + static + tgba_explicit::transition* + create_transition(const tgba* aut, tgba_explicit_formula* out_aut, + const state* in_s, int, const state* out_s, int) + { + const tgba_explicit_formula* a = + static_cast(aut); + const ltl::formula* in_f = a->get_label(in_s); + const ltl::formula* out_f = a->get_label(out_s); + if (!out_aut->has_state(in_f)) + in_f->clone(); + if (!out_aut->has_state(out_f)) + out_f->clone(); + return out_aut->create_transition(in_f, out_f); + } + + template class filter_iter: public tgba_reachable_iterator_depth_first { public: @@ -36,7 +66,7 @@ namespace spot const std::vector& useless, bdd useful, bdd strip) : tgba_reachable_iterator_depth_first(a), - out_(new tgba_explicit_string(a->get_dict())), + out_(new T(a->get_dict())), sm_(sm), useless_(useless), useful_(useful), @@ -45,7 +75,7 @@ namespace spot out_->set_acceptance_conditions(useful); } - tgba_explicit_string* + T* result() { return out_; @@ -62,13 +92,8 @@ namespace spot const state* out_s, int out, const tgba_succ_iterator* si) { - std::ostringstream in_name; - in_name << "(#" << in << ") " << this->automata_->format_state(in_s); - std::ostringstream out_name; - out_name << "(#" << out << ") " << this->automata_->format_state(out_s); - tgba_explicit::transition* t = - out_->create_transition(in_name.str(), out_name.str()); + create_transition(this->automata_, out_, in_s, in, out_s, out); out_->add_conditions(t, si->current_condition()); // Do not output any acceptance condition if either the source or @@ -81,12 +106,13 @@ namespace spot } private: - tgba_explicit_string* out_; + T* out_; const scc_map& sm_; const std::vector& useless_; bdd useful_; bdd strip_; }; + } // anonymous @@ -122,11 +148,33 @@ namespace spot 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(); - return res; + + // In most cases we will create a tgba_explicit_string copy of the + // initial tgba, but this is not very space efficient as the + // labels are built using the "format_state()" string output of + // the original automaton. In the case where the source automaton is + // a tgba_explicit_formula (typically after calling ltl2tgba_fm()) + // we can create another tgba_explicit_formula instead. + const tgba_explicit_formula* af = + dynamic_cast(aut); + if (af) + { + filter_iter fi(af, sm, ss.useless_scc_map, + useful, strip); + fi.run(); + tgba_explicit_formula* res = fi.result(); + res->merge_transitions(); + return res; + } + else + { + filter_iter fi(aut, sm, ss.useless_scc_map, + useful, strip); + fi.run(); + tgba_explicit_string* res = fi.result(); + res->merge_transitions(); + return res; + } }