From e24d3be8a7b11136aab67a8405c83b1ca27e9705 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 25 Jul 2003 13:12:01 +0000 Subject: [PATCH] * src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS): Add reachiters.hh. (libtgbaalgos_la_SOURCES): Add reachiters.cc. * src/tgbaalgos/dotty.cc, src/tgbaalgos/save.cc: Rewrite using spot::tgba_reachable_iterator_breadth_first. * src/tgbatest/explicit.test, src/tgbatest/tgbaread.test, src/tgbatest/tripprod.test: Adjust expected output. --- ChangeLog | 11 +++- src/tgbaalgos/Makefile.am | 2 + src/tgbaalgos/dotty.cc | 102 ++++++++++++------------------ src/tgbaalgos/reachiter.cc | 126 +++++++++++++++++++++++++++++++++++++ src/tgbaalgos/reachiter.hh | 94 +++++++++++++++++++++++++++ src/tgbaalgos/save.cc | 87 +++++++++++++------------ src/tgbatest/explicit.test | 6 +- src/tgbatest/tgbaread.test | 6 +- src/tgbatest/tripprod.test | 2 +- 9 files changed, 322 insertions(+), 114 deletions(-) create mode 100644 src/tgbaalgos/reachiter.cc create mode 100644 src/tgbaalgos/reachiter.hh diff --git a/ChangeLog b/ChangeLog index 6ea0b8fd5..54ea26ede 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,9 +1,18 @@ +2003-07-25 Alexandre Duret-Lutz + + * src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS): Add reachiters.hh. + (libtgbaalgos_la_SOURCES): Add reachiters.cc. + * src/tgbaalgos/dotty.cc, src/tgbaalgos/save.cc: Rewrite using + spot::tgba_reachable_iterator_breadth_first. + * src/tgbatest/explicit.test, src/tgbatest/tgbaread.test, + src/tgbatest/tripprod.test: Adjust expected output. + 2003-07-24 Alexandre Duret-Lutz * configure.ac: Output iface/gspn/defs. * iface/gspn/Makefile.am (EXTRA_DIST): Add $(TESTS). (TESTS, check_SCRIPTS, distclean-local): New. - * iface/gspn/dcswave.test, iface/gspn/simple.test, + * iface/gspn/dcswave.test, iface/gspn/simple.test, iface/gspn/defs.in: New files. * iface/gspn/dottygspn.cc (main): Take the list of properties of interest in argument. diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index ec9563bf6..5b68e4a99 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -4,6 +4,7 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS) tgbaalgosdir = $(pkgincludedir)/tgbaalgos tgbaalgos_HEADERS = \ + reachiter.hh \ dotty.hh \ lbtt.hh \ ltl2tgba.hh \ @@ -11,6 +12,7 @@ tgbaalgos_HEADERS = \ noinst_LTLIBRARIES = libtgbaalgos.la libtgbaalgos_la_SOURCES = \ + reachiter.cc \ dotty.cc \ lbtt.cc \ ltl2tgba.cc \ diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc index 46c6c3431..4d44990f9 100644 --- a/src/tgbaalgos/dotty.cc +++ b/src/tgbaalgos/dotty.cc @@ -1,80 +1,60 @@ -#include #include "tgba/tgba.hh" #include "dotty.hh" #include "tgba/bddprint.hh" +#include "reachiter.hh" namespace spot { - typedef std::map seen_map; - /// Output and record a state. - static bool - dotty_state(std::ostream& os, - const tgba* g, state* st, seen_map& m, int& node) + class dotty_bfs : public tgba_reachable_iterator_breadth_first { - seen_map::iterator i = m.find(st); + public: + dotty_bfs(const tgba* a, std::ostream& os) + : tgba_reachable_iterator_breadth_first(a), os_(os) + { + } - // Already drawn? - if (i != m.end()) - { - node = i->second; - return false; - } + void + start() + { + os_ << "digraph G {" << std::endl; + os_ << " size=\"7.26,10.69\"" << std::endl; + os_ << " 0 [label=\"\", style=invis]" << std::endl; + os_ << " 0 -> 1" << std::endl; + } - node = m.size() + 1; - m[st] = node; + void + end() + { + os_ << "}" << std::endl; + } - os << " " << node << " [label=\"" - << g->format_state(st) << "\"]" << std::endl; - return true; - } + void + process_state(const state* s, int n, tgba_succ_iterator*) + { + os_ << " " << n << " [label=\"" + << automata_->format_state(s) << "\"]" << std::endl; + } - /// Process successors. - static void - dotty_rec(std::ostream& os, - const tgba* g, state* st, seen_map& m, int father) - { - tgba_succ_iterator* si = g->succ_iter(st); - for (si->first(); !si->done(); si->next()) - { - int node; - 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_accepting_conditions()) - << "\"]" << std::endl; - if (recurse) - { - dotty_rec(os, g, s, m, node); - // Do not delete S, it is used as key in M. - } - else - { - delete s; - } - } - delete si; - } + void + process_link(int in, int out, const tgba_succ_iterator* si) + { + os_ << " " << in << " -> " << out << " [label=\""; + bdd_print_set(os_, automata_->get_dict(), + si->current_condition()) << "\\n"; + bdd_print_set(os_, automata_->get_dict(), + si->current_accepting_conditions()) << "\"]" << std::endl; + } + + private: + std::ostream& os_; + }; std::ostream& dotty_reachable(std::ostream& os, const tgba* g) { - seen_map m; - 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; - int init; - dotty_state(os, g, state, m, init); - os << " 0 -> " << init << std::endl; - dotty_rec(os, g, state, m, init); - os << "}" << std::endl; - - // Finally delete all states used as keys in m: - for (seen_map::iterator i = m.begin(); i != m.end(); ++i) - delete i->first; - + dotty_bfs d(g, os); + d.run(); return os; } diff --git a/src/tgbaalgos/reachiter.cc b/src/tgbaalgos/reachiter.cc new file mode 100644 index 000000000..3ded00601 --- /dev/null +++ b/src/tgbaalgos/reachiter.cc @@ -0,0 +1,126 @@ +#include "reachiter.hh" + +namespace spot +{ + // tgba_reachable_iterator + ////////////////////////////////////////////////////////////////////// + + tgba_reachable_iterator::tgba_reachable_iterator(const tgba* a) + : automata_(a) + { + } + + tgba_reachable_iterator::~tgba_reachable_iterator() + { + for (seen_map::const_iterator s = seen.begin(); s != seen.end(); ++s) + delete s->first; + } + + void + tgba_reachable_iterator::run() + { + int n = 0; + start(); + state* i = automata_->get_init_state(); + add_state(i); + seen[i] = ++n; + const state* t; + while ((t = next_state())) + { + assert(seen.find(t) != seen.end()); + int tn = seen[t]; + tgba_succ_iterator* si = automata_->succ_iter(t); + process_state(t, tn, si); + for (si->first(); ! si->done(); si->next()) + { + const state* current = si->current_state(); + seen_map::const_iterator s = seen.find(current); + if (s == seen.end()) + { + seen[current] = ++n; + add_state(current); + process_link(tn, n, si); + } + else + { + process_link(tn, seen[current], si); + delete current; + } + } + delete si; + } + end(); + } + + void + tgba_reachable_iterator::start() + { + } + + void + tgba_reachable_iterator::end() + { + } + + void + tgba_reachable_iterator::process_state(const state*, int, + tgba_succ_iterator*) + { + } + + void + tgba_reachable_iterator::process_link(int, int, const tgba_succ_iterator*) + { + } + + // tgba_reachable_iterator_depth_first + ////////////////////////////////////////////////////////////////////// + + tgba_reachable_iterator_depth_first:: + tgba_reachable_iterator_depth_first(const tgba* a) + : tgba_reachable_iterator(a) + { + } + + void + tgba_reachable_iterator_depth_first::add_state(const state* s) + { + todo.push(s); + } + + const state* + tgba_reachable_iterator_depth_first::next_state() + { + if (todo.empty()) + return 0; + const state* s = todo.top(); + todo.pop(); + return s; + } + + // tgba_reachable_iterator_breadth_first + ////////////////////////////////////////////////////////////////////// + + tgba_reachable_iterator_breadth_first:: + tgba_reachable_iterator_breadth_first(const tgba* a) + : tgba_reachable_iterator(a) + { + } + + void + tgba_reachable_iterator_breadth_first::add_state(const state* s) + { + todo.push_back(s); + } + + const state* + tgba_reachable_iterator_breadth_first::next_state() + { + if (todo.empty()) + return 0; + const state* s = todo.front(); + todo.pop_front(); + return s; + } + +} diff --git a/src/tgbaalgos/reachiter.hh b/src/tgbaalgos/reachiter.hh new file mode 100644 index 000000000..d6a0a9fb3 --- /dev/null +++ b/src/tgbaalgos/reachiter.hh @@ -0,0 +1,94 @@ +#ifndef SPOT_TGBAALGOS_REACHITER_HH +# define SPOT_TGBAALGOS_REACHITER_HH + +#include "tgba/tgba.hh" +#include +#include + +namespace spot +{ + /// \brief Iterate over all reachable states of a spot::tgba. + class tgba_reachable_iterator + { + public: + tgba_reachable_iterator(const tgba* a); + virtual ~tgba_reachable_iterator(); + + /// \brief Iterate over all reachable states of a spot::tgba. + /// + /// This is a template method that will call add_state(), next_state(), + /// start(), end(), process_state(), and process_link(), while it + /// iterate over state. + void run(); + + /// \name Todo list management. + /// + /// spot::tgba_reachable_iterator_depth_first and + /// spot::tgba_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 state* s) = 0; + /// \brief Called by run() to obtain the + virtual const state* next_state() = 0; + /// \} + + /// 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 An unique number assigned to \a s. + /// \param si The spot::tgba_succ_iterator for \a s. + virtual void process_state(const state* s, int n, tgba_succ_iterator* si); + /// Called by run() to process a transition. + /// + /// \param in The source state number. + /// \param out The destination state number. + /// \param si The spot::tgba_succ_iterator positionned on the current + /// transition. + virtual void process_link(int in, int out, const tgba_succ_iterator* si); + + protected: + const tgba* automata_; ///< The spot::tgba to explore. + + typedef std::map seen_map; + seen_map seen; ///< States already seen. + }; + + /// \brief An implementation of spot::tgba_reachable_iterator that browses + /// states depth first. + class tgba_reachable_iterator_depth_first : public tgba_reachable_iterator + { + public: + tgba_reachable_iterator_depth_first(const tgba* a); + + virtual void add_state(const state* s); + virtual const state* next_state(); + + protected: + std::stack todo; ///< A stack of state yet to explore. + }; + + /// \brief An implementation of spot::tgba_reachable_iterator that browses + /// states breadth first. + class tgba_reachable_iterator_breadth_first : public tgba_reachable_iterator + { + public: + tgba_reachable_iterator_breadth_first(const tgba* a); + + virtual void add_state(const state* s); + virtual const state* next_state(); + + protected: + std::deque todo; ///< A queue of state yet to explore. + }; + + +} + + +#endif // SPOT_TGBAALGOS_REACHITER_HH diff --git a/src/tgbaalgos/save.cc b/src/tgbaalgos/save.cc index 735983835..afc1a5a55 100644 --- a/src/tgbaalgos/save.cc +++ b/src/tgbaalgos/save.cc @@ -1,63 +1,60 @@ -#include #include "tgba/tgba.hh" #include "save.hh" #include "tgba/bddprint.hh" #include "ltlvisit/tostring.hh" +#include "reachiter.hh" namespace spot { - typedef std::set seen_set; - /// Process successors. - static void - save_rec(std::ostream& os, const tgba* g, state* st, seen_set& m) + class save_bfs : public tgba_reachable_iterator_breadth_first { - m.insert(st); - std::string cur = g->format_state(st); - tgba_succ_iterator* si = g->succ_iter(st); - for (si->first(); !si->done(); si->next()) - { - state* s = si->current_state(); - os << "\"" << cur << "\", \"" << g->format_state(s) << "\", "; + public: + save_bfs(const tgba* a, std::ostream& os) + : tgba_reachable_iterator_breadth_first(a), os_(os) + { + } - bdd_print_sat(os, g->get_dict(), si->current_condition()) << ","; - bdd_print_acc(os, g->get_dict(), si->current_accepting_conditions()) - << ";" << std::endl; + void + start() + { + const bdd_dict* d = automata_->get_dict(); + os_ << "acc ="; + for (bdd_dict::fv_map::const_iterator ai = d->acc_map.begin(); + ai != d->acc_map.end(); ++ai) + { + os_ << " \""; + ltl::to_string(ai->first, os_) << "\""; + } + os_ << ";" << std::endl; + } + + void + process_state(const state* s, int, tgba_succ_iterator* si) + { + const bdd_dict* d = automata_->get_dict(); + std::string cur = automata_->format_state(s); + for (si->first(); !si->done(); si->next()) + { + state* dest = si->current_state(); + os_ << "\"" << cur << "\", \"" + << automata_->format_state(dest) << "\", "; + bdd_print_sat(os_, d, si->current_condition()) << ","; + bdd_print_acc(os_, d, si->current_accepting_conditions()); + os_ << ";" << std::endl; + } + } + + private: + std::ostream& os_; + }; - // Destination already explored? - seen_set::iterator i = m.find(s); - if (i != m.end()) - { - delete s; - } - else - { - save_rec(os, g, s, m); - // Do not delete S, it is used as key in M. - } - } - delete si; - } std::ostream& tgba_save_reachable(std::ostream& os, const tgba* g) { - const bdd_dict* d = g->get_dict(); - os << "acc ="; - for (bdd_dict::fv_map::const_iterator ai = d->acc_map.begin(); - ai != d->acc_map.end(); ++ai) - { - os << " \""; - ltl::to_string(ai->first, os) << "\""; - } - os << ";" << std::endl; - - seen_set m; - state* state = g->get_init_state(); - save_rec(os, g, state, m); - // Finally delete all states used as keys in m: - for (seen_set::iterator i = m.begin(); i != m.end(); ++i) - delete *i; + save_bfs b(g, os); + b.run(); return os; } } diff --git a/src/tgbatest/explicit.test b/src/tgbatest/explicit.test index 24c2a00bd..8689d9d47 100755 --- a/src/tgbatest/explicit.test +++ b/src/tgbatest/explicit.test @@ -10,12 +10,12 @@ cat >expected < 1 - 2 [label="state 1"] + 1 [label="state 0"] 1 -> 2 [label="T\n"] - 3 [label="state 2"] + 2 [label="state 1"] 2 -> 3 [label="\n"] + 3 [label="state 2"] 3 -> 1 [label="\nF"] } EOF diff --git a/src/tgbatest/tgbaread.test b/src/tgbatest/tgbaread.test index 1946ed1c3..62c92c09f 100755 --- a/src/tgbatest/tgbaread.test +++ b/src/tgbatest/tgbaread.test @@ -17,12 +17,12 @@ cat >expected < 1 - 2 [label="s2"] + 1 [label="s1"] 1 -> 2 [label="\n"] - 3 [label="state 3"] + 2 [label="s2"] 2 -> 3 [label="\n"] + 3 [label="state 3"] 3 -> 1 [label="T\nF"] } EOF diff --git a/src/tgbatest/tripprod.test b/src/tgbatest/tripprod.test index 99920d8bf..9aa0f05cf 100755 --- a/src/tgbatest/tripprod.test +++ b/src/tgbatest/tripprod.test @@ -30,9 +30,9 @@ cat >expected <