diff --git a/ChangeLog b/ChangeLog index 7908650f3..232401a78 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,12 @@ 2003-07-07 Alexandre Duret-Lutz + * src/tgba/succiterconcrete.hh + (tgba_succ_iterator_concrete::current_acc_): New attribute. + * src/tgba/succiterconcrete.cc + (tgba_succ_iterator_concrete::next): Set current_acc_. + (tgba_succ_iterator_concrete::current_accepting_conditions): + Simply return it. + * configure.ac: Output iface/Makefile and iface/gspn/Makefile. * iface/Makefile.am, iface/gspn/Makefile.am: New files. * Makefile.am (SUBDIRS): Add iface. diff --git a/src/tgba/succiterconcrete.cc b/src/tgba/succiterconcrete.cc index 6f09debc8..432fcc1c8 100644 --- a/src/tgba/succiterconcrete.cc +++ b/src/tgba/succiterconcrete.cc @@ -99,13 +99,17 @@ namespace spot // cube = (!ab & Acc[a]) bdd prop = bdd_exist(cube, data_.acc_set); // prop = (!a)&b - bdd 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]) - bdd all = as & acc; + bdd all = as & current_acc_; // all = (a | (!a)&b) & (Acc[a] | Acc[b]) current_ = bdd_exist(all, data_.acc_set) & dest; // current_ = (a | (!a)&b) & (Next...) } + else + { + current_acc_ = bddfalse; + } assert(current_ != bddfalse); // The destination state, computed here, should be compatible @@ -142,10 +146,7 @@ namespace spot tgba_succ_iterator_concrete::current_accepting_conditions() { assert(!done()); - return bdd_exist(bdd_forall(bdd_restrict(data_.accepting_conditions, - current_), - data_.var_set), - data_.notacc_set); + return current_acc_; } } diff --git a/src/tgba/succiterconcrete.hh b/src/tgba/succiterconcrete.hh index 8b18389d0..4f78f8ec7 100644 --- a/src/tgba/succiterconcrete.hh +++ b/src/tgba/succiterconcrete.hh @@ -42,6 +42,8 @@ namespace spot /// atomic proposition and Next variables. bdd current_state_; ///< \brief Current successor, as a /// conjunction of Now variables. + bdd current_acc_; ///< \brief Accepting condition for the current + /// transition. }; }