From d14eee25bff91f5bc31adf571467997f71a8f259 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 9 Jul 2003 14:05:49 +0000 Subject: [PATCH] * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::next): Fix computation of states sharing the same accepting state. --- ChangeLog | 3 +++ src/tgba/succiterconcrete.cc | 17 ++++++++++++++--- 2 files changed, 17 insertions(+), 3 deletions(-) diff --git a/ChangeLog b/ChangeLog index faf0192eb..c70af461d 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,8 @@ 2003-07-09 Alexandre Duret-Lutz + * 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. * src/tgbaalgos/lbtt.cc (fill_todo): Add the 'first' argument to designate initial states. diff --git a/src/tgba/succiterconcrete.cc b/src/tgba/succiterconcrete.cc index d526dd5ff..2c85649c3 100644 --- a/src/tgba/succiterconcrete.cc +++ b/src/tgba/succiterconcrete.cc @@ -100,10 +100,21 @@ namespace spot bdd prop = bdd_exist(cube, data_.acc_set); // prop = (!a)&b current_acc_ = bdd_forall(bdd_restrict(as, prop), data_.var_set); - // acc = (Acc[a] | Acc[b]) - bdd all = as & current_acc_; + // current_acc_ = (Acc[a] | Acc[b]) + 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]) - current_ = bdd_exist(all, data_.acc_set) & dest; + current_ = all & dest; // current_ = (a | (!a)&b) & (Next...) } else