From 52faa81a77844e6cab960add4138090116dba554 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 5 Mar 2010 22:27:36 +0100 Subject: [PATCH] Generalize the previous patch to accepting states in SBA. * src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator::sync_): Move the optimization step added by the previous patch outside the before the bddtrue check, so that it also applies to accepting states in SBA. --- ChangeLog | 9 +++++++++ src/tgba/tgbatba.cc | 28 +++++++++++++--------------- 2 files changed, 22 insertions(+), 15 deletions(-) diff --git a/ChangeLog b/ChangeLog index 5cf219b2d..7bdee08a2 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,12 @@ +2010-03-05 Alexandre Duret-Lutz + + Generalize the previous patch to accepting states in SBA. + + * src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator::sync_): Move + the optimization step added by the previous patch outside the + before the bddtrue check, so that it also applies to accepting + states in SBA. + 2010-03-03 Alexandre Duret-Lutz Optimize tgba_tba_proxy and tgba_sba_proxy for states that share diff --git a/src/tgba/tgbatba.cc b/src/tgba/tgbatba.cc index a17bdd867..ecc5b118d 100644 --- a/src/tgba/tgbatba.cc +++ b/src/tgba/tgbatba.cc @@ -181,6 +181,19 @@ namespace spot bdd acc = it_->current_acceptance_conditions(); + // As an extra optimization step, gather the acceptance + // conditions common to all outgoing transitions of the + // destination state, and pretend they are already present + // on this transition. + bdd common = aut_->all_acceptance_conditions(); + state* dest = it_->current_state(); + tgba_succ_iterator* dest_it = aut_->succ_iter(dest); + for (dest_it->first(); !dest_it->done(); dest_it->next()) + common &= dest_it->current_acceptance_conditions(); + acc |= common; + delete dest_it; + delete dest; + // bddtrue is a special condition used for tgba_sba_proxy // to denote the (N+1)th copy of the state, after all acceptance // conditions have been traversed. Such state is always accepting, @@ -205,21 +218,6 @@ namespace spot // address= {Paris, France}, // month = {December} // } - - - // As an extra optimization step, gather the acceptance - // conditions common to all outgoing transitions of the - // destination state, and pretend they are already present - // on this transition. - bdd common = aut_->all_acceptance_conditions(); - state* dest = it_->current_state(); - tgba_succ_iterator* dest_it = aut_->succ_iter(dest); - for (dest_it->first(); !dest_it->done(); dest_it->next()) - common &= dest_it->current_acceptance_conditions(); - acc |= common; - delete dest_it; - delete dest; - next_ = expected_; while (next_ != cycle_.end() && (acc & *next_) == *next_) ++next_;