Commit 1aeb260a authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

trival: new class for tri-valued logic

* spot/misc/trival.hh: New file.
* spot/misc/Makefile.am: Add it.
* python/spot_impl.i: Add Python bindings.
* tests/core/trival.cc, tests/core/trival.test,
tests/python/trival.py: New files, testing it.
* tests/Makefile.am: Add them.
parent e764cf6f
// -*- 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 <spot/misc/optionmap.hh>
#include <spot/misc/random.hh>
#include <spot/misc/escape.hh>
#include <spot/misc/trival.hh>
#include <spot/tl/formula.hh>
......@@ -331,6 +332,9 @@ namespace swig
%include <spot/misc/random.hh>
%include <spot/misc/escape.hh>
%implicitconv spot::trival;
%include <spot/misc/trival.hh>
%implicitconv std::vector<spot::formula>;
%include <spot/tl/formula.hh>
......@@ -439,7 +443,36 @@ namespace std {
%include <spot/taalgos/minimize.hh>
#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 {
......
## -*- 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
......
// -*- 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 <http://www.gnu.org/licenses/>.
#pragma once
#include <iostream>
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<value_t>(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");
}
/// @}
}
......@@ -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
......
......@@ -65,6 +65,7 @@ tgbagraph
tgbaread
tostring
tripprod
trival
tunabbrev
tunenoform
unabbrevwm
// -*- 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 <http://www.gnu.org/licenses/>.
#undef NDEBUG
#include <spot/misc/trival.hh>
#include <cassert>
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';
}
#!/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 <http://www.gnu.org/licenses/>.
# 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 <<EOF
no && no == no
no && maybe == no
no && yes == no
maybe && no == no
maybe && maybe == maybe
maybe && yes == maybe
yes && no == no
yes && maybe == maybe
yes && yes == yes
no || no == no
no || maybe == maybe
no || yes == yes
maybe || no == maybe
maybe || maybe == maybe
maybe || yes == yes
yes || no == yes
yes || maybe == yes
yes || yes == yes
EOF
diff trival.out expected
# -*- mode: python; coding: utf-8 -*-
# Copyright (C) 2016 Laboratoire de Recherche et Développement
# de l'Epita
#
# 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/>.
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)
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