Commit 1e271b5a authored by Etienne Renault's avatar Etienne Renault

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.
parent 66aa6d08
......@@ -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.
......
......@@ -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
......
......@@ -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
......
## -*- 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
// -*- 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;
}
}
// -*- 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;
};
}
......@@ -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 \
......
......@@ -8,6 +8,7 @@ checkpsl
checkta
complement
consterm
cube
defs
.deps
*.dot
......
// -*- 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);
}
#!/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
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment