diff --git a/README b/README
index b7c1f2fc9dbe4a2a778609b8565971c55389d952..95da581fefe911ddde0f739fea92e69b27dbd759 100644
--- a/README
+++ b/README
@@ -290,6 +290,7 @@ spot/ Sources for libspot.
ta/ TA objects and cousins (TGTA).
taalgos/ Algorithms on TA/TGTA.
twa/ TωA objects and cousins (Transition-based ω-Automata).
+ twacube/ TωA objects based on cube (not-bdd).
twaalgos/ Algorithms on TωA.
gtec/ Couvreur's Emptiness-Check (old version).
gen/ Sources for libspotgen.
diff --git a/configure.ac b/configure.ac
index a898e735f226188ad675882cbaa1927e6e531aeb..d6d915aecb4173b5b6efc204ca7de2d486d45052 100644
--- a/configure.ac
+++ b/configure.ac
@@ -244,6 +244,7 @@ AC_CONFIG_FILES([
spot/twaalgos/Makefile
spot/twa/Makefile
spot/gen/Makefile
+ spot/twacube/Makefile
python/Makefile
tests/core/defs
tests/ltsmin/defs:tests/core/defs.in
diff --git a/spot/Makefile.am b/spot/Makefile.am
index e8229e8f2b24398b78ff6a5b1f9ed3886cc0d51f..ee2686ba2e50d4fe7a0540834cf38a272f3cbdda 100644
--- a/spot/Makefile.am
+++ b/spot/Makefile.am
@@ -25,7 +25,7 @@ AUTOMAKE_OPTIONS = subdir-objects
# List directories in the order they must be built. Keep tests at the
# end, after building '.' (since the current directory contains
# libspot.la needed by the tests)
-SUBDIRS = misc priv tl graph twa twaalgos ta taalgos kripke \
+SUBDIRS = misc priv tl graph twa twacube twaalgos ta taalgos kripke \
parseaut parsetl . ltsmin gen
lib_LTLIBRARIES = libspot.la
@@ -42,6 +42,7 @@ libspot_la_LIBADD = \
tl/libtl.la \
twaalgos/libtwaalgos.la \
twa/libtwa.la \
+ twacube/libtwacube.la \
../lib/libgnu.la \
../picosat/libpico.la
diff --git a/spot/twacube/Makefile.am b/spot/twacube/Makefile.am
new file mode 100644
index 0000000000000000000000000000000000000000..6fecda6f15f8bf122a9334b3633d1e52f00d04ec
--- /dev/null
+++ b/spot/twacube/Makefile.am
@@ -0,0 +1,32 @@
+## -*- coding: utf-8 -*-
+## Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire
+## de Recherche et Développement de l'Epita (LRDE).
+## Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
+## département Systèmes Répartis Coopératifs (SRC), Université Pierre
+## et Marie Curie.
+##
+## 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 .
+
+AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS)
+AM_CXXFLAGS = $(WARNING_CXXFLAGS)
+
+twacubedir = $(pkgincludedir)/twacube
+
+twacube_HEADERS = cube.hh
+
+noinst_LTLIBRARIES = libtwacube.la
+libtwacube_la_SOURCES = \
+ cube.cc
diff --git a/spot/twacube/cube.cc b/spot/twacube/cube.cc
new file mode 100644
index 0000000000000000000000000000000000000000..c5985c8afd7a926829e96a74e0850a85c666b5f5
--- /dev/null
+++ b/spot/twacube/cube.cc
@@ -0,0 +1,167 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2015, 2016 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
+#include
+#include
+#include
+
+namespace spot
+{
+ cubeset::cubeset(int aps)
+ {
+ size_ = aps;
+ nb_bits_ = sizeof(unsigned int) * CHAR_BIT;
+ uint_size_ = 1;
+ while ((aps = aps - nb_bits_)>0)
+ ++uint_size_;
+ }
+
+ cubeset::~cubeset()
+ { }
+
+ cube cubeset::alloc() const
+ {
+ auto* res = new unsigned int[2*uint_size_];
+ for (unsigned int i = 0; i < 2*uint_size_; ++i)
+ res[i] = 0;
+ return res;
+ }
+
+ void cubeset::set_true_var(cube c, unsigned int x) const
+ {
+ *(c+x/nb_bits_) |= 1 << (x%nb_bits_);
+ *(c+uint_size_+x/nb_bits_) &= ~(1 << (x%nb_bits_));
+ }
+
+ void cubeset::set_false_var(cube c, unsigned int x) const
+ {
+ *(c+uint_size_+x/nb_bits_) |= 1 << (x%nb_bits_);
+ *(c+x/nb_bits_) &= ~(1 << (x%nb_bits_));
+ }
+
+ bool cubeset::is_true_var(cube c, unsigned int x) const
+ {
+ unsigned int i = x/nb_bits_;
+ bool true_var = (*(c+i) >> x) & 1;
+ bool false_var = (*(c+i+uint_size_) >> x) & 1;
+ return true_var && !false_var;
+ }
+
+ bool cubeset::is_false_var(cube c, unsigned int x) const
+ {
+ unsigned int i = x/nb_bits_;
+ bool true_var = (*(c+i) >> x) & 1;
+ bool false_var = (*(c+i+uint_size_) >> x) & 1;
+ return !true_var && false_var;
+ }
+
+ bool cubeset::intersect(const cube lhs, const cube rhs) const
+ {
+ unsigned int true_elt;
+ unsigned int false_elt;
+ bool incompatible = false;
+ for (unsigned int i = 0; i < uint_size_ && !incompatible; ++i)
+ {
+ true_elt = *(lhs+i) | *(rhs+i);
+ false_elt = *(lhs+i+uint_size_) | *(rhs+i+uint_size_);
+ incompatible |= (true_elt & false_elt);
+ }
+ return !incompatible;
+ }
+
+ cube cubeset::intersection(const cube lhs, const cube rhs) const
+ {
+ auto* res = new unsigned int[2*uint_size_];
+ for (unsigned int i = 0; i < uint_size_; ++i)
+ {
+ res[i] = *(lhs+i) | *(rhs+i);
+ res[i+uint_size_] = *(lhs+i+uint_size_) | *(rhs+i+uint_size_);
+ }
+ return res;
+ }
+
+ bool cubeset::is_valid(const cube lhs) const
+ {
+ bool incompatible = false;
+ for (unsigned int i = 0; i < uint_size_ && !incompatible; ++i)
+ incompatible |= *(lhs+i) & *(lhs+i+uint_size_);
+ return !incompatible;
+ }
+
+ size_t cubeset::size() const
+ {
+ return size_;
+ }
+
+ void cubeset::release(cube c) const
+ {
+ delete[] c;
+ }
+
+ void cubeset::display(const cube c) const
+ {
+ for (unsigned int i = 0; i < 2*uint_size_; ++i)
+ {
+ if (i == uint_size_)
+ std::cout << '\n';
+
+ for (unsigned x = 0; x < nb_bits_; ++x)
+ std::cout << ((*(c+i) >> x) & 1);
+ }
+ std::cout << '\n';
+ }
+
+ std::string cubeset::dump(cube c, const std::vector& aps) const
+ {
+ std::ostringstream oss;
+ bool all_free = true;
+ unsigned int cpt = 0;
+ for (unsigned int i = 0; i < uint_size_; ++i)
+ {
+ for (unsigned x = 0; x < nb_bits_ && cpt != size_; ++x)
+ {
+ bool true_var = (*(c+i) >> x) & 1;
+ bool false_var = (*(c+i+uint_size_) >> x) & 1;
+ if (true_var)
+ {
+ oss << aps[cpt]
+ << (cpt != (size_ - 1) ? "&": "");
+ all_free = false;
+ }
+ else if (false_var)
+ {
+ oss << '!' << aps[cpt]
+ << (cpt != (size_ - 1) ? "&": "");
+ all_free = false;
+ }
+ ++cpt;
+ }
+ }
+ if (all_free)
+ oss << '1';
+
+ std::string res = oss.str();
+ if (res.back() == '&')
+ res.pop_back();
+ if (res.front() == '&')
+ res = res.substr(1);
+ return res;
+ }
+}
diff --git a/spot/twacube/cube.hh b/spot/twacube/cube.hh
new file mode 100644
index 0000000000000000000000000000000000000000..6dda9c9e8d7d47ad7442fb78aecdadb118d62608
--- /dev/null
+++ b/spot/twacube/cube.hh
@@ -0,0 +1,125 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2015, 2016 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 .
+
+
+#pragma once
+
+#include
+#include
+#include
+#include
+#include
+
+namespace spot
+{
+ /// \brief A cube is only a set of bits in memory.
+ ///
+ /// This set can be seen as two bitsets
+ /// - true_var : a bitset representing variables that
+ /// are set to true
+ /// - false_var : a bitset representing variables that
+ /// are set to false
+ ///
+ /// In the two vectors a bit set to 1 represent a variable set to
+ /// true (resp. false) for the true_var (resp. false_var)
+ ///
+ /// Warning : a variable cannot be set in both bitset at the
+ /// same time (consistency! cannot be true and false)
+ ///
+ /// The cube for (a & !b) will be repensented by :
+ /// - true_var = 1 0
+ /// - false_var = 0 1
+ ///
+ /// To represent free variables such as in (a & !b) | (a & b)
+ /// (wich is equivalent to (a) with b free)
+ /// - true_var : 1 0
+ /// - false_var : 0 0
+ /// This exemple shows that the representation of free variables
+ /// is done by unsetting variable in both vector
+ ///
+ /// To be memory efficient, these two bitsets are contigous in memory
+ /// i.e. if we want to represent 35 variables, a cube will be
+ /// represented by 4 unsigned int contiguous in memory. The 35
+ /// first bits represent truth values. The 29 bits following are
+ /// useless. Then, the 35 bits represents false value and the
+ /// rest is useless.
+ ///
+ /// Note that useless bits are only to perform some action efficiently,
+ /// i.e. only by ignoring them. The manipulation of cubes must be done
+ /// using the cubeset class
+ using cube = unsigned*;
+
+ class SPOT_API cubeset final
+ {
+ // \brief The total number of variables stored
+ size_t size_;
+
+ /// \brief The number of unsigned needed by the cube (for each part)
+ size_t uint_size_;
+
+ /// \brief The number of bits for an unsigned int
+ size_t nb_bits_;
+
+ public:
+ // Some deleted constructor
+ cubeset() = delete;
+
+ /// \brief Build the cubeset manager for \a aps variables
+ cubeset(int aps);
+
+ virtual ~cubeset();
+
+ /// \brief Allocate a new cube
+ cube alloc() const;
+
+ /// \brief Set the variable at position \a x to true.
+ void set_true_var(cube c, unsigned int x) const;
+
+ /// \brief Set the variable at position \a x to false.
+ void set_false_var(cube c, unsigned int x) const;
+
+ /// \brief Check if the variable at position \a x is true.
+ bool is_true_var(cube c, unsigned int x) const;
+
+ /// \brief Check if the variable at position \a x is false.
+ bool is_false_var(cube c, unsigned int x) const;
+
+ /// \brief return true if two cube intersect, i.e synchronisables.
+ bool intersect(const cube lhs, const cube rhs) const;
+
+ /// \brief return a cube resulting from the intersection of the two cubes
+ cube intersection(const cube lhs, const cube rhs) const;
+
+ /// \brief Check wether \a lhs is valid, is there is not variable
+ /// that is true and false at the same time.
+ bool is_valid(const cube lhs) const;
+
+ /// \brief Return the size of each cube.
+ size_t size() const;
+
+ /// \brief Release a cube.
+ void release(cube lhs) const;
+
+ /// \brief Raw display cube
+ void display(const cube c) const;
+
+ /// \brief Return the cube binded with atomic proposition names
+ std::string dump(cube c, const std::vector& aps) const;
+ };
+}
diff --git a/tests/Makefile.am b/tests/Makefile.am
index b39a54be818582ea88c687bf7f186b0bddcf6cdf..1c8617cb78ae13f6cf51f553b94df02af9f722e6 100644
--- a/tests/Makefile.am
+++ b/tests/Makefile.am
@@ -67,6 +67,7 @@ check_PROGRAMS = \
core/checkpsl \
core/checkta \
core/consterm \
+ core/cube \
core/emptchk \
core/equals \
core/graph \
@@ -118,6 +119,7 @@ core_randtgba_SOURCES = core/randtgba.cc
core_taatgba_SOURCES = core/taatgba.cc
core_tgbagraph_SOURCES = core/twagraph.cc
core_consterm_SOURCES = core/consterm.cc
+core_cube_SOURCES = core/cube.cc
core_equals_SOURCES = core/equalsf.cc
core_kind_SOURCES = core/kind.cc
core_length_SOURCES = core/length.cc
@@ -152,6 +154,7 @@ core_tunenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM -DUNABBREV='"^ieFG"'
TESTS_tl = \
core/bare.test \
+ core/cube.test \
core/parse.test \
core/parseerr.test \
core/utf8.test \
diff --git a/tests/core/.gitignore b/tests/core/.gitignore
index 254d5cee15d7450301f3f4ee03a1a1357bed3bd1..4e87ead2b7c61d87c94bfbc450f2f74e5081e4d4 100644
--- a/tests/core/.gitignore
+++ b/tests/core/.gitignore
@@ -8,6 +8,7 @@ checkpsl
checkta
complement
consterm
+cube
defs
.deps
*.dot
diff --git a/tests/core/cube.cc b/tests/core/cube.cc
new file mode 100644
index 0000000000000000000000000000000000000000..9fcdf19dcb27f7057e8efae66c955a8488b319da
--- /dev/null
+++ b/tests/core/cube.cc
@@ -0,0 +1,58 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement
+// de l'Epita.
+//
+// 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
+
+int main()
+{
+ std::vector aps = {"a", "b", "c", "d", "e"};
+ spot::cubeset cs(aps.size());
+ spot::cube mc = cs.alloc();
+ cs.set_true_var(mc, 0);
+ cs.set_false_var(mc, 3);
+ std::cout << "size : " << cs.size() << '\n';
+ std::cout << "cube : " << cs.dump(mc, aps) << '\n';
+ std::cout << "valid : " << cs.is_valid(mc) << '\n';
+ std::cout << "intersect(c,c) : " << cs.intersect(mc, mc) << '\n';
+
+ spot::cube mc1 = cs.alloc();
+ cs.set_false_var(mc1, 0);
+ cs.set_true_var(mc1, 1);
+ std::cout << "size : " << cs.size() << '\n';
+ std::cout << "cube : " << cs.dump(mc1, aps) << '\n';
+ std::cout << "valid : " << cs.is_valid(mc1) << '\n';
+ std::cout << "intersect(c1,c1) : " << cs.intersect(mc1, mc1) << '\n';
+ std::cout << "intersect(c,c1) : " << cs.intersect(mc, mc1) << '\n';
+ std::cout << "intersect(c1,c) : " << cs.intersect(mc1, mc) << '\n';
+
+ spot::cube mc2 = cs.alloc();
+ cs.set_true_var(mc2, 1);
+ cs.set_true_var(mc2, 3);
+ std::cout << "size : " << cs.size() << '\n';
+ std::cout << "cube : " << cs.dump(mc2, aps) << '\n';
+ std::cout << "valid : " << cs.is_valid(mc2) << '\n';
+ std::cout << "intersect(c2,c1) : " << cs.intersect(mc1, mc2) << '\n';
+ std::cout << "intersect(c2,c) : " << cs.intersect(mc, mc2) << '\n';
+
+ cs.release(mc2);
+ cs.release(mc1);
+ cs.release(mc);
+}
diff --git a/tests/core/cube.test b/tests/core/cube.test
new file mode 100755
index 0000000000000000000000000000000000000000..30bb3c4249e7aefb791be11f38dae75949174d7a
--- /dev/null
+++ b/tests/core/cube.test
@@ -0,0 +1,53 @@
+#!/bin/sh
+# -*- coding: utf-8 -*-
+# Copyright (C) 2015, 2016 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 .
+
+# While running some benchmark, Tomáš Babiak found that Spot took too
+# much time (i.e. >1h) to translate those six formulae. It turns out
+# that the WDBA minimization was performed after the degeneralization
+# algorithm, while this is not necessary (WDBA will produce a BA, so
+# we may as well skip degeneralization). Translating these formulae
+# in the test-suite ensure that they don't take too much time (the
+# buildfarm will timeout if it does).
+
+. ./defs
+
+set -e
+
+run 0 ../cube > stdout
+
+cat >expected <