alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Use tgba_explicit_numbered to create SCC-filtered automata.

Browse source 
* src/tgbaalgos/sccfilter.cc: tgba_explicit_numbered replace
tgba_explicit_string for the general case.  This way we don't have to
prefix the result of format_state() in case to states have the same
description.  We just number the states instead.  For the specific
cases where the input automata are instance of tgba_explicit_string or
tgba_explicit_formula, we clone the label.
This commit is contained in:
Alexandre Duret-Lutz 2012-05-23 17:00:28 +02:00
parent 988e7e2499
commit 04cc63cac2
1 changed files with 26 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

34
src/tgbaalgos/sccfilter.cc
View file

@ -29,17 +29,23 @@ namespace spot
{ {
namespace 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 static
state_explicit_string::transition* state_explicit_string::transition*
create_transition(const tgba* aut, tgba_explicit_string* out_aut, create_transition(const tgba* aut, tgba_explicit_string* out_aut,
const state* in_s, int in, const state* in_s, int, const state* out_s, int)
const state* out_s, int out)
{ {
std::ostringstream in_name; const tgba_explicit_string* a =
in_name << "(#" << in << ") " << aut->format_state(in_s); static_cast<const tgba_explicit_string*>(aut);
std::ostringstream out_name; return out_aut->create_transition(a->get_label(in_s),
out_name << "(#" << out << ") " << aut->format_state(out_s); a->get_label(out_s));
return out_aut->create_transition(in_name.str(), out_name.str());
} }
static static
@ -193,7 +199,9 @@ namespace spot
res->merge_transitions(); res->merge_transitions();
return res; return res;
} }
else const tgba_explicit_string* as =
dynamic_cast<const tgba_explicit_string*>(aut);
if (as)
{ {
filter_iter<tgba_explicit_string> fi(aut, sm, ss.useless_scc_map, filter_iter<tgba_explicit_string> fi(aut, sm, ss.useless_scc_map,
useful, useless, useful, useless,
@ -203,6 +211,16 @@ namespace spot
res->merge_transitions(); res->merge_transitions();
return res; return res;
} }
else
{
filter_iter<tgba_explicit_number> 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;
}
} }
} }