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

* src/tgba/succiterconcrete.cc, src/tgba/tgbaexplicit.cc,

Browse source 
src/tgba/tgbatba.cc, src/tgbaalgos/lbtt.cc: Use `-' instead of `& !'
between two BDDs.  That's one less call to BuDDy.
This commit is contained in:
Alexandre Duret-Lutz 2003-08-10 13:09:50 +00:00
parent 63c62e1767
commit 317fed597b
6 changed files with 15 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

4
ChangeLog
View file

@ -1,5 +1,9 @@
2003-08-10 Alexandre Duret-Lutz <aduret@src.lip6.fr> 2003-08-10 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgba/succiterconcrete.cc, src/tgba/tgbaexplicit.cc,
src/tgba/tgbatba.cc, src/tgbaalgos/lbtt.cc: Use `-' instead of `& !'
between two BDDs. That's one less call to BuDDy.
* src/tgbatest/tgbaread.test, src/tgbatest/explicit.test: * src/tgbatest/tgbaread.test, src/tgbatest/explicit.test:
Adjust expected output after 2003-08-07's change. Adjust expected output after 2003-08-07's change.

2
src/tgba/bdddict.cc
View file

@ -28,7 +28,7 @@ namespace spot
fv_map::iterator sii = var_map.find(f); fv_map::iterator sii = var_map.find(f);
if (sii != var_map.end()) if (sii != var_map.end())
{ {
num = sii->second; num = sii->second;
} }
else else
{ {

8
src/tgba/succiterconcrete.cc
View file

@ -66,11 +66,11 @@ namespace spot
do do
{ {
// FIXME: Iterating on the successors this way (calling // FIXME: Iterating on the successors this way (calling
// bdd_satone{,set} and NANDing out the result from a // bdd_satone{,set} and NANDing out (-=) the result from a
// set) requires several descent of the BDD. Maybe it would be // set) requires several descent of the BDD. Maybe it would be
// faster to compute all satisfying formula in one operation. // faster to compute all satisfying formula in one operation.
succ_set_left_ &= !current_; succ_set_left_ -= current_;
if (succ_set_left_ == bddfalse) // No more successors? if (succ_set_left_ == bddfalse) // No more successors?
return; return;
@ -113,7 +113,7 @@ namespace spot
// So, first, filter out all transitions like p, which // So, first, filter out all transitions like p, which
// are also in other accepting sets. // are also in other accepting sets.
bdd fout = bdd_relprod(as, !current_acc_, data_.acc_set); bdd fout = bdd_relprod(as, !current_acc_, data_.acc_set);
bdd as_fout = as & !fout; bdd as_fout = as - fout;
// Then, pick the remaining term that are exactly in all // Then, pick the remaining term that are exactly in all
// required accepting sets. // required accepting sets.
bdd all = bddtrue; bdd all = bddtrue;
@ -121,7 +121,7 @@ namespace spot
do do
{ {
bdd one_acc = bdd_satone(acc); bdd one_acc = bdd_satone(acc);
acc &= !one_acc; acc -= one_acc;
all &= bdd_relprod(as_fout, one_acc, data_.acc_set); all &= bdd_relprod(as_fout, one_acc, data_.acc_set);
} }
while (acc != bddfalse); while (acc != bddfalse);

2
src/tgba/tgbaexplicit.cc
View file

@ -151,7 +151,7 @@ namespace spot
void void
tgba_explicit::add_neg_condition(transition* t, ltl::formula* f) tgba_explicit::add_neg_condition(transition* t, ltl::formula* f)
{ {
t->condition &= ! get_condition(f); t->condition -= get_condition(f);
} }
void void

4
src/tgba/tgbatba.cc
View file

@ -156,14 +156,14 @@ namespace spot
// Now build the "cycle" of accepting conditions. // Now build the "cycle" of accepting conditions.
bdd last = bdd_satone(all); bdd last = bdd_satone(all);
all &= !last; all -= last;
acc_cycle_[bddtrue] = last; acc_cycle_[bddtrue] = last;
while (all != bddfalse) while (all != bddfalse)
{ {
bdd next = bdd_satone(all); bdd next = bdd_satone(all);
all &= !next; all -= next;
acc_cycle_[last] = next; acc_cycle_[last] = next;
last = next; last = next;
} }

6
src/tgbaalgos/lbtt.cc
View file

@ -24,7 +24,7 @@ namespace spot
while (all_acc != bddfalse) while (all_acc != bddfalse)
{ {
bdd acc = bdd_satone(all_acc); bdd acc = bdd_satone(all_acc);
all_acc &= !acc; all_acc -= acc;
sm[acc] = count++; sm[acc] = count++;
} }
} }
@ -35,7 +35,7 @@ namespace spot
while (b != bddfalse) while (b != bddfalse)
{ {
bdd acc = bdd_satone(b); bdd acc = bdd_satone(b);
b &= !acc; b -= acc;
os << sm[acc] << " "; os << sm[acc] << " ";
} }
return os; return os;
@ -65,7 +65,7 @@ namespace spot
else else
{ {
bdd cube = bdd_satone(b); bdd cube = bdd_satone(b);
b &= !cube; b -= cube;
if (b != bddfalse) if (b != bddfalse)
{ {
return "| " + bdd_to_lbtt(b, d) + " " + bdd_to_lbtt(cube, d); return "| " + bdd_to_lbtt(b, d) + " " + bdd_to_lbtt(cube, d);