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

graph: filter accepting sinks in univ_dest_mapper

Browse source
This commit is contained in:
Antoine Martin 2022-07-07 16:38:33 +02:00
parent 1b393aefad
commit f2a3ecab0d
1 changed files with 6 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

8
spot/graph/graph.hh
View file

@ -557,10 +557,11 @@ namespace spot
{
std::map<std::vector<unsigned>, unsigned> uniq_;
G& g_;
unsigned acc_sink_;
public:
univ_dest_mapper(G& graph)
: g_(graph)
univ_dest_mapper(G& graph, unsigned sink = -1u)
: g_(graph), acc_sink_(sink)
{
}
@ -570,6 +571,9 @@ namespace spot
std::vector<unsigned> tmp(begin, end);
std::sort(tmp.begin(), tmp.end());
tmp.erase(std::unique(tmp.begin(), tmp.end()), tmp.end());
if (acc_sink_ != -1u && tmp.size() > 1)
tmp.erase(std::remove(tmp.begin(), tmp.end(), acc_sink_),
tmp.end());
auto p = uniq_.emplace(tmp, 0);
if (p.second)
p.first->second = g_.new_univ_dests(tmp.begin(), tmp.end());