From 882097a2ce17b94585a2b4d8dd5574d2daa107da Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 24 Jun 2013 21:59:52 +0200 Subject: [PATCH] Remove modgray, it's not used. * src/misc/modgray.cc, src/misc/modgray.hh: Delete. * src/misc/Makefile.am: Adjust. * wrap/python/tests/modgray.py: Delete. * wrap/python/tests/Makefile.am: Adjust. * wrap/python/spot.i: Remove binding. --- src/misc/Makefile.am | 2 - src/misc/modgray.cc | 131 ------------------------------ src/misc/modgray.hh | 145 ---------------------------------- wrap/python/spot.i | 4 - wrap/python/tests/Makefile.am | 3 +- wrap/python/tests/modgray.py | 58 -------------- 6 files changed, 1 insertion(+), 342 deletions(-) delete mode 100644 src/misc/modgray.cc delete mode 100644 src/misc/modgray.hh delete mode 100755 wrap/python/tests/modgray.py diff --git a/src/misc/Makefile.am b/src/misc/Makefile.am index bf27c91ca..4812bdcf3 100644 --- a/src/misc/Makefile.am +++ b/src/misc/Makefile.am @@ -45,7 +45,6 @@ misc_HEADERS = \ intvcmp2.hh \ ltstr.hh \ minato.hh \ - modgray.hh \ memusage.hh \ mspool.hh \ optionmap.hh \ @@ -64,7 +63,6 @@ libmisc_la_SOURCES = \ freelist.cc \ intvcomp.cc \ intvcmp2.cc \ - modgray.cc \ memusage.cc \ minato.cc \ optionmap.cc \ diff --git a/src/misc/modgray.cc b/src/misc/modgray.cc deleted file mode 100644 index 0941ac995..000000000 --- a/src/misc/modgray.cc +++ /dev/null @@ -1,131 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2012 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). -// Copyright (C) 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 . - -#include "modgray.hh" - -namespace spot -{ - - loopless_modular_mixed_radix_gray_code:: - loopless_modular_mixed_radix_gray_code(int n) - : n_(n), done_(false), a_(0), f_(0), m_(0), s_(0), non_one_radixes_(0) - { - } - - loopless_modular_mixed_radix_gray_code:: - ~loopless_modular_mixed_radix_gray_code() - { - delete[] a_; - delete[] f_; - delete[] m_; - delete[] s_; - delete[] non_one_radixes_; - } - - void - loopless_modular_mixed_radix_gray_code::first() - { - if (!non_one_radixes_) - { - // This computation needs to be done only once, but we cannot - // do it in the constructor because it involves virtual - // functions. - - // non_one_radixes_ needs to hold at most n_ integer, maybe less - // we do not know yet and do not care (saving these extra bytes - // would require two loops over a_last(j); this doesn't seem - // worth the hassle). We update n_ before allocating the other - // arrays. - non_one_radixes_ = new int[n_]; - int k = 0; - for (int j = 0; j < n_; ++j) - { - a_first(j); - if (!a_last(j)) - non_one_radixes_[k++] = j; - } - n_ = k; - a_ = new int[k]; - f_ = new int[k + 1]; - m_ = new int[k]; - s_ = new int[k]; - - for (int j = 0; j < n_; ++j) - m_[j] = -1; - f_[n_] = n_; - } - - // Reset everything except m_[j] (let's preserve discovered - // radixes between runs) and f_[n_] (never changes). - for (int j = 0; j < n_; ++j) - { - a_[j] = 0; - a_first(non_one_radixes_[j]); - s_[j] = m_[j]; - f_[j] = j; - } - done_ = false; - } - - // Update one item of the tuple and return its position. - int - loopless_modular_mixed_radix_gray_code::next() - { - int j = f_[0]; - - if (j == n_) - { - done_ = true; - return -1; - } - - f_[0] = 0; - - int real_j = non_one_radixes_[j]; - - if (a_[j] == m_[j]) - { - a_[j] = 0; - a_first(real_j); - } - else - { - ++a_[j]; - a_next(real_j); - // Discover the radix on-the-fly. - if (m_[j] == -1 && a_last(real_j)) - s_[j] = m_[j] = a_[j]; - } - - if (a_[j] == s_[j]) - { - --s_[j]; - if (s_[j] < 0) - s_[j] = m_[j]; - f_[j] = f_[j + 1]; - f_[j + 1] = j + 1; - } - - return real_j; - } - -} // spot diff --git a/src/misc/modgray.hh b/src/misc/modgray.hh deleted file mode 100644 index c9327c994..000000000 --- a/src/misc/modgray.hh +++ /dev/null @@ -1,145 +0,0 @@ -// Copyright (C) 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 . - -#ifndef SPOT_MISC_MODGRAY_HH -# define SPOT_MISC_MODGRAY_HH - -namespace spot -{ - - /// \ingroup misc_tools - /// \brief Loopless modular mixed radix Gray code iteration. - /// - /// This class is based on the loopless modular mixed radix gray - /// code algorithm described in exercise 77 of "The Art of Computer - /// Programming", Pre-Fascicle 2A (Draft of section 7.2.1.1: - /// generating all n-tuples) by Donald E. Knuth. - /// - /// The idea is to enumerate the set of all n-tuples - /// (a0,a1,...,an-1) where each - /// aj range over a distinct set (this is the mixed - /// radix part), so that only one aj changes between - /// two successive tuples of the iteration (that is the Gray - /// code part), and that this changes occurs always in the same - /// direction, cycling over the set aj must cover (i.e., - /// modular). The algorithm is loopless in that - /// computing the next tuple done without any loop, i.e., in - /// constant time. - /// - /// This class does not need to know the type of the aj, - /// it will handle them indirectly through three methods: a_first(), - /// a_next(), and a_last(). These methods need to be implemented - /// in a subclass for the particular type of aj at hand. - /// - /// The class itself offers four functions to control the iteration - /// over the set of all the (a0,a1,..., - /// an-1) tuples: first(), next(), last(), and done(). - /// These functions are usually used as follows: - /// \code - /// for (g.first(); !g.done(); g.next()) - /// use the tuple - /// \endcode - /// How to use the tuple of course depends on the way - /// it as been stored in the subclass. - /// - /// Finally, let's mention two differences between this algorithm - /// and the one in Knuth's book. This version of the algorithm does - /// not need to know the radixes (i.e., the size of set of each - /// aj) beforehand: it will discover them on-the-fly when - /// a_last(j) first return true. It will also work with - /// aj that cannot be changed. (This is achieved by - /// reindexing the elements through \c non_one_radixes_, to consider - /// only the elements with a non-singleton range.) - class loopless_modular_mixed_radix_gray_code - { - public: - /// Constructor. - /// - /// \param n The size of the tuples to enumerate. - loopless_modular_mixed_radix_gray_code(int n); - - virtual ~loopless_modular_mixed_radix_gray_code(); - - /// \name iteration over an element in a tuple - /// - /// The class does not know how to modify the elements of the - /// tuple (Knuth's ajs). These changes are therefore - /// abstracted using the a_first(), a_next(), and a_last() - /// abstract functions. These need to be implemented in - /// subclasses as appropriate. - /// - /// @{ - - /// Reset aj to its initial value. - virtual void a_first(int j) = 0; - /// \brief Advance aj to its next value. - /// - /// This will never be called if a_last(j) is true. - virtual void a_next(int j) = 0; - /// Whether aj is on its last value. - virtual bool a_last(int j) const = 0; - /// @} - - /// \name iteration over all the tuples - /// @{ - - /// \brief Reset the iteration to the first tuple. - /// - /// This must be called before calling any of next(), last(), or done(). - void first(); - - /// \brief Whether this the last tuple. - /// - /// At this point it is still OK to call next(), and then done() will - /// become true. - bool - last() const - { - return f_[0] == n_; - } - - /// Whether all tuple have been explored. - bool - done() const - { - return done_; - } - - /// \brief Update one item of the tuple and return its position. - /// - /// next() should never be called if done() is true. If it is - /// called on the last tuple (i.e., last() is true), it will return - /// -1. Otherwise it will update one aj of the tuple - /// through one the aj handling functions, and return j. - int next(); - /// @} - - protected: - int n_; - bool done_; - int* a_; - int* f_; - int* m_; - int* s_; - int* non_one_radixes_; - }; - -} // spot - -# endif // SPOT_MISC_MODGRAY_HH diff --git a/wrap/python/spot.i b/wrap/python/spot.i index fd84b75e1..58dc34368 100644 --- a/wrap/python/spot.i +++ b/wrap/python/spot.i @@ -45,7 +45,6 @@ namespace std { #include "misc/version.hh" #include "misc/minato.hh" -#include "misc/modgray.hh" #include "misc/optionmap.hh" #include "misc/random.hh" @@ -161,9 +160,6 @@ using namespace spot; %include "misc/optionmap.hh" %include "misc/random.hh" -%feature("director") spot::loopless_modular_mixed_radix_gray_code; -%include "misc/modgray.hh" - %include "ltlast/formula.hh" %include "ltlast/refformula.hh" %include "ltlast/atomic_prop.hh" diff --git a/wrap/python/tests/Makefile.am b/wrap/python/tests/Makefile.am index d06660532..47c61ca4a 100644 --- a/wrap/python/tests/Makefile.am +++ b/wrap/python/tests/Makefile.am @@ -1,4 +1,4 @@ -## Copyright (C) 2010, 2012 Labortatoire de Recherche et Développement de +## Copyright (C) 2010, 2012, 2013 Labortatoire de Recherche et Développement de ## l'EPITA. ## Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -36,7 +36,6 @@ TESTS = \ ltlparse.py \ ltlsimple.py \ minato.py \ - modgray.py \ optionmap.py \ parsetgba.py \ setxor.py diff --git a/wrap/python/tests/modgray.py b/wrap/python/tests/modgray.py deleted file mode 100755 index 0779f15a0..000000000 --- a/wrap/python/tests/modgray.py +++ /dev/null @@ -1,58 +0,0 @@ -# -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2010, 2012 Laboratoire de Recherche et Développement -# de l'Epita. -# Copyright (C) 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 . - -import spot -import sys - -class test(spot.loopless_modular_mixed_radix_gray_code): - def __init__(self, lim): - spot.loopless_modular_mixed_radix_gray_code.__init__(self, len(lim)) - self.msg = list(lim) - self.lim = list(lim) - - def a_first(self, j): - self.msg[j] = 'a' - - def a_next(self, j): - self.msg[j] = chr(1 + ord(self.msg[j])) - - def a_last(self, j): - return self.msg[j] == self.lim[j] - - def run(self): - self.first() - res = [] - while not self.done(): - m = "".join(self.msg) - res.append(m) - sys.stdout.write(m + "\n") - self.next() - return res - - -t = test("acbb") - -expected = [ 'aaaa', 'abaa', 'acaa', 'acba', - 'aaba', 'abba', 'abbb', 'acbb', - 'aabb', 'aaab', 'abab', 'acab' ] - -assert t.run() == expected