From 041109950644b715b921801ff85b7434bd0adbb7 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 3 Jul 2018 23:28:41 +0200 Subject: [PATCH] trival: prefer a global operator== relying on implicit conversion Hopefully fixes #359. * spot/misc/trival.hh: Declare a global operator==(trival,trival) that replace the specialized operator==(bool,trival), and the in class trival::operator(trival), thanks to the implicit construction from bool to trival. Make the repr_t/value_t constructor explicit, are those are mostly internal to the library and may cause conflicts. * spot/twa/twa.hh: Adjust to construct trival explicitly. * python/spot/impl.i: Since Swig/Python does not support global comparison operators, implement a member version, supporting only __eq__(trival,bool) as before. * tests/python/setacc.py: Adjust erroneous code. * tests/python/trival.py: Add test cases. --- python/spot/impl.i | 10 ++++++++++ spot/misc/trival.hh | 41 ++++++++++++++++++++++------------------- spot/twa/twa.hh | 22 +++++++++++----------- tests/python/setacc.py | 5 +++-- tests/python/trival.py | 7 ++++++- 5 files changed, 52 insertions(+), 33 deletions(-) diff --git a/python/spot/impl.i b/python/spot/impl.i index e06f4835a..1050c7568 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -681,6 +681,16 @@ def state_is_accepting(self, src) -> "bool": { return *self || other; } + + bool __eq__(spot::trival other) + { + return self->val() == other.val(); + } + + bool __ne__(spot::trival other) + { + return self->val() != other.val(); + } } diff --git a/spot/misc/trival.hh b/spot/misc/trival.hh index 36f0f8eef..91464c01a 100644 --- a/spot/misc/trival.hh +++ b/spot/misc/trival.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2016 Laboratoire de Recherche et Developpement de -// l'Epita (LRDE). +// Copyright (C) 2016, 2018 Laboratoire de Recherche et Developpement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -50,12 +50,16 @@ namespace spot { } - trival(repr_t v) +#ifndef SWIG + // This is needed internally by Spot to work around the bitfield + // issue mentioned earlier, it makes no sense to use it in Python. + static trival from_repr_t(repr_t v) { - val_ = static_cast(v); + return trival(static_cast(v)); } +#endif - constexpr trival(value_t v) + constexpr explicit trival(value_t v) : val_(v) { } @@ -86,16 +90,6 @@ namespace spot 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_; @@ -118,15 +112,24 @@ namespace spot } }; - constexpr bool operator==(bool a, trival b) + // We prefer a global version of the operator so that the left + // argument can be promoted (think "bool == trival" being promoted + // to "trival == trival"). However Swig's generated Python bindings + // cannot deal with operators in the global namespace, so we use an + // in-class version (coded in impl.i) in this case. This will fail + // on a "bool == trival" comparison in Python, but we usually write + // "trival == bool" and that works. +#ifndef SWIG + constexpr bool operator==(trival a, trival b) { - return b == trival(a); + return a.val() == b.val(); } - constexpr bool operator!=(bool a, trival b) + constexpr bool operator!=(trival a, trival b) { - return b != trival(a); + return !(a == b); } +#endif constexpr trival operator&&(trival a, trival b) { diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh index 6b29bc142..f6d00d7e8 100644 --- a/spot/twa/twa.hh +++ b/spot/twa/twa.hh @@ -1203,8 +1203,8 @@ namespace spot trival prop_state_acc() const { if (num_sets() == 0) - return true; - return is.state_based_acc; + return trival(true); + return trival::from_repr_t(is.state_based_acc); } /// \brief Set the state-based-acceptance property. @@ -1235,7 +1235,7 @@ namespace spot /// \see prop_terminal() trival prop_inherently_weak() const { - return is.inherently_weak; + return trival::from_repr_t(is.inherently_weak); } /// \brief Set the "inherently weak" property. @@ -1265,7 +1265,7 @@ namespace spot /// \see prop_inherently_weak() trival prop_terminal() const { - return is.terminal; + return trival::from_repr_t(is.terminal); } /// \brief Set the terminal property. @@ -1291,7 +1291,7 @@ namespace spot /// \see prop_inherently_weak() trival prop_weak() const { - return is.weak; + return trival::from_repr_t(is.weak); } /// \brief Set the weak property. @@ -1321,7 +1321,7 @@ namespace spot /// \see prop_weak() trival prop_very_weak() const { - return is.very_weak; + return trival::from_repr_t(is.very_weak); } /// \brief Set the very-weak property. @@ -1352,7 +1352,7 @@ namespace spot /// \see is_complete() trival prop_complete() const { - return is.complete; + return trival::from_repr_t(is.complete); } /// \brief Set the complete property. @@ -1376,7 +1376,7 @@ namespace spot /// \see is_universal() trival prop_universal() const { - return is.universal; + return trival::from_repr_t(is.universal); } /// \brief Set the universal property. @@ -1427,7 +1427,7 @@ namespace spot /// \see is_unambiguous() trival prop_unambiguous() const { - return is.unambiguous; + return trival::from_repr_t(is.unambiguous); } /// \brief Set the unambiguous property @@ -1457,7 +1457,7 @@ namespace spot /// \see is_semi_deterministic() trival prop_semi_deterministic() const { - return is.semi_deterministic; + return trival::from_repr_t(is.semi_deterministic); } /// \brief Set the semi-deterministic property @@ -1487,7 +1487,7 @@ namespace spot /// \see is_stutter_invariant trival prop_stutter_invariant() const { - return is.stutter_invariant; + return trival::from_repr_t(is.stutter_invariant); } /// \brief Set the stutter-invariant property diff --git a/tests/python/setacc.py b/tests/python/setacc.py index 58f0feedd..e3402cc34 100644 --- a/tests/python/setacc.py +++ b/tests/python/setacc.py @@ -1,6 +1,6 @@ #!/usr/bin/python3 # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2016 Laboratoire de Recherche et Développement de +# Copyright (C) 2016, 2018 Laboratoire de Recherche et Développement de # l'EPITA. # # This file is part of Spot, a model checking library. @@ -22,5 +22,6 @@ import spot a = spot.make_twa_graph(spot._bdd_dict) a.set_acceptance(0, spot.acc_code("t")) +assert(a.prop_state_acc() == True); a.set_acceptance(1, spot.acc_code("Fin(0)")) -assert(a.prop_state_acc() == 0); +assert(a.prop_state_acc() == spot.trival.maybe()); diff --git a/tests/python/trival.py b/tests/python/trival.py index 2dda087a1..f9274e630 100644 --- a/tests/python/trival.py +++ b/tests/python/trival.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2016 Laboratoire de Recherche et Développement +# Copyright (C) 2016, 2018 Laboratoire de Recherche et Développement # de l'Epita # # This file is part of Spot, a model checking library. @@ -26,11 +26,16 @@ v4 = spot.trival_maybe() assert v1 != v2 assert v1 != v3 assert v2 != v3 +assert v2 == spot.trival(spot.trival.no_value) +assert v2 != spot.trival(spot.trival.yes_value) assert v4 != v2 assert v4 != v3 assert v2 == False assert True == v3 +assert v2 != True +assert False != v3 assert v4 == spot.trival_maybe() +assert v4 == spot.trival(spot.trival.maybe_value) assert v3 assert -v2 assert not -v1