diff --git a/python/spot_impl.i b/python/spot_impl.i index 9d2e0107f..c65e95bcf 100644 --- a/python/spot_impl.i +++ b/python/spot_impl.i @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de -// Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016 +// Laboratoire de Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique // de Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -81,6 +81,7 @@ #include #include #include +#include #include @@ -331,6 +332,9 @@ namespace swig %include %include +%implicitconv spot::trival; +%include + %implicitconv std::vector; %include @@ -439,7 +443,36 @@ namespace std { %include -#undef ltl +%extend spot::trival { + std::string __repr__() + { + std::ostringstream os; + os << *self; + return os.str(); + } + + std::string __str__() + { + std::ostringstream os; + os << *self; + return os.str(); + } + + spot::trival __neg__() + { + return !*self; + } + + spot::trival __and__(spot::trival other) + { + return *self && other; + } + + spot::trival __or__(spot::trival other) + { + return *self || other; + } +} %exception spot::formula::__getitem__ { try { diff --git a/spot/misc/Makefile.am b/spot/misc/Makefile.am index 233c1af6b..103e9db45 100644 --- a/spot/misc/Makefile.am +++ b/spot/misc/Makefile.am @@ -1,6 +1,6 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2011, 2012, 2013, 2014 Laboratoire de Recherche et -## Développement de l'Epita (LRDE). +## Copyright (C) 2011, 2012, 2013, 2014, 2016 Laboratoire de Recherche +## et Développement de l'Epita (LRDE). ## Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de ## Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), ## Université Pierre et Marie Curie. @@ -53,6 +53,7 @@ misc_HEADERS = \ satsolver.hh \ timer.hh \ tmpfile.hh \ + trival.hh \ version.hh noinst_LTLIBRARIES = libmisc.la diff --git a/spot/misc/trival.hh b/spot/misc/trival.hh new file mode 100644 index 000000000..f9ad14544 --- /dev/null +++ b/spot/misc/trival.hh @@ -0,0 +1,179 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 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 + +namespace spot +{ + + /// \ingroup misc_tools + /// @{ + + /// \brief A class implementing Kleene's three-valued logic. + /// + /// https://en.wikipedia.org/wiki/Three-valued_logic#Kleene_and_Priest_logics + class trival + { + public: + // We use repr_t instead of value_t in bitfields to avoid a warning from gcc + // https://gcc.gnu.org/bugzilla/show_bug.cgi?id=51242 + typedef signed char repr_t; + enum value_t : repr_t { no_value = -1, maybe_value = 0, yes_value = 1 }; + private: + value_t val_; + public: + constexpr trival() + : val_(maybe_value) + { + } + + constexpr trival(bool v) + : val_(v ? yes_value : no_value) + { + } + + trival(repr_t v) + { + val_ = static_cast(v); + } + + constexpr trival(value_t v) + : val_(v) + { + } + + static constexpr trival maybe() + { + return trival(); + } + + /// Is true or false, but not maybe. + constexpr bool is_known() const + { + return val_ != maybe_value; + } + + constexpr bool is_maybe() const + { + return val_ == maybe_value; + } + + constexpr bool is_true() const + { + return val_ == yes_value; + } + + constexpr bool is_false() const + { + return val_ == no_value; + } + + constexpr bool operator==(trival o) const + { + return val_ == o.val_; + } + + constexpr bool operator!=(trival o) const + { + return val_ != o.val_; + } + + constexpr value_t val() const + { + return val_; + } + +#ifndef SWIG + // constexpr explicit only supported in SWIG >= 3.0.4 + constexpr +#endif + explicit operator bool() const + { + return val_ == yes_value; + } + + constexpr trival operator!() const + { + return trival((val_ == yes_value) ? no_value : + (val_ == no_value) ? yes_value : + maybe_value); + } + }; + + constexpr bool operator==(bool a, trival b) + { + return b == trival(a); + } + + constexpr bool operator!=(bool a, trival b) + { + return b != trival(a); + } + + constexpr trival operator&&(trival a, trival b) + { + return + (a.val() == trival::no_value || b.val() == trival::no_value) + ? trival(false) + : (a.val() == trival::maybe_value || b.val() == trival::maybe_value) + ? trival::maybe() + : trival(true); + } + + constexpr trival operator&&(bool a, trival b) + { + return trival(a) && b; + } + + constexpr trival operator&&(trival a, bool b) + { + return a && trival(b); + } + + constexpr trival operator||(trival a, trival b) + { + return + (a.val() == trival::yes_value || b.val() == trival::yes_value) + ? trival(true) + : (a.val() == trival::maybe_value || b.val() == trival::maybe_value) + ? trival::maybe() + : trival(false); + } + + constexpr trival operator||(bool a, trival b) + { + return trival(a) || b; + } + + constexpr trival operator||(trival a, bool b) + { + return a || trival(b); + } + + inline std::ostream& operator<<(std::ostream& os, trival v) + { + return os << ((v.val() == trival::no_value) ? "no" + : (v.val() == trival::maybe_value) ? "maybe" + : "yes"); + } + + /// @} +} diff --git a/tests/Makefile.am b/tests/Makefile.am index aa1b4e9fd..fd107e74c 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -36,8 +36,8 @@ check_SCRIPTS = run # We try to keep this somehow by strength. Test basic things first, # because such failures will be easier to diagnose and fix. -TESTS = $(TESTS_sanity) $(TESTS_tl) $(TESTS_graph) $(TESTS_kripke) \ - $(TESTS_twa) $(TESTS_python) $(TESTS_ltsmin) +TESTS = $(TESTS_sanity) $(TESTS_misc) $(TESTS_tl) $(TESTS_graph) \ + $(TESTS_kripke) $(TESTS_twa) $(TESTS_python) $(TESTS_ltsmin) distclean-local: find . -name '*.dir' -type d -print | xargs rm -rf @@ -85,6 +85,7 @@ check_PROGRAMS = \ core/reductaustr \ core/syntimpl \ core/taatgba \ + core/trival \ core/tgbagraph \ core/tostring \ core/tunabbrev \ @@ -131,6 +132,7 @@ core_reductaustr_SOURCES = core/equalsf.cc core_reductaustr_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC_TAUSTR core_syntimpl_SOURCES = core/syntimpl.cc core_tostring_SOURCES = core/tostring.cc +core_trival_SOURCES = core/trival.cc core_tunabbrev_SOURCES = core/equalsf.cc core_tunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DUNABBREV='"^ieFG"' core_tunenoform_SOURCES = core/equalsf.cc @@ -180,11 +182,14 @@ TESTS_graph = \ TESTS_kripke = \ core/kripke.test +TESTS_misc = \ + core/bitvect.test \ + core/intvcomp.test \ + core/trival.test + TESTS_twa = \ core/acc.test \ core/acc2.test \ - core/intvcomp.test \ - core/bitvect.test \ core/ltlcross3.test \ core/taatgba.test \ core/renault.test \ @@ -299,7 +304,8 @@ TESTS_python = \ python/remfin.py \ python/satmin.py \ python/setxor.py \ - python/testingaut.ipynb + python/testingaut.ipynb \ + python/trival.py endif SUFFIXES = .ipynb .html diff --git a/tests/core/.gitignore b/tests/core/.gitignore index 35bf1ca83..bad8812a1 100644 --- a/tests/core/.gitignore +++ b/tests/core/.gitignore @@ -65,6 +65,7 @@ tgbagraph tgbaread tostring tripprod +trival tunabbrev tunenoform unabbrevwm diff --git a/tests/core/trival.cc b/tests/core/trival.cc new file mode 100644 index 000000000..04d760d12 --- /dev/null +++ b/tests/core/trival.cc @@ -0,0 +1,50 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 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 . + +#undef NDEBUG +#include +#include + +int main() +{ + spot::trival v1; + spot::trival v2(false); + spot::trival v3(true); + spot::trival v4 = spot::trival::maybe(); + assert(v1 != v2); + assert(v1 != v3); + assert(v2 != v3); + assert(v4 != v2); + assert(v4 != v3); + assert(v2 == false); + assert(true == v3); + assert(v4 == spot::trival::maybe()); + assert(v3); + assert(!v2); + assert(!(bool)!v1); + assert(!(bool)v1); + assert(!(bool)!v3); + + for (auto u : {v2, v1, v3}) + for (auto v : {v2, v1, v3}) + std::cout << u << " && " << v << " == " << (u && v) << '\n'; + for (auto u : {v2, v1, v3}) + for (auto v : {v2, v1, v3}) + std::cout << u << " || " << v << " == " << (u || v) << '\n'; +} diff --git a/tests/core/trival.test b/tests/core/trival.test new file mode 100755 index 000000000..c808f87ae --- /dev/null +++ b/tests/core/trival.test @@ -0,0 +1,56 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 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 ../trival > trival.out + +cat > expected <. + +import spot + +v1 = spot.trival() +v2 = spot.trival(False) +v3 = spot.trival(True) +v4 = spot.trival_maybe() +assert v1 != v2 +assert v1 != v3 +assert v2 != v3 +assert v4 != v2 +assert v4 != v3 +assert v2 == False +assert True == v3 +assert v4 == spot.trival_maybe() +assert v3 +assert -v2 +assert not -v1 +assert not v1; +assert not -v3 + +for u in (v1, v2, v3): + for v in (v1, v2, v3): + assert (u & v) == -(-u | -v)