diff --git a/src/misc/acccompl.cc b/src/misc/acccompl.cc index aee09f31d..3212f5718 100644 --- a/src/misc/acccompl.cc +++ b/src/misc/acccompl.cc @@ -21,32 +21,18 @@ namespace spot { - // The algorithm of this method is simple. We explain this in - // bottom/up. - // Internally, the bdd is represented like a tree. There is two - // output: high(1) and low (0). An acceptance condition is like - // the following: - // if all has three acceptance conditions, all is equal to - // "a!b!c + !ab!c + !a!bc". - // So, to compute the negation of an acceptance condition, say "a!b!c" - // we need to know wich one is go to one when true. So we are looping - // through the conditions until bdd_high is true. - // Once found, we keep only it. - bdd acc_compl::complement(const bdd acc) + // If ALL = a!b!c + !ab!c + !a!bc", the negation of ACC = a!b!c is + // RES = bc. We do that by computing ALL-ACC and enumerating + // all positive variables in the remaining products. + bdd acc_compl::complement(const bdd& acc) { bdd_cache_t::const_iterator it = cache_.find(acc); if (it != cache_.end()) return it->second; bdd res = bddtrue; - bdd n = all_ - acc; - // This means, if acc == all, the opposite is bddfalse, and not - // bddtrue. - if (n == bddfalse) - res = bddtrue; - while (n != bddfalse) { bdd cond = bdd_satone(n); @@ -67,41 +53,27 @@ namespace spot return res; } - - bdd acc_compl::reverse_complement(const bdd acc) + bdd acc_compl::reverse_complement(const bdd& acc) { - // We are sure that if we have no acceptance condition - // the result is all_. + // We are sure that if we have no acceptance condition the result + // is all_. if (acc == bddtrue) return all_; // Since we never cache a unique positive bdd, we can reuse the - // same cache. - // In fact the only kind of acc we will received in this method, - // are a conjunction of positive acceptance condition. - // I mean: "ab" and not "a!b + !ab" + // same cache. In fact the only kind of acc we will receive in + // this method, are a conjunction of positive acceptance + // conditions. (i.e., "ab" and not "a!b + !ab") bdd_cache_t::const_iterator it = cache_.find(acc); if (it != cache_.end()) return it->second; bdd res = all_; bdd cond = acc; - while (cond != bddtrue) { - bdd one; - - one = bdd_ithvar(bdd_var(cond)); - - // Because it is a conjunction of positive bdd, we just have to - // traverse through the high branch. + res &= bdd_nithvar(bdd_var(cond)); cond = bdd_high(cond); - - // We remove the current `one' from the `neg_' and we associate - // `one'. - bdd n = bdd_exist(neg_, one) & one; - - res -= n; } cache_[acc] = res; diff --git a/src/misc/acccompl.hh b/src/misc/acccompl.hh index af66ed984..b8d30e0f5 100644 --- a/src/misc/acccompl.hh +++ b/src/misc/acccompl.hh @@ -35,19 +35,19 @@ namespace spot class acc_compl { public: - acc_compl(bdd all, bdd neg) + acc_compl(const bdd& all, const bdd& neg) : all_(all), neg_(neg) { } - bdd complement(const bdd acc); - bdd reverse_complement(const bdd acc); + bdd complement(const bdd& acc); + bdd reverse_complement(const bdd& acc); protected: - bdd all_; - bdd neg_; + const bdd all_; + const bdd neg_; typedef Sgi::hash_map bdd_cache_t; bdd_cache_t cache_; };