From 509fb7e2a8a049b99940c48801c556fa08b4619e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 14 Jun 2012 15:17:45 +0200 Subject: [PATCH] * src/tgbaalgos/degen.cc: Use the new bdd_implies() function. --- src/tgbaalgos/degen.cc | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/tgbaalgos/degen.cc b/src/tgbaalgos/degen.cc index b5872ac68..f4336014b 100644 --- a/src/tgbaalgos/degen.cc +++ b/src/tgbaalgos/degen.cc @@ -284,10 +284,10 @@ namespace spot { unsigned prev = order.size() - 1; bdd common = outgoing.common_acc(s.first); - if ((common & order[prev]) == order[prev]) + if (bdd_implies(order[prev], common)) { bdd u = outgoing.union_acc(d.first); - if ((u & order[prev]) != order[prev]) + if (!bdd_implies(order[prev], u)) acc -= order[prev]; } } @@ -314,8 +314,7 @@ namespace spot // acceptance sets common to the outgoing transitions of // the destination state. acc |= otheracc; - while (next < order.size() - && (acc & order[next]) == order[next]) + while (next < order.size() && bdd_implies(order[next], acc)) ++next; d.second = next;