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

* src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::next):

Browse source 
Fix computation of states sharing the same accepting state.
This commit is contained in:
Alexandre Duret-Lutz 2003-07-09 14:05:49 +00:00
parent 2a8b1b7471
commit d14eee25bf
2 changed files with 17 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

3
ChangeLog
View file

@ -1,5 +1,8 @@
2003-07-09 Alexandre Duret-Lutz <aduret@src.lip6.fr> 2003-07-09 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::next):
Fix computation of states sharing the same accepting state.
Make sure we only output one initial state in LBTT's output. Make sure we only output one initial state in LBTT's output.
* src/tgbaalgos/lbtt.cc (fill_todo): Add the 'first' argument * src/tgbaalgos/lbtt.cc (fill_todo): Add the 'first' argument
to designate initial states. to designate initial states.

17
src/tgba/succiterconcrete.cc
View file

@ -100,10 +100,21 @@ namespace spot
bdd prop = bdd_exist(cube, data_.acc_set); bdd prop = bdd_exist(cube, data_.acc_set);
// prop = (!a)&b // prop = (!a)&b
current_acc_ = bdd_forall(bdd_restrict(as, prop), data_.var_set); current_acc_ = bdd_forall(bdd_restrict(as, prop), data_.var_set);
// acc = (Acc[a] | Acc[b]) // current_acc_ = (Acc[a] | Acc[b])
bdd all = as & current_acc_; assert(current_acc_ != bddfalse);
// Find other transitions included in each of these
// accepting sets.
bdd all = bddtrue;
bdd acc = current_acc_;
do
{
bdd one_acc = bdd_satone(acc);
acc &= !one_acc;
all &= bdd_relprod(as, one_acc, data_.acc_set);
}
while (acc != bddfalse);
// all = (a | (!a)&b) & (Acc[a] | Acc[b]) // all = (a | (!a)&b) & (Acc[a] | Acc[b])
current_ = bdd_exist(all, data_.acc_set) & dest; current_ = all & dest;
// current_ = (a | (!a)&b) & (Next...) // current_ = (a | (!a)&b) & (Next...)
} }
else else