From e2e138f6e6e569b2f1d13d312b7f94758a503068 Mon Sep 17 00:00:00 2001 From: Felix Abecassis Date: Sat, 20 Mar 2010 14:01:10 +0100 Subject: [PATCH] Modify the powerset algorithm to keep track of accepting states from the initial automaton. * src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh: Added class tgba_explicit_number, a tgba_explicit where states are labelled by integers. * src/tgbaalgos/powerset.hh, src/tgbaalgos/powerset.cc: When building the deterministic automaton, keep track of which states were created from an accepting state in the initial automaton. The states are added to the new optional parameter (if not 0), acc_list. Use tgba_explicit_number instead of tgba_explicit_string to build the result. * src/tgbaalgos/scc.cc (spot): Small fix. Print everything on std::cout. --- ChangeLog | 18 ++++++++++++++++++ src/tgba/tgbaexplicit.cc | 31 +++++++++++++++++++++++++++++++ src/tgba/tgbaexplicit.hh | 12 ++++++++++++ src/tgbaalgos/powerset.cc | 39 +++++++++++++++++++++++++-------------- src/tgbaalgos/powerset.hh | 7 ++++++- src/tgbaalgos/scc.cc | 6 +++--- 6 files changed, 95 insertions(+), 18 deletions(-) diff --git a/ChangeLog b/ChangeLog index 2f292c65b..24c667fd7 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,21 @@ +2010-03-20 Felix Abecassis + + Modify the powerset algorithm to keep track of accepting states + from the initial automaton. + + * src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh: + Added tgba_explicit_number, a tgba_explicit where states are labelled + by integers. + * src/tgbaalgos/powerset.hh, src/tgbaalgos/powerset.cc: + When building the deterministic automaton, keep track of which states + were created from an accepting state in the initial automaton. + The states are added to the new optional parameter (if not 0), + acc_list. + Now use tgba_explicit_number instead of tgba_explicit_string to build + the result. + * src/tgbaalgos/scc.cc (spot): Small fix. + Print everything on std::cout. + 2011-01-05 Alexandre Duret-Lutz Fix computation of support_conditions for bdd-based TGBA. diff --git a/src/tgba/tgbaexplicit.cc b/src/tgba/tgbaexplicit.cc index 2aeaa0991..1cbcc628c 100644 --- a/src/tgba/tgbaexplicit.cc +++ b/src/tgba/tgbaexplicit.cc @@ -21,6 +21,7 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. +#include #include "ltlast/atomic_prop.hh" #include "ltlast/constant.hh" #include "tgbaexplicit.hh" @@ -349,4 +350,34 @@ namespace spot return ltl::to_string(i->second); } + tgba_explicit_number::~tgba_explicit_number() + { + ns_map::iterator i = name_state_map_.begin(); + while (i != name_state_map_.end()) + { + tgba_explicit::state::iterator i2; + for (i2 = i->second->begin(); i2 != i->second->end(); ++i2) + delete *i2; + // Advance the iterator before deleting the formula. + delete i->second; + ++i; + } + } + + tgba_explicit::state* tgba_explicit_number::add_default_init() + { + return add_state(0); + } + + std::string + tgba_explicit_number::format_state(const spot::state* s) const + { + const state_explicit* se = dynamic_cast(s); + assert(se); + sn_map::const_iterator i = state_name_map_.find(se->get_state()); + assert(i != state_name_map_.end()); + std::stringstream ss; + ss << i->second; + return ss.str(); + } } diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh index 7dc7a3267..4e387c71b 100644 --- a/src/tgba/tgbaexplicit.hh +++ b/src/tgba/tgbaexplicit.hh @@ -345,6 +345,18 @@ namespace spot virtual state* add_default_init(); virtual std::string format_state(const spot::state* s) const; }; + + class tgba_explicit_number: + public tgba_explicit_labelled > + { + public: + tgba_explicit_number(bdd_dict* dict): + tgba_explicit_labelled >(dict) + {}; + virtual ~tgba_explicit_number(); + virtual state* add_default_init(); + virtual std::string format_state(const spot::state* s) const; + }; } #endif // SPOT_TGBA_TGBAEXPLICIT_HH diff --git a/src/tgbaalgos/powerset.cc b/src/tgbaalgos/powerset.cc index ab41829e9..4fd0408cb 100644 --- a/src/tgbaalgos/powerset.cc +++ b/src/tgbaalgos/powerset.cc @@ -24,25 +24,28 @@ #include #include #include -#include +#include "powerset.hh" #include "misc/hash.hh" #include "tgbaalgos/powerset.hh" +#include "tgbaalgos/scc.hh" #include "bdd.h" namespace spot { tgba_explicit* - tgba_powerset(const tgba* aut) + tgba_powerset(const tgba* aut, + std::list* acc_list) { typedef Sgi::hash_set state_set; typedef std::set power_state; - typedef std::map power_set; + typedef std::map power_set; typedef std::deque todo_list; power_set seen; todo_list todo; - tgba_explicit_string* res = new tgba_explicit_string(aut->get_dict()); + scc_map m(aut); + tgba_explicit_number* res = new tgba_explicit_number(aut->get_dict()); state_set states; @@ -52,7 +55,8 @@ namespace spot states.insert(s); ps.insert(s); todo.push_back(ps); - seen[ps] = "1"; + seen[ps] = 1; + m.build_map(); } unsigned state_num = 1; @@ -77,6 +81,7 @@ namespace spot // Construct the set of all states reachable via COND. power_state dest; + bool accepting = false; for (i = src.begin(); i != src.end(); ++i) { tgba_succ_iterator *si = aut->succ_iter(*i); @@ -94,30 +99,36 @@ namespace spot { states.insert(s); } + unsigned scc_num = m.scc_of_state(s); + if (m.accepting(scc_num)) + accepting = true; dest.insert(s); } delete si; } if (dest.empty()) continue; - // Add that transition. power_set::const_iterator i = seen.find(dest); - std::string dest_name; + int dest_num; + tgba_explicit::transition* t; if (i != seen.end()) { - dest_name = i->second; + dest_num = i->second; + t = res->create_transition(seen[src], dest_num); } else { - std::ostringstream str; - str << ++state_num; - dest_name = str.str(); - seen[dest] = dest_name; + dest_num = ++state_num; + seen[dest] = dest_num; todo.push_back(dest); + t = res->create_transition(seen[src], dest_num); + if (acc_list && accepting) + { + const state* dst = new state_explicit(t->dest); + acc_list->push_front(dst); + } } - tgba_explicit::transition* t = - res->create_transition(seen[src], dest_name); res->add_conditions(t, cond); } } diff --git a/src/tgbaalgos/powerset.hh b/src/tgbaalgos/powerset.hh index cc329ff9c..84af72cf0 100644 --- a/src/tgbaalgos/powerset.hh +++ b/src/tgbaalgos/powerset.hh @@ -22,6 +22,7 @@ #ifndef SPOT_TGBAALGOS_POWERSET_HH # define SPOT_TGBAALGOS_POWERSET_HH +# include # include "tgba/tgbaexplicit.hh" namespace spot @@ -32,7 +33,11 @@ namespace spot /// This create a deterministic automaton that recognize the /// same language as \a aut would if its acceptance conditions /// were ignored. This is the classical powerset algorithm. - tgba_explicit* tgba_powerset(const tgba* aut); + /// If acc_list is not 0. Whenever a power state is created from one + /// accepting state (a state belonging to an accepting SCC), then this power + /// state is added to acc_list. + tgba_explicit* tgba_powerset(const tgba* aut, + std::list* acc_list = 0); } #endif // SPOT_TGBAALGOS_POWERSET_HH diff --git a/src/tgbaalgos/scc.cc b/src/tgbaalgos/scc.cc index 038d19be8..75bac5261 100644 --- a/src/tgbaalgos/scc.cc +++ b/src/tgbaalgos/scc.cc @@ -505,9 +505,9 @@ namespace spot m.useful_acc_of(state))) << "]"; } - std::cout << " " << state << " [shape=box," - << (m.accepting(state) ? "style=bold," : "") - << "label=\"" << ostr.str() << "\"]" << std::endl; + out << " " << state << " [shape=box," + << (m.accepting(state) ? "style=bold," : "") + << "label=\"" << ostr.str() << "\"]" << std::endl; const scc_map::succ_type& succ = m.succ(state);