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);