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

* src/twa/acc.cc: Fix BDD conversion in case of unused sets.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2015-04-27 14:23:19 +02:00
parent 0ede968760
commit 6e32b65875
1 changed files with 9 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/twa/acc.cc
View file

@ -412,13 +412,14 @@ namespace spot
auto used = acc_cond::acc_code::used_sets(); auto used = acc_cond::acc_code::used_sets();
unsigned c = used.count(); unsigned c = used.count();
unsigned max = used.max_set();
bdd_allocator ba; bdd_allocator ba;
int base = ba.allocate_variables(c); int base = ba.allocate_variables(c);
assert(base == 0); assert(base == 0);
std::vector<bdd> r; std::vector<bdd> r;
std::vector<unsigned> sets(c); std::vector<unsigned> sets(c);
for (unsigned i = 0; r.size() < c; ++i) for (unsigned i = 0; r.size() < max; ++i)
{ {
if (used.has(i)) if (used.has(i))
{ {
@ -473,6 +474,7 @@ namespace spot
c.append_or(std::move(rescode)); c.append_or(std::move(rescode));
std::swap(c, rescode); std::swap(c, rescode);
} }
return rescode; return rescode;
} }
@ -483,13 +485,14 @@ namespace spot
auto used = acc_cond::acc_code::used_sets(); auto used = acc_cond::acc_code::used_sets();
unsigned c = used.count(); unsigned c = used.count();
unsigned max = used.max_set();
bdd_allocator ba; bdd_allocator ba;
int base = ba.allocate_variables(c); int base = ba.allocate_variables(c);
assert(base == 0); assert(base == 0);
std::vector<bdd> r; std::vector<bdd> r;
std::vector<unsigned> sets(c); std::vector<unsigned> sets(c);
for (unsigned i = 0; r.size() < c; ++i) for (unsigned i = 0; r.size() < max; ++i)
{ {
if (used.has(i)) if (used.has(i))
{ {
@ -555,13 +558,14 @@ namespace spot
auto used = acc_cond::acc_code::used_sets(); auto used = acc_cond::acc_code::used_sets();
unsigned c = used.count(); unsigned c = used.count();
unsigned max = used.max_set();
bdd_allocator ba; bdd_allocator ba;
int base = ba.allocate_variables(c); int base = ba.allocate_variables(c);
assert(base == 0); assert(base == 0);
std::vector<bdd> r; std::vector<bdd> r;
std::vector<unsigned> sets(c); std::vector<unsigned> sets(c);
for (unsigned i = 0; r.size() < c; ++i) for (unsigned i = 0; r.size() < max; ++i)
{ {
if (used.has(i)) if (used.has(i))
{ {
@ -616,6 +620,7 @@ namespace spot
} }
auto used = acc_cond::acc_code::used_sets(); auto used = acc_cond::acc_code::used_sets();
unsigned c = used.count(); unsigned c = used.count();
unsigned max = used.max_set();
bdd_allocator ba; bdd_allocator ba;
int base = ba.allocate_variables(c); int base = ba.allocate_variables(c);
@ -623,7 +628,7 @@ namespace spot
std::vector<bdd> r; std::vector<bdd> r;
std::vector<unsigned> sets(c); std::vector<unsigned> sets(c);
bdd known = bddtrue; bdd known = bddtrue;
for (unsigned i = 0; r.size() < c; ++i) for (unsigned i = 0; r.size() < max; ++i)
{ {
if (used.has(i)) if (used.has(i))
{ {