From 3f0e95f061d99d026512fda8b7da49802dbcbf56 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 27 May 2003 10:40:16 +0000 Subject: [PATCH] * src/tgba/succiter.hh (tgba_succ_iterator::current_state): Return a state*, not a state_bdd. * src/tgba/succiterconcrete.hh (tgba_succ_iterator_concrete::current_state): Return a state_bdd*, not a state_bdd. * src/tgba/state.hh (state::as_bdd): New abstract method. * src/tgba/statebdd.hh (state_bdd::as_bdd): Move definitions ... * src/tgba/statebdd.cc (state_bdd::as_bdd): ... here. * src/tgba/tgba.hh: Add Doxygen comments. (tgba::succ_iter, tgba::get_init_state): Use state*, not state_bdd. * src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete::get_init_state): Return a state_bdd*, not a state_bdd. (tgba_bdd_concrete::get_init_bdd): New method. (tgba_bdd_concrete::succ_uter): Take a state* as argument. * src/tgba/tgbabddconcrete.cc: Likewise. * src/tgba/tgbabddtranslatefactory.cc (tgba_bdd_translate_factory::tgba_bdd_translate_factory): Use tgba_bdd_concrete::get_init_bdd. * src/tgbaalgos/dotty.cc (dotty_state, dotty_rec, dotty): Adjust to use state* instead of state_bdd. * src/tgba/succlist.hh: Delete. (Leftover from a previous draft.) --- ChangeLog | 25 ++++++++++++++ src/tgba/state.hh | 4 +++ src/tgba/statebdd.cc | 7 ++++ src/tgba/statebdd.hh | 7 +--- src/tgba/succiter.hh | 12 +++---- src/tgba/succiterconcrete.cc | 20 +++++------ src/tgba/succiterconcrete.hh | 9 ++--- src/tgba/succlist.hh | 15 --------- src/tgba/tgba.hh | 52 +++++++++++++++++++++++++++-- src/tgba/tgbabddconcrete.cc | 14 ++++++-- src/tgba/tgbabddconcrete.hh | 5 +-- src/tgba/tgbabddtranslatefactory.cc | 2 +- src/tgbaalgos/dotty.cc | 31 +++++++++-------- 13 files changed, 139 insertions(+), 64 deletions(-) delete mode 100644 src/tgba/succlist.hh diff --git a/ChangeLog b/ChangeLog index 1b70f0749..6fd24a13e 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,28 @@ +2003-05-27 Alexandre Duret-Lutz + + * src/tgba/succiter.hh (tgba_succ_iterator::current_state): + Return a state*, not a state_bdd. + * src/tgba/succiterconcrete.hh + (tgba_succ_iterator_concrete::current_state): Return a state_bdd*, + not a state_bdd. + * src/tgba/state.hh (state::as_bdd): New abstract method. + * src/tgba/statebdd.hh (state_bdd::as_bdd): Move definitions ... + * src/tgba/statebdd.cc (state_bdd::as_bdd): ... here. + * src/tgba/tgba.hh: Add Doxygen comments. + (tgba::succ_iter, tgba::get_init_state): Use state*, not state_bdd. + * src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete::get_init_state): + Return a state_bdd*, not a state_bdd. + (tgba_bdd_concrete::get_init_bdd): New method. + (tgba_bdd_concrete::succ_uter): Take a state* as argument. + * src/tgba/tgbabddconcrete.cc: Likewise. + * src/tgba/tgbabddtranslatefactory.cc + (tgba_bdd_translate_factory::tgba_bdd_translate_factory): Use + tgba_bdd_concrete::get_init_bdd. + * src/tgbaalgos/dotty.cc (dotty_state, dotty_rec, dotty): Adjust + to use state* instead of state_bdd. + * src/tgba/succlist.hh: Delete. (Leftover from a previous + draft.) + 2003-05-26 Alexandre Duret-Lutz * src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh: New files. diff --git a/src/tgba/state.hh b/src/tgba/state.hh index 1de81eb95..3d5d2ba44 100644 --- a/src/tgba/state.hh +++ b/src/tgba/state.hh @@ -1,6 +1,8 @@ #ifndef SPOT_TGBA_STATE_HH # define SPOT_TGBA_STATE_HH +#include + namespace spot { class state @@ -16,6 +18,8 @@ namespace spot // different automata. virtual int compare(const state& other) const = 0; + virtual bdd as_bdd() const = 0; + virtual ~state() { } diff --git a/src/tgba/statebdd.cc b/src/tgba/statebdd.cc index eea428255..4a6688eda 100644 --- a/src/tgba/statebdd.cc +++ b/src/tgba/statebdd.cc @@ -13,4 +13,11 @@ namespace spot assert(o); return o->as_bdd().id() - state_.id(); } + + bdd + state_bdd::as_bdd() const + { + return state_; + } + } diff --git a/src/tgba/statebdd.hh b/src/tgba/statebdd.hh index e5e0ab431..c721497f6 100644 --- a/src/tgba/statebdd.hh +++ b/src/tgba/statebdd.hh @@ -14,12 +14,7 @@ namespace spot { } - bdd - as_bdd() const - { - return state_; - } - + virtual bdd as_bdd() const; virtual int compare(const state& other) const; protected: diff --git a/src/tgba/succiter.hh b/src/tgba/succiter.hh index 71a242b4b..0ff7e7e77 100644 --- a/src/tgba/succiter.hh +++ b/src/tgba/succiter.hh @@ -1,7 +1,7 @@ #ifndef SPOT_TGBA_SUCCITER_H # define SPOT_TGBA_SUCCITER_H -#include "statebdd.hh" +#include "state.hh" namespace spot { @@ -9,18 +9,18 @@ namespace spot class tgba_succ_iterator { public: - virtual - ~tgba_succ_iterator() + virtual + ~tgba_succ_iterator() { } - + // iteration virtual void first() = 0; virtual void next() = 0; virtual bool done() = 0; - + // inspection - virtual state_bdd current_state() = 0; + virtual state* current_state() = 0; virtual bdd current_condition() = 0; virtual bdd current_promise() = 0; }; diff --git a/src/tgba/succiterconcrete.cc b/src/tgba/succiterconcrete.cc index 6a882848f..7a57b0751 100644 --- a/src/tgba/succiterconcrete.cc +++ b/src/tgba/succiterconcrete.cc @@ -8,11 +8,11 @@ namespace spot current_(bddfalse) { } - + tgba_succ_iterator_concrete::~tgba_succ_iterator_concrete() { } - + void tgba_succ_iterator_concrete::first() { @@ -20,12 +20,12 @@ namespace spot if (!done()) next(); } - + void tgba_succ_iterator_concrete::next() { assert(!done()); - + // FIXME: Iterating on the successors this way (calling bdd_satone // and NANDing out the result from the set) requires several descent // of the BDD. Maybe it would be faster to compute all satisfying @@ -33,27 +33,27 @@ namespace spot next_succ_set_ &= !current_; current_ = bdd_satone(next_succ_set_); } - + bool tgba_succ_iterator_concrete::done() { return next_succ_set_ == bddfalse; } - - state_bdd + + state_bdd* tgba_succ_iterator_concrete::current_state() { assert(!done()); - return bdd_exist(current_, data_.notnow_set); + return new state_bdd(bdd_exist(current_, data_.notnow_set)); } - + bdd tgba_succ_iterator_concrete::current_condition() { assert(!done()); return bdd_exist(current_, data_.notvar_set); } - + bdd tgba_succ_iterator_concrete::current_promise() { diff --git a/src/tgba/succiterconcrete.hh b/src/tgba/succiterconcrete.hh index 8620575e6..339ac5625 100644 --- a/src/tgba/succiterconcrete.hh +++ b/src/tgba/succiterconcrete.hh @@ -1,6 +1,7 @@ #ifndef SPOT_TGBA_SUCCITERCONCRETE_HH # define SPOT_TGBA_SUCCITERCONCRETE_HH +#include "statebdd.hh" #include "succiter.hh" #include "tgbabddcoredata.hh" @@ -11,17 +12,17 @@ namespace spot public: tgba_succ_iterator_concrete(const tgba_bdd_core_data& d, bdd successors); virtual ~tgba_succ_iterator_concrete(); - + // iteration void first(); void next(); bool done(); - + // inspection - state_bdd current_state(); + state_bdd* current_state(); bdd current_condition(); bdd current_promise(); - + private: const tgba_bdd_core_data& data_; bdd succ_set_; // The set of successors. diff --git a/src/tgba/succlist.hh b/src/tgba/succlist.hh deleted file mode 100644 index b3ae8a2b2..000000000 --- a/src/tgba/succlist.hh +++ /dev/null @@ -1,15 +0,0 @@ -#ifndef SPOT_WAUTO_SUCCLIST_HH -# define SPOT_WAUTO_SUCCLIST_HH - -namespace spot -{ - - struct successor_list - { - virtual - - }; - -} - -#endif SPOT_WAUTO_SUCCLIST_HH diff --git a/src/tgba/tgba.hh b/src/tgba/tgba.hh index 43b214b7f..206912548 100644 --- a/src/tgba/tgba.hh +++ b/src/tgba/tgba.hh @@ -1,12 +1,34 @@ #ifndef SPOT_TGBA_TGBA_HH # define SPOT_TGBA_TGBA_HH -#include "statebdd.hh" +#include "state.hh" #include "succiter.hh" #include "tgbabdddict.hh" namespace spot { + /// \brief A Transition-based Generalized Büchi Automaton. + /// + /// The acronym TGBA (Transition-based Generalized Büchi Automaton) + /// was coined by Dimitra Giannakopoulou and Flavio Lerda + /// in "From States to Transitions: Improving Translation of LTL + /// Formulae to Büchi Automata". (FORTE'02) + /// + /// TGBAs are transition-based, meanings their labels are put + /// on arcs, not on nodes. They use Generalized Büchi acceptance + /// conditions: there are several accepting sets (of + /// transitions), and a path can be accepted only if it traverse + /// at least one transition of each set infinitely often. + /// + /// 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 allows to explore 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 tgba { public: @@ -15,9 +37,33 @@ namespace spot { } - virtual state_bdd get_init_state() const = 0; - virtual tgba_succ_iterator* succ_iter(state_bdd state) const = 0; + /// \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 state* get_init_state() const = 0; + /// \brief Get an iterator over the successors of \a 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 state is 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 tgba_succ_iterator* succ_iter(const state* 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 const tgba_bdd_dict& get_dict() const = 0; }; diff --git a/src/tgba/tgbabddconcrete.cc b/src/tgba/tgbabddconcrete.cc index 39c5b4f20..a65b72d20 100644 --- a/src/tgba/tgbabddconcrete.cc +++ b/src/tgba/tgbabddconcrete.cc @@ -22,16 +22,24 @@ namespace spot init_ = s; } - state_bdd + state_bdd* tgba_bdd_concrete::get_init_state() const + { + return new state_bdd(init_); + } + + bdd + tgba_bdd_concrete::get_init_bdd() const { return init_; } tgba_succ_iterator_concrete* - tgba_bdd_concrete::succ_iter(state_bdd state) const + tgba_bdd_concrete::succ_iter(const state* state) const { - bdd succ_set = bdd_replace(bdd_exist(data_.relation & state.as_bdd(), + const state_bdd* s = dynamic_cast(state); + assert(s); + bdd succ_set = bdd_replace(bdd_exist(data_.relation & s->as_bdd(), data_.now_set), data_.next_to_now); return new tgba_succ_iterator_concrete(data_, succ_set); diff --git a/src/tgba/tgbabddconcrete.hh b/src/tgba/tgbabddconcrete.hh index 62e9901c7..97d5e6a07 100644 --- a/src/tgba/tgbabddconcrete.hh +++ b/src/tgba/tgbabddconcrete.hh @@ -16,9 +16,10 @@ namespace spot ~tgba_bdd_concrete(); void set_init_state(bdd s); - state_bdd get_init_state() const; + state_bdd* get_init_state() const; + bdd get_init_bdd() const; - tgba_succ_iterator_concrete* succ_iter(state_bdd state) const; + tgba_succ_iterator_concrete* succ_iter(const state* state) const; const tgba_bdd_dict& get_dict() const; const tgba_bdd_core_data& get_core_data() const; diff --git a/src/tgba/tgbabddtranslatefactory.cc b/src/tgba/tgbabddtranslatefactory.cc index 7f7b3b0fe..39a407885 100644 --- a/src/tgba/tgbabddtranslatefactory.cc +++ b/src/tgba/tgbabddtranslatefactory.cc @@ -18,7 +18,7 @@ namespace spot data_.notvar_set = bdd_replace(in.notvar_set, rewrite); data_.notprom_set = bdd_replace(in.notprom_set, rewrite); - init_ = bdd_replace(from.get_init_state().as_bdd(), rewrite); + init_ = bdd_replace(from.get_init_bdd(), rewrite); bdd_freepair(rewrite); } diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc index 79f9d42ba..c61b3d528 100644 --- a/src/tgbaalgos/dotty.cc +++ b/src/tgbaalgos/dotty.cc @@ -1,58 +1,60 @@ #include +#include "tgba/tgba.hh" #include "dotty.hh" #include "tgba/bddprint.hh" namespace spot { typedef std::map seen_map; - + static bool dotty_state(std::ostream& os, - const tgba& g, state_bdd state, seen_map& m, int& node) + const tgba& g, state* st, seen_map& m, int& node) { - bdd s = state.as_bdd(); + bdd s = st->as_bdd(); seen_map::iterator i = m.find(s.id()); - + // Already drawn? if (i != m.end()) { node = i->second; return false; } - + node = m.size() + 1; m[s.id()] = node; - + std::cout << " " << node << " [label=\""; bdd_print_set(os, g.get_dict(), s) << "\"]" << std::endl; return true; } - + static void dotty_rec(std::ostream& os, - const tgba& g, state_bdd state, seen_map& m, int father) + const tgba& g, state* st, seen_map& m, int father) { - tgba_succ_iterator* si = g.succ_iter(state); + tgba_succ_iterator* si = g.succ_iter(st); for (si->first(); !si->done(); si->next()) { int node; - state_bdd s = si->current_state(); + state* s = si->current_state(); bool recurse = dotty_state(os, g, s, m, node); os << " " << father << " -> " << node << " [label=\""; bdd_print_set(os, g.get_dict(), si->current_condition()) << "\\n"; - bdd_print_set(os, g.get_dict(), si->current_promise()) << "\"]" + bdd_print_set(os, g.get_dict(), si->current_promise()) << "\"]" << std::endl; if (recurse) dotty_rec(os, g, s, m, node); + delete s; } delete si; } - - std::ostream& + + std::ostream& dotty_reachable(std::ostream& os, const tgba& g) { seen_map m; - state_bdd state = g.get_init_state(); + state* state = g.get_init_state(); os << "digraph G {" << std::endl; os << " size=\"7.26,10.69\"" << std::endl; os << " 0 [label=\"\", style=invis]" << std::endl; @@ -61,6 +63,7 @@ namespace spot os << " 0 -> " << init << std::endl; dotty_rec(os, g, state, m, init); os << "}" << std::endl; + delete state; return os; }