diff --git a/README b/README index 95da581fe..2195f09a8 100644 --- a/README +++ b/README @@ -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. diff --git a/configure.ac b/configure.ac index d6d915aec..6f25d894f 100644 --- a/configure.ac +++ b/configure.ac @@ -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 diff --git a/spot/Makefile.am b/spot/Makefile.am index ee2686ba2..b61a180ea 100644 --- a/spot/Makefile.am +++ b/spot/Makefile.am @@ -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 diff --git a/spot/twacube_algos/Makefile.am b/spot/twacube_algos/Makefile.am new file mode 100644 index 000000000..310ad3307 --- /dev/null +++ b/spot/twacube_algos/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) + +twacube_algosdir = $(pkgincludedir)/twacube_algos + +twacube_algos_HEADERS = convert.hh + +noinst_LTLIBRARIES = libtwacube_algos.la +libtwacube_algos_la_SOURCES = \ + convert.cc diff --git a/spot/twacube_algos/convert.cc b/spot/twacube_algos/convert.cc new file mode 100644 index 000000000..3a434b1f1 --- /dev/null +++ b/spot/twacube_algos/convert.cc @@ -0,0 +1,61 @@ +// -*- 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 + +namespace spot +{ + spot::cube satone_to_cube(bdd one, cubeset& cubeset, + std::unordered_map& 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& 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; + } +} diff --git a/spot/twacube_algos/convert.hh b/spot/twacube_algos/convert.hh new file mode 100644 index 000000000..313b114e1 --- /dev/null +++ b/spot/twacube_algos/convert.hh @@ -0,0 +1,40 @@ +// -*- 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 + +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& 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& reverse_binder); +} diff --git a/tests/core/cube.cc b/tests/core/cube.cc index 9fcdf19dc..cfcf77f99 100644 --- a/tests/core/cube.cc +++ b/tests/core/cube.cc @@ -17,9 +17,120 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include #include #include +#include +#include +#include +#include +#include +#include +#include + + +static bool test_translation(bdd& input, spot::cubeset& cubeset, + std::unordered_map& binder, + std::unordered_map& reverse_binder, + std::vector& 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 aps = {"a", "b", "c", "d", "e"}; + spot::cubeset cubeset(aps.size()); + + // Map Bdd indexes to cube indexes + std::unordered_map 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 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(); } diff --git a/tests/core/cube.test b/tests/core/cube.test index 30bb3c424..414f40e49 100755 --- a/tests/core/cube.test +++ b/tests/core/cube.test @@ -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