Commit 9725456b authored by Etienne Renault's avatar Etienne Renault

convert: BDD to cube conversions

* README, configure.ac, spot/Makefile.am,
spot/twacube_algos/Makefile.am, spot/twacube_algos/convert.cc
spot/twacube_algos/convert.hh, tests/core/cube.cc,
tests/core/cube.test: here.
parent 1e271b5a
......@@ -291,6 +291,7 @@ spot/ Sources for libspot.
taalgos/ Algorithms on TA/TGTA.
twa/ TωA objects and cousins (Transition-based ω-Automata).
twacube/ TωA objects based on cube (not-bdd).
twacube_algos/ TωAcube algorithms
twaalgos/ Algorithms on TωA.
gtec/ Couvreur's Emptiness-Check (old version).
gen/ Sources for libspotgen.
......
......@@ -242,6 +242,7 @@ AC_CONFIG_FILES([
spot/tl/Makefile
spot/twaalgos/gtec/Makefile
spot/twaalgos/Makefile
spot/twacube_algos/Makefile
spot/twa/Makefile
spot/gen/Makefile
spot/twacube/Makefile
......
......@@ -26,7 +26,7 @@ AUTOMAKE_OPTIONS = subdir-objects
# end, after building '.' (since the current directory contains
# libspot.la needed by the tests)
SUBDIRS = misc priv tl graph twa twacube twaalgos ta taalgos kripke \
parseaut parsetl . ltsmin gen
twacube_algos parseaut parsetl . ltsmin gen
lib_LTLIBRARIES = libspot.la
libspot_la_SOURCES =
......@@ -42,6 +42,7 @@ libspot_la_LIBADD = \
tl/libtl.la \
twaalgos/libtwaalgos.la \
twa/libtwa.la \
twacube_algos/libtwacube_algos.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)
twacube_algosdir = $(pkgincludedir)/twacube_algos
twacube_algos_HEADERS = convert.hh
noinst_LTLIBRARIES = libtwacube_algos.la
libtwacube_algos_la_SOURCES = \
convert.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 <spot/twacube_algos/convert.hh>
#include <assert.h>
namespace spot
{
spot::cube satone_to_cube(bdd one, cubeset& cubeset,
std::unordered_map<int, int>& binder)
{
auto cube = cubeset.alloc();
while (one != bddtrue)
{
if (bdd_high(one) == bddfalse)
{
assert(binder.find(bdd_var(one)) != binder.end());
cubeset.set_false_var(cube, binder[bdd_var(one)]);
one = bdd_low(one);
}
else
{
assert(binder.find(bdd_var(one)) != binder.end());
cubeset.set_true_var(cube, binder[bdd_var(one)]);
one = bdd_high(one);
}
}
return cube;
}
bdd cube_to_bdd(spot::cube cube, const cubeset& cubeset,
std::unordered_map<int, int>& reverse_binder)
{
bdd result = bddtrue;
for (unsigned int i = 0; i < cubeset.size(); ++i)
{
assert(reverse_binder.find(i) != reverse_binder.end());
if (cubeset.is_false_var(cube, i))
result &= bdd_nithvar(reverse_binder[i]);
if (cubeset.is_true_var(cube, i))
result &= bdd_ithvar(reverse_binder[i]);
}
return result;
}
}
// -*- 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 <bddx.h>
#include <unordered_map>
#include <spot/misc/common.hh>
#include <spot/twacube/cube.hh>
namespace spot
{
/// \brief Transform one truth assignment represented as a BDD
/// into a \a cube cube passed in parameter. The parameter
/// \a binder map bdd indexes to cube indexes.
SPOT_API spot::cube satone_to_cube(bdd one, cubeset& cubeset,
std::unordered_map<int, int>& binder);
/// \brief Transform a \a cube cube into bdd using the map
/// that bind cube indexes to bdd indexes.
SPOT_API bdd cube_to_bdd(spot::cube cube, const cubeset& cubeset,
std::unordered_map<int, int>& reverse_binder);
}
......@@ -17,9 +17,120 @@
// 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 <bddx.h>
#include <iostream>
#include <spot/twacube/cube.hh>
#include <spot/misc/hash.hh>
#include <spot/twacube/cube.hh>
#include <spot/twacube_algos/convert.hh>
#include <spot/twa/bdddict.hh>
#include <spot/tl/environment.hh>
#include <spot/tl/defaultenv.hh>
#include <unordered_map>
static bool test_translation(bdd& input, spot::cubeset& cubeset,
std::unordered_map<int, int>& binder,
std::unordered_map<int, int>& reverse_binder,
std::vector<std::string>& aps)
{
// The BDD used to detect if the convertion works
bdd res = bddfalse;
bdd initial = input;
std::cout << "bdd : " << input << '\n';
while (initial != bddfalse)
{
bdd one = bdd_satone(initial);
initial -= one;
auto cube = spot::satone_to_cube(one, cubeset, binder);
res |= spot::cube_to_bdd(cube, cubeset, reverse_binder);
std::cout << "cube : " << cubeset.dump(cube, aps) << '\n';
delete[] cube;
}
// Translating BDD to cubes and cubes to BDD should provide same BDD.
return input == res;
}
static void test_bdd_to_cube()
{
auto d = spot::make_bdd_dict();
spot::environment& e = spot::default_environment::instance();
// Some of these variables are not desired into the final cube
auto ap_0 = e.require("0");
int idx_0 = d->register_proposition(ap_0, d);
auto ap_a = e.require("a");
int idx_a = d->register_proposition(ap_a, d);
auto ap_b = e.require("b");
int idx_b = d->register_proposition(ap_b, d);
auto ap_1 = e.require("1");
int idx_1 = d->register_proposition(ap_1, d);
auto ap_c = e.require("c");
int idx_c = d->register_proposition(ap_c, d);
auto ap_d = e.require("d");
int idx_d = d->register_proposition(ap_d, d);
auto ap_e = e.require("e");
int idx_e = d->register_proposition(ap_e, d);
// Prepare cube
std::vector<std::string> aps = {"a", "b", "c", "d", "e"};
spot::cubeset cubeset(aps.size());
// Map Bdd indexes to cube indexes
std::unordered_map<int, int> binder = {
{idx_a, 0},
{idx_b, 1},
{idx_c, 2},
{idx_d, 3},
{idx_e, 4}
};
// Map cube indexes to Bdd indexes
std::unordered_map<int, int> reverse_binder = {
{0, idx_a},
{1, idx_b},
{2, idx_c},
{3, idx_d},
{4, idx_e}
};
// The BDD to convert
bdd x;
bool result;
// Test bddtrue
x = bddtrue;
result = test_translation(x, cubeset, binder, reverse_binder, aps);
assert(result);
// Test bddfalse
x = bddfalse;
result = test_translation(x, cubeset, binder, reverse_binder, aps);
assert(result);
// Test bdddeterministic bdd
x = bdd_ithvar(idx_a) & !bdd_ithvar(idx_b) & bdd_ithvar(idx_c) &
!bdd_ithvar(idx_d) & bdd_ithvar(idx_e);
result = test_translation(x, cubeset, binder, reverse_binder, aps);
assert(result);
// // Test some free var bdd
x = (bdd_ithvar(idx_a) | bdd_ithvar(idx_b)) & bdd_ithvar(idx_d);
result = test_translation(x, cubeset, binder, reverse_binder, aps);
assert(result);
// Free all variables
d->unregister_variable(idx_e, d);
d->unregister_variable(idx_d, d);
d->unregister_variable(idx_c, d);
d->unregister_variable(idx_1, d);
d->unregister_variable(idx_b, d);
d->unregister_variable(idx_a, d);
d->unregister_variable(idx_0, d);
}
int main()
{
......@@ -55,4 +166,5 @@ int main()
cs.release(mc2);
cs.release(mc1);
cs.release(mc);
test_bdd_to_cube();
}
......@@ -48,6 +48,14 @@ cube : b&d
valid : 1
intersect(c2,c1) : 1
intersect(c2,c) : 0
bdd : T
cube : 1
bdd : F
bdd : <1:1, 2:0, 4:1, 5:0, 6:1>
cube : a&!b&c&!d&e
bdd : <1:0, 2:1, 5:1><1:1, 5:1>
cube : !a&b&d
cube : a&d
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