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

scc_filter: preserve state names and highlighted states

Browse source 
Suggested by Juraj Major.

* spot/twaalgos/sccfilter.cc: Here.
* tests/python/sccfilter.py: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention the news.
This commit is contained in:
Alexandre Duret-Lutz 2016-11-11 15:17:34 +01:00
parent dd706d7847
commit 85f6e0e158
4 changed files with 92 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

31
spot/twaalgos/sccfilter.cc
View file

@ -330,10 +330,37 @@ namespace spot
// has one initial state).
auto init = inout[aut->get_init_state_number()];
filtered->set_init_state(init < out_n ? init : filtered->new_state());
if (auto* names =
aut->get_named_prop<std::vector<std::string>>("state-names"))
{
std::cerr << "names\n";
unsigned size = names->size();
if (size > in_n)
size = in_n;
auto* new_names = new std::vector<std::string>(out_n);
filtered->set_named_prop("state-names", new_names);
for (unsigned s = 0; s < size; ++s)
{
unsigned new_s = inout[s];
if (new_s != -1U)
(*new_names)[new_s] = (*names)[s];
}
}
if (auto hs =
aut->get_named_prop<std::map<unsigned, unsigned>>("highlight-states"))
{
auto* new_hs = new std::map<unsigned, unsigned>;
filtered->set_named_prop("highlight-states", new_hs);
for (auto p: *hs)
{
unsigned new_s = inout[p.first];
if (new_s != -1U)
new_hs->emplace(new_s, p.second);
}
}
return filtered;
}
}
twa_graph_ptr