From 094ddca6659ac70edef365a6b5f09a058c231b04 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 20 Oct 2004 15:46:56 +0000 Subject: [PATCH] * src/misc/modgray.hh, src/misc/modgray.cc: New files. * src/misc/Makefile.am (libmisc_la_SOURCES, misc_HEADERS): Add them. * wrap/python/spot.i: Activate directors, and interface modgray.hh. * wrap/python/tests/modgray.py: New file. * wrap/python/tests/Makefile.am (TESTS): Add it. --- ChangeLog | 8 ++ src/misc/Makefile.am | 2 + src/misc/modgray.cc | 130 ++++++++++++++++++++++++++++++ src/misc/modgray.hh | 146 ++++++++++++++++++++++++++++++++++ wrap/python/spot.i | 6 +- wrap/python/tests/Makefile.am | 3 +- wrap/python/tests/modgray.py | 58 ++++++++++++++ 7 files changed, 351 insertions(+), 2 deletions(-) create mode 100644 src/misc/modgray.cc create mode 100644 src/misc/modgray.hh create mode 100755 wrap/python/tests/modgray.py diff --git a/ChangeLog b/ChangeLog index 104cbf510..e1d338059 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,11 @@ +2004-10-20 Alexandre Duret-Lutz + + * src/misc/modgray.hh, src/misc/modgray.cc: New files. + * src/misc/Makefile.am (libmisc_la_SOURCES, misc_HEADERS): Add them. + * wrap/python/spot.i: Activate directors, and interface modgray.hh. + * wrap/python/tests/modgray.py: New file. + * wrap/python/tests/Makefile.am (TESTS): Add it. + 2004-10-18 Alexandre Duret-Lutz * iface/gspn/gspn.cc, src/ltlvisit/basicreduce.cc, diff --git a/src/misc/Makefile.am b/src/misc/Makefile.am index 2b0253fdb..ffd0b43d2 100644 --- a/src/misc/Makefile.am +++ b/src/misc/Makefile.am @@ -31,6 +31,7 @@ misc_HEADERS = \ freelist.hh \ hash.hh \ minato.hh \ + modgray.hh \ version.hh noinst_LTLIBRARIES = libmisc.la @@ -39,4 +40,5 @@ libmisc_la_SOURCES = \ escape.cc \ freelist.cc \ minato.cc \ + modgray.cc \ version.cc diff --git a/src/misc/modgray.cc b/src/misc/modgray.cc new file mode 100644 index 000000000..e45e8b6a5 --- /dev/null +++ b/src/misc/modgray.cc @@ -0,0 +1,130 @@ +// 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 2 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 Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include "modgray.hh" + +namespace spot +{ + + loopless_modular_mixed_radix_gray_code:: + loopless_modular_mixed_radix_gray_code(int n) + : n_(n), 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 new file mode 100644 index 000000000..74865f526 --- /dev/null +++ b/src/misc/modgray.hh @@ -0,0 +1,146 @@ +// 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 2 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 Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_MISC_MODGRAY_HH +# define SPOT_MISC_MODGRAY_HH + +namespace spot +{ + + /// \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() + { + return f_[0] == n_; + } + + /// Whether all tuple have been explored. + bool + done() + { + 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 7e42cc47f..2e1f85384 100644 --- a/wrap/python/spot.i +++ b/wrap/python/spot.i @@ -19,7 +19,7 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -%module spot +%module(directors="1") spot %include "std_string.i" %include "std_list.i" @@ -35,6 +35,7 @@ #include "misc/version.hh" #include "misc/bddalloc.hh" #include "misc/minato.hh" +#include "misc/modgray.hh" #include "ltlast/formula.hh" #include "ltlast/refformula.hh" @@ -91,6 +92,9 @@ using namespace spot; %include "misc/bddalloc.hh" %include "misc/minato.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 09754ae0c..23610c210 100644 --- a/wrap/python/tests/Makefile.am +++ b/wrap/python/tests/Makefile.am @@ -33,4 +33,5 @@ TESTS = \ bddnqueen.py \ ltl2tgba.test \ interdep.py \ - minato.py + minato.py \ + modgray.py diff --git a/wrap/python/tests/modgray.py b/wrap/python/tests/modgray.py new file mode 100755 index 000000000..3c10b09b9 --- /dev/null +++ b/wrap/python/tests/modgray.py @@ -0,0 +1,58 @@ +# -*- mode: python; coding: iso-8859-1 -*- +# 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 2 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 Spot; see the file COPYING. If not, write to the Free +# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +# 02111-1307, USA. + +import ltihooks +import spot + +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) + print m + self.next() + return res + + +t = test("acbb") + +expected = [ 'aaaa', 'abaa', 'acaa', 'acba', + 'aaba', 'abba', 'abbb', 'acbb', + 'aabb', 'aaab', 'abab', 'acab' ] + +assert t.run() == expected