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

* src/tgbaalgos/degen.cc: Use the new bdd_implies() function.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2012-06-14 15:17:45 +02:00
parent b7c77dca31
commit 509fb7e2a8
1 changed files with 3 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/tgbaalgos/degen.cc
View file

@ -284,10 +284,10 @@ namespace spot
{ {
unsigned prev = order.size() - 1; unsigned prev = order.size() - 1;
bdd common = outgoing.common_acc(s.first); 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); bdd u = outgoing.union_acc(d.first);
if ((u & order[prev]) != order[prev]) if (!bdd_implies(order[prev], u))
acc -= order[prev]; acc -= order[prev];
} }
} }
@ -314,8 +314,7 @@ namespace spot
// acceptance sets common to the outgoing transitions of // acceptance sets common to the outgoing transitions of
// the destination state. // the destination state.
acc |= otheracc; acc |= otheracc;
while (next < order.size() while (next < order.size() && bdd_implies(order[next], acc))
&& (acc & order[next]) == order[next])
++next; ++next;
d.second = next; d.second = next;