Create a new src/priv/ directory for private algorithms.

* README: Document it. * configure.ac: Generate src/priv/Makefile. * src/Makefile.am: Recurse into priv/. * src/priv/Makefile.am: New file. * src/misc/acccompl.cc, src/misc/acccompl.hh, src/misc/accconv.cc, src/misc/accconv.hh: Move to... * src/priv/acccompl.cc, src/priv/acccompl.hh, src/priv/accconv.cc, src/priv/accconv.hh: ... here. * src/misc/Makefile.am: Adjust. * src/tgbaalgos/scc.cc, src/tgbaalgos/simulation.cc: Adjust includes. * src/sanity/style.test: Make sure no public header file include a private one.
2013-06-24 20:55:40 +02:00 · 2013-06-24 20:55:40 +02:00 · f2078ac325
commit f2078ac325
parent 2ef8917ba5
12 changed files with 59 additions and 23 deletions
--- a/src/priv/acccompl.cc
+++ b/src/priv/acccompl.cc
@ -0,0 +1,84 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2012 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 <http://www.gnu.org/licenses/>.
+
+#include "acccompl.hh"
+
+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_;
+
+    // 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;
+    while (cond != bddtrue)
+    {
+      res &= bdd_nithvar(bdd_var(cond));
+      cond = bdd_high(cond);
+    }
+
+    cache_[acc] = res;
+
+    return res;
+  }
+
+} // End namespace spot.