diff --git a/src/tgbaalgos/sccfilter.cc b/src/tgbaalgos/sccfilter.cc index 53f670ce5..997f56841 100644 --- a/src/tgbaalgos/sccfilter.cc +++ b/src/tgbaalgos/sccfilter.cc @@ -29,17 +29,23 @@ namespace spot { namespace { + static + state_explicit_number::transition* + create_transition(const tgba*, tgba_explicit_number* out_aut, + const state*, int in, const state*, int out) + { + return out_aut->create_transition(in, out); + } + static state_explicit_string::transition* create_transition(const tgba* aut, tgba_explicit_string* out_aut, - const state* in_s, int in, - const state* out_s, int out) + const state* in_s, int, const state* out_s, int) { - 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()); + const tgba_explicit_string* a = + static_cast(aut); + return out_aut->create_transition(a->get_label(in_s), + a->get_label(out_s)); } static @@ -193,7 +199,9 @@ namespace spot res->merge_transitions(); return res; } - else + const tgba_explicit_string* as = + dynamic_cast(aut); + if (as) { filter_iter fi(aut, sm, ss.useless_scc_map, useful, useless, @@ -203,6 +211,16 @@ namespace spot res->merge_transitions(); return res; } + else + { + filter_iter fi(aut, sm, ss.useless_scc_map, + useful, useless, + remove_all_useless); + fi.run(); + tgba_explicit_number* res = fi.result(); + res->merge_transitions(); + return res; + } } }