From 2377523c02eb9eecdc7e0cb4a7eaecd3d1c0a792 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 11 Jan 2015 19:14:32 +0100 Subject: [PATCH] powerset: simplify an implication check * src/tgbaalgos/powerset.cc: Use bdd_implies. --- src/tgbaalgos/powerset.cc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/tgbaalgos/powerset.cc b/src/tgbaalgos/powerset.cc index 1ecb5d08b..ca257cf00 100644 --- a/src/tgbaalgos/powerset.cc +++ b/src/tgbaalgos/powerset.cc @@ -81,8 +81,8 @@ namespace spot // Construct the set of all states reachable via COND. power_state dest; for (auto s: src) - for (auto si: aut->out(s)) - if ((cond >> si.cond) == bddtrue) + for (auto& si: aut->out(s)) + if (bdd_implies(cond, si.cond)) dest.insert(si.dst); if (dest.empty()) continue;