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

powerset: simplify an implication check

Browse source 
* src/tgbaalgos/powerset.cc: Use bdd_implies.
This commit is contained in:
Alexandre Duret-Lutz 2015-01-11 19:14:32 +01:00
parent 6f7f9ef8bc
commit 2377523c02
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/tgbaalgos/powerset.cc
View file

@ -81,8 +81,8 @@ namespace spot
// Construct the set of all states reachable via COND. // Construct the set of all states reachable via COND.
power_state dest; power_state dest;
for (auto s: src) for (auto s: src)
for (auto si: aut->out(s)) for (auto& si: aut->out(s))
if ((cond >> si.cond) == bddtrue) if (bdd_implies(cond, si.cond))
dest.insert(si.dst); dest.insert(si.dst);
if (dest.empty()) if (dest.empty())
continue; continue;