Add a class to convert a bdd into its complement.

* src/misc/acccompl.cc, src/misc/acccompl.hh: Add a way to
an acceptance condition in an automaton, into its
complement.
Create a method to make the reverse operation.
* src/misc/Makefile.am: Add the new files to the compilation.

src/misc/Makefile.am

@@ -30,6 +30,7 @@ nodist_misc_HEADERS = _config.h
 DISTCLEANFILES = _config.h
 
 misc_HEADERS = \
+  acccompl.hh \
   accconv.hh \
   bareword.hh \
   bddalloc.hh \
@@ -55,6 +56,7 @@ misc_HEADERS = \
 
 noinst_LTLIBRARIES = libmisc.la
 libmisc_la_SOURCES = \
+  acccompl.cc \
   accconv.cc \
   bareword.cc \
   bddalloc.cc \

src/misc/acccompl.cc

@@ -0,0 +1,116 @@
+// -*- 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#include "acccompl.hh"
+#include "tgba/tgbaexplicit.hh"
+
+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 AccCompl::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);
+      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 AccCompl::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 received in this method,
+    // are a conjunction of positive acceptance condition.
+    // I mean: "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.
+      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;
+
+    return res;
+  }
+
+} // End namespace spot.

src/misc/acccompl.hh

@@ -0,0 +1,58 @@
+// -*- 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+
+#ifndef SPOT_MISC_ACCCOMPL_HH
+# define SPOT_MISC_ACCCOMPL_HH
+
+#include <map>
+#include <bdd.h>
+#include "misc/hash.hh"
+#include "misc/bddlt.hh"
+
+namespace spot
+{
+  /// \brief Help class to convert a bdd of an automaton into
+  /// its complement.
+  /// This is used when you need to complement all the acceptance
+  /// conditions in an automaton. For example in the simulation.
+  class AccCompl
+  {
+    public:
+      AccCompl(bdd all, bdd neg)
+        : all_(all),
+          neg_(neg)
+      {
+      }
+
+
+      bdd complement(const bdd acc);
+      bdd reverse_complement(const bdd acc);
+
+    protected:
+      bdd all_;
+      bdd neg_;
+      typedef Sgi::hash_map<bdd, bdd, bdd_hash> bdd_cache_t;
+      bdd_cache_t cache_;
+  };
+} // End namespace Spot
+
+#endif // !SPOT_MISC_ACCCOMPL_HH