Introduce cube data structure

* README, configure.ac, spot/Makefile.am,
spot/twacube/Makefile.am, spot/twacube/cube.cc,
spot/twacube/cube.hh, tests/Makefile.am,
tests/core/.gitignore, tests/core/cube.cc,
tests/core/cube.test: here.

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.

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

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
 

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 <http://www.gnu.org/licenses/>.
+
+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

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 <http://www.gnu.org/licenses/>.
+
+#include <sstream>
+#include <iostream>
+#include <spot/twacube/cube.hh>
+#include <assert.h>
+
+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<std::string>& 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;
+  }
+}

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 <http://www.gnu.org/licenses/>.
+
+
+#pragma once
+
+#include <spot/misc/common.hh>
+#include <vector>
+#include <string>
+#include <climits>
+#include <sstream>
+
+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<std::string>& aps) const;
+  };
+}

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 \

tests/core/.gitignore

@@ -8,6 +8,7 @@ checkpsl
 checkta
 complement
 consterm
+cube
 defs
 .deps
 *.dot

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 <http://www.gnu.org/licenses/>.
+
+
+#include <iostream>
+#include <spot/twacube/cube.hh>
+
+int main()
+{
+  std::vector<std::string> 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);
+}

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 <http://www.gnu.org/licenses/>.
+
+# 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 <<EOF
+size : 5
+cube : a&!d
+valid : 1
+intersect(c,c) : 1
+size : 5
+cube : !a&b
+valid : 1
+intersect(c1,c1) : 1
+intersect(c,c1) : 0
+intersect(c1,c) : 0
+size : 5
+cube : b&d
+valid : 1
+intersect(c2,c1) : 1
+intersect(c2,c) : 0
+EOF
+
+diff stdout expected