From 7cb6ff331dcb8a95bb157c5bba781c1fa8019d0b Mon Sep 17 00:00:00 2001 From: Guillaume Sadegh Date: Mon, 30 Nov 2009 23:22:13 +0100 Subject: [PATCH] =?UTF-8?q?Add=20a=20new=20type=20of=20automata:=20State-l?= =?UTF-8?q?abeled=20Alternating=20B=C3=BCchi=20Automata=20(SABA).?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * src/saba/saba.hh, src/saba/saba.cc, src/saba/sabastate.hh, src/saba/sabasucciter.hh: New. Interface for SABA (State-labeled Alternating Büchi Automata). * src/saba/explicitstateconjunction.cc, src/saba/explicitstateconjunction.hh: New. Default implementation for a conjunction of states. * src/saba/Makefile.am: New. * src/Makefile.am, configure.ac: Adjust. * src/sabaalgos/sabareachiter.cc, src/sabaalgos/sabareachiter.hh: New. Iterate over all reachable states of a spot::saba. * src/sabaalgos/sabadotty.cc, src/sabaalgos/sabadotty.hh: New. Print reachable states in dot format. * src/sabaalgos/Makefile.am: New. --- ChangeLog | 20 +++ configure.ac | 4 + src/Makefile.am | 11 +- src/saba/Makefile.am | 38 +++++ src/saba/explicitstateconjunction.cc | 91 ++++++++++ src/saba/explicitstateconjunction.hh | 79 +++++++++ src/saba/saba.cc | 52 ++++++ src/saba/saba.hh | 117 +++++++++++++ src/saba/sabastate.hh | 246 +++++++++++++++++++++++++++ src/saba/sabasucciter.hh | 160 +++++++++++++++++ src/sabaalgos/Makefile.am | 30 ++++ src/sabaalgos/sabadotty.cc | 111 ++++++++++++ src/sabaalgos/sabadotty.hh | 38 +++++ src/sabaalgos/sabareachiter.cc | 189 ++++++++++++++++++++ src/sabaalgos/sabareachiter.hh | 150 ++++++++++++++++ 15 files changed, 1331 insertions(+), 5 deletions(-) create mode 100644 src/saba/Makefile.am create mode 100644 src/saba/explicitstateconjunction.cc create mode 100644 src/saba/explicitstateconjunction.hh create mode 100644 src/saba/saba.cc create mode 100644 src/saba/saba.hh create mode 100644 src/saba/sabastate.hh create mode 100644 src/saba/sabasucciter.hh create mode 100644 src/sabaalgos/Makefile.am create mode 100644 src/sabaalgos/sabadotty.cc create mode 100644 src/sabaalgos/sabadotty.hh create mode 100644 src/sabaalgos/sabareachiter.cc create mode 100644 src/sabaalgos/sabareachiter.hh diff --git a/ChangeLog b/ChangeLog index 6e9799bdb..829d77b7a 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,23 @@ +2009-11-30 Guillaume Sadegh + + Add a new type of automata: State-labeled Alternating Büchi + Automata (SABA). + + * src/saba/saba.hh, src/saba/saba.cc, src/saba/sabastate.hh, + src/saba/sabasucciter.hh: New. Interface for + SABA (State-labeled Alternating Büchi Automata). + * src/saba/explicitstateconjunction.cc, + src/saba/explicitstateconjunction.hh: New. Default + implementation for a conjunction of states. + * src/saba/Makefile.am: New. + * src/Makefile.am, configure.ac: Adjust. + * src/sabaalgos/sabareachiter.cc, + src/sabaalgos/sabareachiter.hh: New. Iterate over all reachable + states of a spot::saba. + * src/sabaalgos/sabadotty.cc, src/sabaalgos/sabadotty.hh: New. + Print reachable states in dot format. + * src/sabaalgos/Makefile.am: New. + 2009-11-27 Guillaume Sadegh Rename the class taa as taa_tgba. diff --git a/configure.ac b/configure.ac index 8845cb03a..7c2a9968c 100644 --- a/configure.ac +++ b/configure.ac @@ -108,6 +108,10 @@ AC_CONFIG_FILES([ src/Makefile src/misc/Makefile src/sanity/Makefile + src/saba/Makefile + src/sabaalgos/Makefile + src/sabatest/defs + src/sabatest/Makefile src/tgbaalgos/gtec/Makefile src/tgbaalgos/Makefile src/tgba/Makefile diff --git a/src/Makefile.am b/src/Makefile.am index d33944fe1..f2ff54cd3 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -23,11 +23,10 @@ AUTOMAKE_OPTIONS = subdir-objects # List directories in the order they must be built. # Keep tests at the end. -SUBDIRS = misc ltlenv ltlast ltlvisit ltlparse eltlparse \ - tgba tgbaalgos tgbaparse \ - evtgba evtgbaalgos evtgbaparse \ - kripke . \ - ltltest eltltest tgbatest evtgbatest sanity +SUBDIRS = misc ltlenv ltlast ltlvisit ltlparse eltlparse tgba \ + tgbaalgos tgbaparse evtgba evtgbaalgos evtgbaparse kripke \ + saba sabaalgos ltltest eltltest tgbatest evtgbatest sabatest \ + sanity lib_LTLIBRARIES = libspot.la libspot_la_SOURCES = @@ -45,6 +44,8 @@ libspot_la_LIBADD = \ evtgba/libevtgba.la \ evtgbaalgos/libevtgbaalgos.la \ evtgbaparse/libevtgbaparse.la \ + saba/libsaba.la \ + sabaalgos/libsabaalgos.la \ kripke/libkripke.la # Dummy C++ source to cause C++ linking. diff --git a/src/saba/Makefile.am b/src/saba/Makefile.am new file mode 100644 index 000000000..37527c6bc --- /dev/null +++ b/src/saba/Makefile.am @@ -0,0 +1,38 @@ +## Copyright (C) 2009 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. + +AM_CPPFLAGS = -I$(srcdir)/.. $(BUDDY_CPPFLAGS) +AM_CXXFLAGS = $(WARNING_CXXFLAGS) + +sabadir = $(pkgincludedir)/saba + +saba_HEADERS = \ + explicitstateconjunction.hh \ + saba.hh \ + sabastate.hh \ + sabasucciter.hh \ + sabacomplementtgba.hh + +noinst_LTLIBRARIES = libsaba.la +libsaba_la_SOURCES = \ + explicitstateconjunction.cc \ + saba.cc \ + sabacomplementtgba.cc diff --git a/src/saba/explicitstateconjunction.cc b/src/saba/explicitstateconjunction.cc new file mode 100644 index 000000000..4ffed619b --- /dev/null +++ b/src/saba/explicitstateconjunction.cc @@ -0,0 +1,91 @@ +// Copyright (C) 2009 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 "explicitstateconjunction.hh" + +namespace spot +{ + + /// explicit_state_conjunction + //////////////////////////////////////// + + explicit_state_conjunction::explicit_state_conjunction() + { + } + + explicit_state_conjunction:: + explicit_state_conjunction(const explicit_state_conjunction* other) + : set_(other->set_) + { + } + + explicit_state_conjunction* + explicit_state_conjunction::operator=(const explicit_state_conjunction& o) + { + if (this != &o) + { + this->~explicit_state_conjunction(); + new (this) explicit_state_conjunction(&o); + } + return this; + } + + explicit_state_conjunction::~explicit_state_conjunction() + { + } + + void + explicit_state_conjunction::first() + { + it_ = set_.begin(); + } + + void + explicit_state_conjunction::next() + { + ++it_; + } + + bool + explicit_state_conjunction::done() const + { + return it_ == set_.end(); + } + + explicit_state_conjunction* + explicit_state_conjunction::clone() const + { + return new explicit_state_conjunction(this); + } + + saba_state* + explicit_state_conjunction::current_state() const + { + return (*it_)->clone(); + } + + void + explicit_state_conjunction::add(saba_state* state) + { + set_.insert(shared_saba_state(state)); + } + +} // end namespace spot. diff --git a/src/saba/explicitstateconjunction.hh b/src/saba/explicitstateconjunction.hh new file mode 100644 index 000000000..ef43d997d --- /dev/null +++ b/src/saba/explicitstateconjunction.hh @@ -0,0 +1,79 @@ +// Copyright (C) 2009 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_SABA_EXPLICITSTATECONJUNCTION_HH +# define SPOT_SABA_EXPLICITSTATECONJUNCTION_HH + +#include +#include "sabasucciter.hh" + +namespace spot +{ + /// \brief Basic implementation of saba_state_conjunction. + /// \ingroup saba_essentials + /// + /// This class provides a basic implementation to + /// iterate over a conjunction of states of a saba. + class explicit_state_conjunction : public saba_state_conjunction + { + public: + + explicit_state_conjunction(); + explicit_state_conjunction(const explicit_state_conjunction* other); + virtual ~explicit_state_conjunction(); + + explicit_state_conjunction* operator=(const explicit_state_conjunction& o); + + /// \name Iteration + //@{ + + virtual void first(); + virtual void next(); + virtual bool done() const; + + //@} + + /// \name Inspection + //@{ + + /// Duplicate a this conjunction. + explicit_state_conjunction* clone() const; + + /// Return the a new instance on the current state. + /// This is the caller responsibility to delete the returned state. + virtual saba_state* current_state() const; + + //@} + + /// Add a new state in the conjunction. + /// The class becomes owner of \a state. + void add(saba_state* state); + private: + typedef Sgi::hash_set saba_state_set_t; + saba_state_set_t set_; + saba_state_set_t::iterator it_; + }; +} // end namespace spot. + + +#endif // SPOT_SABA_EXPLICITSTATECONJUNCTION_HH diff --git a/src/saba/saba.cc b/src/saba/saba.cc new file mode 100644 index 000000000..cc31a911b --- /dev/null +++ b/src/saba/saba.cc @@ -0,0 +1,52 @@ +// Copyright (C) 2009 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 "saba.hh" + +namespace spot +{ + saba::saba() + : num_acc_(-1) + { + } + + saba::~saba() + { + } + + unsigned int + saba::number_of_acceptance_conditions() const + { + if (num_acc_ < 0) + { + bdd all = all_acceptance_conditions(); + unsigned int n = 0; + while (all != bddfalse) + { + ++n; + all -= bdd_satone(all); + } + num_acc_ = n; + } + return num_acc_; + } + +} // end namespace spot. diff --git a/src/saba/saba.hh b/src/saba/saba.hh new file mode 100644 index 000000000..47f733eec --- /dev/null +++ b/src/saba/saba.hh @@ -0,0 +1,117 @@ +// Copyright (C) 2009 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_SABA_SABA_HH +# define SPOT_SABA_SABA_HH + +#include "sabastate.hh" +#include "sabasucciter.hh" +#include + +namespace spot +{ + /// \defgroup saba SABA (State-based Alternating Büchi Automata) + /// + /// Spot was centered around non-deterministic \ref tgba. + /// Alternating automata are an extension to non-deterministic + /// automata, and are presented with spot::saba. + /// This type and its cousins are listed \ref saba_essentials "here". + /// This is an abstract interface. + + /// \addtogroup saba_essentials Essential SABA types + /// \ingroup saba + + /// \brief A State-based Alternating (Generalized) Büchi Automaton. + /// \ingroup saba_essentials + /// + /// Browsing such automaton can be achieved using two functions: + /// \c get_init_state, and \c succ_iter. The former returns + /// the initial state while the latter lists the + /// successor states of any state. + /// + /// Note that although this is a transition-based automata, + /// we never represent transitions! Transition informations are + /// obtained by querying the iterator over the successors of + /// a state. + class saba + { + protected: + saba(); + + public: + virtual ~saba(); + + /// \brief Get the initial state of the automaton. + /// + /// The state has been allocated with \c new. It is the + /// responsability of the caller to \c delete it when no + /// longer needed. + virtual saba_state* get_init_state() const = 0; + + /// \brief Get an iterator over the successors of \a local_state. + /// + /// The iterator has been allocated with \c new. It is the + /// responsability of the caller to \c delete it when no + /// longer needed. + /// + /// \param local_state The state whose successors are to be explored. + /// This pointer is not adopted in any way by \c succ_iter, and + /// it is still the caller's responsability to delete it when + /// appropriate (this can be done during the lifetime of + /// the iterator). + virtual saba_succ_iterator* + succ_iter(const saba_state* local_state) const = 0; + + /// \brief Get the dictionary associated to the automaton. + /// + /// State are represented as BDDs. The dictionary allows + /// to map BDD variables back to formulae, and vice versa. + /// This is useful when dealing with several automata (which + /// may use the same BDD variable for different formula), + /// or simply when printing. + virtual bdd_dict* get_dict() const = 0; + + /// \brief Format the state as a string for printing. + /// + /// This formating is the responsability of the automata + /// that owns the state. + virtual std::string format_state(const saba_state* state) const = 0; + + /// \brief Return the set of all acceptance conditions used + /// by this automaton. + /// + /// The goal of the emptiness check is to ensure that + /// a strongly connected component walks through each + /// of these acceptiong conditions. I.e., the union + /// of the acceptiong conditions of all transition in + /// the SCC should be equal to the result of this function. + virtual bdd all_acceptance_conditions() const = 0; + + /// The number of acceptance conditions. + virtual unsigned int number_of_acceptance_conditions() const; + private: + mutable int num_acc_; + }; + +} // end namespace spot. + + +#endif // SPOT_SABA_SABA_HH diff --git a/src/saba/sabastate.hh b/src/saba/sabastate.hh new file mode 100644 index 000000000..9e3319724 --- /dev/null +++ b/src/saba/sabastate.hh @@ -0,0 +1,246 @@ +// Copyright (C) 2009 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_SABA_SABASTATE_HH +# define SPOT_SABA_SABASTATE_HH + +#include +#include +#include + +namespace spot +{ + + /// \brief Abstract class for saba states. + /// \ingroup saba_essentials + class saba_state + { + public: + /// \brief Compares two states (that come from the same automaton). + /// + /// This method returns an integer less than, equal to, or greater + /// than zero if \a this is found, respectively, to be less than, equal + /// to, or greater than \a other according to some implicit total order. + /// + /// This method should not be called to compare states from + /// different automata. + /// + /// \sa spot::saba_state_ptr_less_than + virtual int compare(const saba_state* other) const = 0; + + /// \brief Hash a state. + /// + /// This method returns an integer that can be used as a + /// hash value for this state. + /// + /// Note that the hash value is guaranteed to be unique for all + /// equal states (in compare()'s sense) for only has long has one + /// of these states exists. So it's OK to use a spot::saba_state as a + /// key in a \c hash_map because the mere use of the state as a + /// key in the hash will ensure the state continues to exist. + /// + /// However if you create the state, get its hash key, delete the + /// state, recreate the same state, and get its hash key, you may + /// obtain two different hash keys if the same state were not + /// already used elsewhere. In practice this weird situation can + /// occur only when the state is BDD-encoded, because BDD numbers + /// (used to build the hash value) can be reused for other + /// formulas. That probably doesn't matter, since the hash value + /// is meant to be used in a \c hash_map, but it had to be noted. + virtual size_t hash() const = 0; + + /// Duplicate a state. + virtual saba_state* clone() const = 0; + + /// \brief Get the acceptance condition. + /// + /// saba are state-labeled automata, then their acceptance conditions + /// are labeled on states. + virtual bdd acceptance_conditions() const = 0; + + virtual ~saba_state() + { + } + }; + + /// \brief Strict Weak Ordering for \c saba_state*. + /// \ingroup saba_essentials + /// + /// This is meant to be used as a comparison functor for + /// STL \c map whose key are of type \c saba_state*. + /// + /// For instance here is how one could declare + /// a map of \c saba_state*. + /// \code + /// // Remember how many times each state has been visited. + /// std::map seen; + /// \endcode + struct saba_state_ptr_less_than: + public std::binary_function + { + bool + operator()(const saba_state* left, const saba_state* right) const + { + assert(left); + return left->compare(right) < 0; + } + }; + + /// \brief An Equivalence Relation for \c saba_state*. + /// \ingroup saba_essentials + /// + /// This is meant to be used as a comparison functor for + /// Sgi \c hash_map whose key are of type \c saba_state*. + /// + /// For instance here is how one could declare + /// a map of \c saba_state*. + /// \code + /// // Remember how many times each state has been visited. + /// Sgi::hash_map seen; + /// \endcode + struct saba_state_ptr_equal: + public std::binary_function + { + bool + operator()(const saba_state* left, const saba_state* right) const + { + assert(left); + return 0 == left->compare(right); + } + }; + + /// \brief Hash Function for \c saba_state*. + /// \ingroup saba_essentials + /// \ingroup hash_funcs + /// + /// This is meant to be used as a hash functor for + /// Sgi's \c hash_map whose key are of type \c saba_state*. + /// + /// For instance here is how one could declare + /// a map of \c saba_state*. + /// \code + /// // Remember how many times each state has been visited. + /// Sgi::hash_map seen; + /// \endcode + struct saba_state_ptr_hash: + public std::unary_function + { + size_t + operator()(const saba_state* that) const + { + assert(that); + return that->hash(); + } + }; + + // Functions related to shared_ptr. + ////////////////////////////////////////////////// + + typedef boost::shared_ptr shared_saba_state; + + /// \brief Strict Weak Ordering for \c shared_saba_state + /// (shared_ptr). + /// \ingroup saba_essentials + /// + /// This is meant to be used as a comparison functor for + /// STL \c map whose key are of type \c shared_saba_state. + /// + /// For instance here is how one could declare + /// a map of \c shared_saba_state. + /// \code + /// // Remember how many times each state has been visited. + /// std::map + /// seen; + /// \endcode + struct saba_state_shared_ptr_less_than: + public std::binary_function + { + bool + operator()(shared_saba_state left, + shared_saba_state right) const + { + assert(left); + return left->compare(right.get()) < 0; + } + }; + + /// \brief An Equivalence Relation for \c shared_saba_state + /// (shared_ptr). + /// \ingroup saba_essentials + /// + /// This is meant to be used as a comparison functor for + /// Sgi \c hash_map whose key are of type \c shared_saba_state. + /// + /// For instance here is how one could declare + /// a map of \c shared_saba_state + /// \code + /// // Remember how many times each state has been visited. + /// Sgi::hash_map seen; + /// \endcode + struct saba_state_shared_ptr_equal: + public std::binary_function + { + bool + operator()(shared_saba_state left, + shared_saba_state right) const + { + assert(left); + return 0 == left->compare(right.get()); + } + }; + + /// \brief Hash Function for \c shared_saba_state + /// (shared_ptr). + /// \ingroup saba_essentials + /// \ingroup hash_funcs + /// + /// This is meant to be used as a hash functor for + /// Sgi's \c hash_map whose key are of type + /// \c shared_saba_state. + /// + /// For instance here is how one could declare + /// a map of \c shared_saba_state. + /// \code + /// // Remember how many times each state has been visited. + /// Sgi::hash_map seen; + /// \endcode + struct saba_state_shared_ptr_hash: + public std::unary_function + { + size_t + operator()(shared_saba_state that) const + { + assert(that); + return that->hash(); + } + }; + +} + +#endif // SPOT_SABA_SABASTATE_HH diff --git a/src/saba/sabasucciter.hh b/src/saba/sabasucciter.hh new file mode 100644 index 000000000..58188d669 --- /dev/null +++ b/src/saba/sabasucciter.hh @@ -0,0 +1,160 @@ +// Copyright (C) 2009 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_SABA_SABASUCCITER_HH +# define SPOT_SABA_SABASUCCITER_HH + +#include "sabastate.hh" + +namespace spot +{ + /// \brief Iterate over a conjunction of saba_state. + /// \ingroup saba_essentials + /// + /// This class provides the basic functionalities required to + /// iterate over a conjunction of states of a saba. + class saba_state_conjunction + { + public: + virtual + ~saba_state_conjunction() + { + } + + /// \name Iteration + //@{ + + /// \brief Position the iterator on the first successor of the conjunction + /// (if any). + /// + /// This method can be called several times to make multiple + /// passes over successors. + /// + /// \warning One should always call \c done() to + /// ensure there is a successor, even after \c first(). A + /// common trap is to assume that there is at least one + /// successor: this is wrong. + virtual void first() = 0; + + /// \brief Jump to the next successor (if any). + /// + /// \warning Again, one should always call \c done() to ensure + /// there is a successor. + virtual void next() = 0; + + /// \brief Check whether the iteration over a conjunction of states + /// is finished. + /// + /// This function should be called after any call to \c first() + /// or \c next() and before any enquiry about the current state. + virtual bool done() const = 0; + + //@} + + /// \name Inspection + //@{ + + /// \brief Get the state of the current successor. + /// + /// Note that the same state may occur at different points + /// in the iteration. These actually correspond to the same + /// destination. It just means there were several transitions, + /// with different conditions, leading to the same state. + /// + /// \warning the state is allocated with new, its deletion is + /// the responsibility of the caller. + virtual saba_state* current_state() const = 0; + + //@} + + /// Duplicate a saba_state conjunction. + virtual saba_state_conjunction* clone() const = 0; + }; + + + /// \brief Iterate over the successors of a saba_state. + /// \ingroup saba_essentials + /// + /// This class provides the basic functionalities required to + /// iterate over the successors of a state of a saba. Since + /// transitions of an alternating automaton are defined as a + /// boolean function with conjunctions (universal) and + /// disjunctions (non-deterministic), + class saba_succ_iterator + { + public: + virtual + ~saba_succ_iterator() + { + } + + /// \name Iteration + //@{ + + /// \brief Position the iterator on the first conjunction + /// of successors (if any). + /// + /// This method can be called several times to make multiple + /// passes over successors. + /// + /// \warning One should always call \c done() to + /// ensure there is a successor, even after \c first(). A + /// common trap is to assume that there is at least one + /// successor: this is wrong. + virtual void first() = 0; + + /// \brief Jump to the next conjunction of successors (if any). + /// + /// \warning Again, one should always call \c done() to ensure + /// there is a successor. + virtual void next() = 0; + + /// \brief Check whether the iteration is finished. + /// + /// This function should be called after any call to \c first() + /// or \c next() and before any enquiry about the current state. + /// + /// The usual way to do this is with a \c for loop. + /// \code + /// for (s->first(); !s->done(); s->next()) + /// ... + /// \endcode + virtual bool done() const = 0; + + //@} + + /// \name Inspection + //@{ + + /// \brief Get current conjunction of successor states. + virtual saba_state_conjunction* current_conjunction() const = 0; + + /// \brief Get the condition on the transition leading to this successor. + /// + /// This is a boolean function of atomic propositions. + virtual bdd current_condition() const = 0; + + //@} + }; +} + + +#endif // SPOT_TGBA_SUCCITER_HH diff --git a/src/sabaalgos/Makefile.am b/src/sabaalgos/Makefile.am new file mode 100644 index 000000000..7488db283 --- /dev/null +++ b/src/sabaalgos/Makefile.am @@ -0,0 +1,30 @@ +## Copyright (C) 2009 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. + +AM_CPPFLAGS = -I$(srcdir)/.. $(BUDDY_CPPFLAGS) +AM_CXXFLAGS = $(WARNING_CXXFLAGS) + +sabaalgosdir = $(pkgincludedir)/sabaalgos + +sabaalgos_HEADERS = sabadotty.hh sabareachiter.hh + +noinst_LTLIBRARIES = libsabaalgos.la +libsabaalgos_la_SOURCES = sabadotty.cc sabareachiter.cc diff --git a/src/sabaalgos/sabadotty.cc b/src/sabaalgos/sabadotty.cc new file mode 100644 index 000000000..cf0109705 --- /dev/null +++ b/src/sabaalgos/sabadotty.cc @@ -0,0 +1,111 @@ +// Copyright (C) 2009 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 +#include "saba/saba.hh" +#include "sabadotty.hh" +#include "tgba/bddprint.hh" +#include "sabareachiter.hh" +#include "misc/escape.hh" + +namespace spot +{ + namespace + { + class saba_dotty_bfs : public saba_reachable_iterator_breadth_first + { + public: + saba_dotty_bfs(std::ostream& os, const saba* a) + : saba_reachable_iterator_breadth_first(a), os_(os) + { + } + + void + start() + { + os_ << "digraph G {" << std::endl; + os_ << " 0 [label=\"\", style=invis, height=0]" << std::endl; + os_ << " 0 -> 1;" << std::endl; + } + + void + end() + { + os_ << "}" << std::endl; + } + + void + process_state(const saba_state* s, int n) + { + std::string label = + escape_str(automata_->format_state(s)) + + "\\n" + + bdd_format_accset(automata_->get_dict(), + s->acceptance_conditions()); + os_ << " " << n << " " + << "[label=\"" << label << "\"];" + << std::endl; + } + + void + process_state_conjunction(const saba_state*, int in, + const saba_state_conjunction*, + int sc_id, + const saba_succ_iterator* si) + { + os_ << " s" << in << "sc" << sc_id + << " [label=\"\", style=invis, height=0];" << std::endl; + + std::string label = + bdd_format_formula(automata_->get_dict(), + si->current_condition()); + + os_ << " " << in << " -> s" << in << "sc" << sc_id + << " [label=\"" << label << "\", arrowhead=\"none\"];" + << std::endl; + } + + void + process_link(const saba_state*, int in, + const saba_state*, int out, + const saba_state_conjunction*, + int sc_id, + const saba_succ_iterator*) + { + os_ << " s" << in << "sc" << sc_id << " -> " << out + << " [label=\"\"];" + << std::endl; + } + + private: + std::ostream& os_; + }; + } + + std::ostream& + saba_dotty_reachable(std::ostream& os, const saba* g) + { + saba_dotty_bfs d(os, g); + d.run(); + return os; + } + +} diff --git a/src/sabaalgos/sabadotty.hh b/src/sabaalgos/sabadotty.hh new file mode 100644 index 000000000..4e8b92169 --- /dev/null +++ b/src/sabaalgos/sabadotty.hh @@ -0,0 +1,38 @@ +// Copyright (C) 2009 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_SABAALGOS_SABADOTTY_HH +# define SPOT_SABAALGOS_SABADOTTY_HH + +#include + +namespace spot +{ + class saba; + + /// \brief Print reachable states in dot format. + /// \ingroup saba_io + std::ostream& + saba_dotty_reachable(std::ostream& os, + const saba* g); +} + +#endif // SPOT_SABAALGOS_SABADOTTY_HH diff --git a/src/sabaalgos/sabareachiter.cc b/src/sabaalgos/sabareachiter.cc new file mode 100644 index 000000000..951457c0e --- /dev/null +++ b/src/sabaalgos/sabareachiter.cc @@ -0,0 +1,189 @@ +// Copyright (C) 2009 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 +#include "sabareachiter.hh" + +namespace spot +{ + // saba_reachable_iterator + ////////////////////////////////////////////////////////////////////// + + saba_reachable_iterator::saba_reachable_iterator(const saba* a) + : automata_(a) + { + } + + saba_reachable_iterator::~saba_reachable_iterator() + { + seen_map::const_iterator s = seen.begin(); + while (s != seen.end()) + { + // Advance the iterator before deleting the "key" pointer. + const saba_state* ptr = s->first; + ++s; + delete ptr; + } + } + + void + saba_reachable_iterator::run() + { + int n = 0; + int conjn = 0; + + start(); + saba_state* i = automata_->get_init_state(); + if (want_state(i)) + add_state(i); + seen[i] = ++n; + const saba_state* t; + while ((t = next_state())) + { + assert(seen.find(t) != seen.end()); + int tn = seen[t]; + saba_succ_iterator* si = automata_->succ_iter(t); + process_state(t, tn); + for (si->first(); !si->done(); si->next()) + { + saba_state_conjunction* conj = si->current_conjunction(); + ++conjn; + process_state_conjunction(t, tn, conj, conjn, si); + + for (conj->first(); !conj->done(); conj->next()) + { + const saba_state* current = conj->current_state(); + seen_map::const_iterator s = seen.find(current); + bool ws = want_state(current); + + if (s == seen.end()) + { + seen[current] = ++n; + if (ws) + { + add_state(current); + process_link(t, tn, current, n, conj, conjn, si); + } + } + else + { + if (ws) + process_link(t, tn, s->first, s->second, conj, conjn, si); + delete current; + } + } + delete conj; + } + delete si; + } + end(); + } + + bool + saba_reachable_iterator::want_state(const saba_state*) const + { + return true; + } + + void + saba_reachable_iterator::start() + { + } + + void + saba_reachable_iterator::end() + { + } + + void + saba_reachable_iterator::process_state(const saba_state*, int) + { + } + + void + saba_reachable_iterator:: + process_state_conjunction(const saba_state*, int, + const saba_state_conjunction*, + int, + const saba_succ_iterator*) + { + } + + void + saba_reachable_iterator::process_link(const saba_state*, int, + const saba_state*, int, + const saba_state_conjunction*, + int, + const saba_succ_iterator*) + { + } + + // saba_reachable_iterator_depth_first + ////////////////////////////////////////////////////////////////////// + + saba_reachable_iterator_depth_first:: + saba_reachable_iterator_depth_first(const saba* a) + : saba_reachable_iterator(a) + { + } + + void + saba_reachable_iterator_depth_first::add_state(const saba_state* s) + { + todo.push(s); + } + + const saba_state* + saba_reachable_iterator_depth_first::next_state() + { + if (todo.empty()) + return 0; + const saba_state* s = todo.top(); + todo.pop(); + return s; + } + + // saba_reachable_iterator_breadth_first + ////////////////////////////////////////////////////////////////////// + + saba_reachable_iterator_breadth_first:: + saba_reachable_iterator_breadth_first(const saba* a) + : saba_reachable_iterator(a) + { + } + + void + saba_reachable_iterator_breadth_first::add_state(const saba_state* s) + { + todo.push_back(s); + } + + const saba_state* + saba_reachable_iterator_breadth_first::next_state() + { + if (todo.empty()) + return 0; + const saba_state* s = todo.front(); + todo.pop_front(); + return s; + } + +} diff --git a/src/sabaalgos/sabareachiter.hh b/src/sabaalgos/sabareachiter.hh new file mode 100644 index 000000000..c94f48680 --- /dev/null +++ b/src/sabaalgos/sabareachiter.hh @@ -0,0 +1,150 @@ +// Copyright (C) 2009 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_SABAALGOS_SABAREACHITER_HH +# define SPOT_SABAALGOS_SABAREACHITER_HH + +#include "misc/hash.hh" +#include "saba/saba.hh" +#include +#include + +namespace spot +{ + /// \brief Iterate over all reachable states of a spot::saba. + /// \ingroup saba_generic + class saba_reachable_iterator + { + public: + saba_reachable_iterator(const saba* a); + virtual ~saba_reachable_iterator(); + + /// \brief Iterate over all reachable states of a spot::saba. + /// + /// This is a template method that will call add_state(), next_state(), + /// start(), end(), process_state(), process_state_conjunction() and + /// process_link(), while it iterates over states. + void run(); + + /// \name Todo list management. + /// + /// spot::saba_reachable_iterator_depth_first and + /// spot::saba_reachable_iterator_breadth_first offer two precanned + /// implementations for these functions. + /// \{ + /// \brief Called by run() to register newly discovered states. + virtual void add_state(const saba_state* s) = 0; + /// \brief Called by run() to obtain the next state to process. + virtual const saba_state* next_state() = 0; + /// \} + + /// Called by add_state or next_states implementations to filter + /// states. Default implementation always return true. + virtual bool want_state(const saba_state* s) const; + + /// Called by run() before starting its iteration. + virtual void start(); + /// Called by run() once all states have been explored. + virtual void end(); + + /// Called by run() to process a state. + /// + /// \param s The current state. + /// \param n A unique number assigned to \a s. + virtual void process_state(const saba_state* s, int n); + + /// Called by run() to process a conjunction of states. + /// + /// \param in_s The current state. + /// \param in An unique number assigned to \a in_s. + /// \param sc The spot::saba_state_conjunction positionned on the current + /// conjunction. + /// \param sc_id An unique number for the this transition assigned to \a sc. + /// \param si The spot::saba_succ_iterator positionned on the current + /// transition. + virtual void + process_state_conjunction(const saba_state* in_s, int in, + const saba_state_conjunction* sc, + int sc_id, + const saba_succ_iterator* si); + /// Called by run() to process a transition. + /// + /// \param in_s The source state + /// \param in The source state number. + /// \param out_s The destination state + /// \param out The destination state number. + /// \param sc The spot::saba_state_conjunction positionned on the current + /// conjunction. + /// \param sc_id An unique number for the this transition assigned to \a sc. + /// + /// The in_s and out_s states are owned by the + /// spot::saba_reachable_iterator instance and destroyed when the + /// instance is destroyed. + virtual void + process_link(const saba_state* in_s, int in, + const saba_state* out_s, int out, + const saba_state_conjunction* sc, + int sc_id, + const saba_succ_iterator* si); + + protected: + const saba* automata_; ///< The spot::saba to explore. + + typedef Sgi::hash_map seen_map; + seen_map seen; ///< States already seen. + }; + + /// \brief An implementation of spot::saba_reachable_iterator that browses + /// states depth first. + /// \ingroup saba_generic + class saba_reachable_iterator_depth_first : public saba_reachable_iterator + { + public: + saba_reachable_iterator_depth_first(const saba* a); + + virtual void add_state(const saba_state* s); + virtual const saba_state* next_state(); + + protected: + std::stack todo; ///< A stack of states yet to explore. + }; + + /// \brief An implementation of spot::saba_reachable_iterator that browses + /// states breadth first. + /// \ingroup saba_generic + class saba_reachable_iterator_breadth_first : public saba_reachable_iterator + { + public: + saba_reachable_iterator_breadth_first(const saba* a); + + virtual void add_state(const saba_state* s); + virtual const saba_state* next_state(); + + protected: + std::deque todo; ///< A queue of states yet to explore. + }; + + +} + + +#endif // SPOT_SABAALGOS_SABAREACHITER_HH