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.
This commit is contained in:
parent
43d426aaae
commit
0411099506
5 changed files with 52 additions and 33 deletions
|
|
@ -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();
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -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<value_t>(v);
|
||||
return trival(static_cast<value_t>(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)
|
||||
{
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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());
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue