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

hoa: fix output

Browse source 
* src/tgbaalgos/hoaf.cc: Do not initialize acc_cond::mark_t with -1U.
This commit is contained in:
Alexandre Duret-Lutz 2014-11-18 18:51:58 +01:00
parent 45e9b96b66
commit e1d4522ca9
1 changed files with 10 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/tgbaalgos/hoaf.cc
View file

@ -107,7 +107,8 @@ namespace spot
{
auto src = todo.front();
todo.pop_front();
acc_cond::mark_t prev = -1U;
bool notfirst = false;
acc_cond::mark_t prev = 0U;
bool st_acc = true;
bdd sum = bddfalse;
bdd available = bddtrue;
@ -137,12 +138,17 @@ namespace spot
if (st_acc)
{
acc_cond::mark_t acc = i->current_acceptance_conditions();
if (prev != -1U && prev != acc)
if (notfirst && prev != acc)
{
st_acc = false;
}
else
{
notfirst = true;
prev = acc;
}
}
}
if (is_complete)
is_complete &= sum == bddtrue;