diff --git a/src/priv/Makefile.am b/src/priv/Makefile.am index 6cec370d0..595c82701 100644 --- a/src/priv/Makefile.am +++ b/src/priv/Makefile.am @@ -21,8 +21,6 @@ AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS) AM_CXXFLAGS = $(WARNING_CXXFLAGS) noinst_HEADERS = \ - acccompl.hh \ - accconv.hh \ accmap.hh \ bddalloc.hh \ countstates.hh \ @@ -30,10 +28,6 @@ noinst_HEADERS = \ noinst_LTLIBRARIES = libpriv.la libpriv_la_SOURCES = \ - acccompl.cc \ - accconv.cc \ bddalloc.cc \ countstates.cc \ freelist.cc - - diff --git a/src/priv/acccompl.cc b/src/priv/acccompl.cc deleted file mode 100644 index 17c01e1fa..000000000 --- a/src/priv/acccompl.cc +++ /dev/null @@ -1,88 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2012, 2014 Laboratoire de Recherche et Developpement -// de l'Epita (LRDE) -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -#include "acccompl.hh" -#include - -namespace spot -{ - // 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; - - while (n != bddfalse) - { - bdd cond = bdd_satone(n); - bdd oldcond = cond; - n -= cond; - - while (bdd_high(cond) == bddfalse) - cond = bdd_low(cond); - - // Here we want to keep only the current one. - // tmp is only useful to keep the value and cache it. - bdd tmp = bdd_ithvar(bdd_var(cond)); - res &= tmp; - } - - cache_[acc] = res; - - return res; - } - - bdd acc_compl::reverse_complement(const bdd& acc) - { - // We are sure that if we have no acceptance condition the result - // is all_. - if (acc == bddtrue) - return all_; - - assert(acc != bddfalse); - - // Since we never cache a unique positive bdd, we can reuse the - // 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; - bdd neg = bddtrue; - while (cond != bddtrue) - { - neg &= bdd_nithvar(bdd_var(cond)); - cond = bdd_high(cond); - } - res &= neg; - cache_[acc] = res; - - return res; - } - -} // End namespace spot. diff --git a/src/priv/acccompl.hh b/src/priv/acccompl.hh deleted file mode 100644 index f65bf1074..000000000 --- a/src/priv/acccompl.hh +++ /dev/null @@ -1,56 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et -// Developpement de l'Epita (LRDE) -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - - -#ifndef SPOT_PRIV_ACCCOMPL_HH -# define SPOT_PRIV_ACCCOMPL_HH - -#include -#include -#include "misc/hash.hh" -#include "misc/bddlt.hh" - -namespace spot -{ - /// \brief Helper class to convert acceptance conditions into promises - /// - /// A set of acceptance conditions represented by the sum "à la Spot", - /// is converted into a product of promises. - class acc_compl - { - public: - acc_compl(const bdd& all, const bdd& neg) - : all_(all), - neg_(neg) - { - } - - - bdd complement(const bdd& acc); - bdd reverse_complement(const bdd& acc); - - protected: - const bdd all_; - const bdd neg_; - typedef std::unordered_map bdd_cache_t; - bdd_cache_t cache_; - }; -} // End namespace Spot - -#endif // SPOT_PRIV_ACCCOMPL_HH diff --git a/src/priv/accconv.cc b/src/priv/accconv.cc deleted file mode 100644 index 6a760f462..000000000 --- a/src/priv/accconv.cc +++ /dev/null @@ -1,80 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement -// de l'Epita (LRDE) -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -#include -#include "accconv.hh" - -namespace spot -{ - bdd acceptance_convertor::as_positive_product(bdd acc) - { - // Cache lookup. - bdd_cache_t::const_iterator it = pos_prod_cache_.find(acc); - if (it != pos_prod_cache_.end()) - return it->second; - - // This would be one way to construct the positive product, - // if we did not want to populate a cache. - // - // bdd res = bddtrue; - // BDD a = acc.id(); - // while (a) - // { - // if (bdd_high(a)) - // res &= bdd_ithvar(bdd_var(a)); - // a = bdd_low(a); - // } - - // Skip all negative variables. - bdd a = acc; - while (a != bddfalse && bdd_high(a) == bddfalse) - a = bdd_low(a); - - bdd res = bddtrue; - if (a != bddfalse) - { - // Make a recursive call right below each positive variable, - // in order to populate the cache. - res = bdd_ithvar(bdd_var(a)); - bdd low = bdd_low(a); - if (low != bddfalse) - res &= as_positive_product(low); - } - - // Cache final result. - pos_prod_cache_[acc] = res; - return res; - }; - - bdd acceptance_convertor::as_full_product(bdd acc) - { - // Lookup in cache. - bdd_cache_t::const_iterator it = full_prod_cache_.find(acc); - if (it != full_prod_cache_.end()) - return it->second; - - bdd pos = as_positive_product(acc); - bdd res = bdd_exist(allneg_, pos) & pos; - - // Cache final result. - full_prod_cache_[acc] = res; - return res; - } - -} diff --git a/src/priv/accconv.hh b/src/priv/accconv.hh deleted file mode 100644 index 639b8a5d2..000000000 --- a/src/priv/accconv.hh +++ /dev/null @@ -1,52 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et -// Developpement de l'Epita (LRDE) -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -#ifndef SPOT_PRIV_ACCCONV_HH -# define SPOT_PRIV_ACCCONV_HH - -#include -#include "misc/hash.hh" -#include "misc/bddlt.hh" - -namespace spot -{ - /// \brief Help class to convert between acceptance conditions to - /// other BDD formats. - class acceptance_convertor - { - public: - acceptance_convertor(bdd allneg) - : allneg_(allneg) - { - } - - bdd as_positive_product(bdd acc); - - bdd as_full_product(bdd acc); - - protected: - bdd allneg_; - typedef std::unordered_map bdd_cache_t; - bdd_cache_t pos_prod_cache_; - bdd_cache_t full_prod_cache_; - }; - -} - -#endif // SPOT_PRIV_ACCCONV_HH diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index 3e71b7d80..842a459e9 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -39,7 +39,6 @@ #include "tgba/bddprint.hh" #include "tgbaalgos/sccinfo.hh" //#include "tgbaalgos/dotty.hh" -#include "priv/acccompl.hh" namespace spot { diff --git a/src/tgbaalgos/scc.cc b/src/tgbaalgos/scc.cc index 14806bf80..d6c847109 100644 --- a/src/tgbaalgos/scc.cc +++ b/src/tgbaalgos/scc.cc @@ -24,7 +24,6 @@ #include "scc.hh" #include "tgba/bddprint.hh" #include "misc/escape.hh" -#include "priv/accconv.hh" namespace spot { diff --git a/src/tgbaalgos/sccinfo.cc b/src/tgbaalgos/sccinfo.cc index 8b6faa362..c8f8a7fb1 100644 --- a/src/tgbaalgos/sccinfo.cc +++ b/src/tgbaalgos/sccinfo.cc @@ -23,7 +23,6 @@ #include #include "tgba/bddprint.hh" #include "misc/escape.hh" -#include "priv/accconv.hh" namespace spot { diff --git a/src/tgbaalgos/simulation.cc b/src/tgbaalgos/simulation.cc index c8e07b8f8..9dccbd66a 100644 --- a/src/tgbaalgos/simulation.cc +++ b/src/tgbaalgos/simulation.cc @@ -23,13 +23,13 @@ #include #include #include "simulation.hh" -#include "priv/acccompl.hh" #include "misc/minato.hh" #include "tgba/bddprint.hh" #include "tgbaalgos/reachiter.hh" #include "tgbaalgos/sccfilter.hh" #include "tgbaalgos/sccinfo.hh" #include "tgbaalgos/dupexp.hh" +#include "misc/bddlt.hh" // The way we developed this algorithm is the following: We take an // automaton, and reverse all these acceptance conditions. We reverse