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

determinize: call bdd_implies less often

Browse source 
* spot/twaalgos/determinize.cc (safra_state::merge_redundant_states):
Test is_connected before called bdd_implies.
This commit is contained in:
Alexandre Duret-Lutz 2016-11-01 09:08:05 +01:00
parent d919b78c89
commit 3f64e9723f
1 changed files with 12 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

30
spot/twaalgos/determinize.cc
View file

@ -343,27 +343,21 @@ namespace spot
{ {
std::vector<int> to_remove; std::vector<int> to_remove;
for (auto& n1: nodes_) for (auto& n1: nodes_)
{ for (auto& n2: nodes_)
for (auto& n2: nodes_) {
{ if (n1 == n2)
if (n1 == n2) continue;
continue; // index to see if there is a path from scc2 -> scc1
// index to see if there is a path from scc2 -> scc1 unsigned idx = scc.scc_count() * scc.scc_of(n2.first) +
unsigned idx = scc.scc_count() * scc.scc_of(n2.first) + scc.scc_of(n1.first);
scc.scc_of(n1.first); if (!is_connected[idx] && bdd_implies(implications.at(n1.first),
if (bdd_implies(implications.at(n1.first), implications.at(n2.first)))
implications.at(n2.first)) && !is_connected[idx]) to_remove.push_back(n1.first);
{ }
to_remove.push_back(n1.first);
}
}
}
for (auto& n: to_remove) for (auto& n: to_remove)
{ {
for (auto& brace: nodes_[n]) for (auto& brace: nodes_[n])
{ --nb_braces_[brace];
--nb_braces_[brace];
}
nodes_.erase(n); nodes_.erase(n);
} }
} }