From 358d4bfdf2f9b773e63e3a255978ecd46a6ff6ef Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 4 Jan 2011 19:13:44 +0100 Subject: [PATCH] Rewrite the check of WDBA state acceptance in minimize(). * src/tgbaalgos/powerset.hh (power_map): New structure, allowing the caller to retrieve the set of original states corresponding to the set in the deterministic automaton. (power_set): Adjust prototype to take a power_map instead of the acc_list. * src/tgbaalgos/powerset.cc (power_set): Strip all code using acc_list, and update power_set. * src/tgbaalgos/minimize.cc (minimize): Rewrite, using an algorithm similar to the one in the Dax paper to check whether state of the minimized automaton should be accepting. --- ChangeLog | 15 +++- src/tgbaalgos/minimize.cc | 167 ++++++++++++++++++++++++++++++++++++-- src/tgbaalgos/powerset.cc | 72 ++++------------ src/tgbaalgos/powerset.hh | 67 +++++++++++++-- 4 files changed, 250 insertions(+), 71 deletions(-) diff --git a/ChangeLog b/ChangeLog index fb28ed409..3c26242b5 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,6 +1,19 @@ 2011-01-04 Alexandre Duret-Lutz - Add trivial() and one_state_of() functions to scc_map. + Rewrite the check of WDBA state acceptance in minimize(). + + * src/tgbaalgos/powerset.hh (power_map): New structure, allowing + the caller to retrieve the set of original states corresponding to + the set in the deterministic automaton. + (power_set): Adjust prototype to take a power_map instead of the + acc_list. + * src/tgbaalgos/powerset.cc (power_set): Strip all code using + acc_list, and update power_set. + * src/tgbaalgos/minimize.cc (minimize): Rewrite, using an + algorithm similar to the one in the Dax paper to check whether + state of the minimized automaton should be accepting. + +2011-01-04 Alexandre Duret-Lutz * src/tgbaalgos/scc.hh, src/tgbaalgos/scc.cc (scc_map::trivial, scc_map::one_state_of): Two new helper functions. diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc index 3664fadad..737c9df50 100644 --- a/src/tgbaalgos/minimize.cc +++ b/src/tgbaalgos/minimize.cc @@ -19,6 +19,9 @@ // 02111-1307, USA. #include +#include +#include +#include #include "minimize.hh" #include "ltlast/allnodes.hh" #include "misc/hash.hh" @@ -28,7 +31,9 @@ #include "tgbaalgos/gtec/gtec.hh" #include "tgbaalgos/safety.hh" #include "tgbaalgos/sccfilter.hh" +#include "tgbaalgos/scc.hh" #include "tgbaalgos/ltl2tgba_fm.hh" +#include "tgbaalgos/bfssteps.hh" namespace spot { @@ -141,28 +146,174 @@ namespace spot return res; } + + namespace + { + + struct wdba_search_acc_loop : public bfs_steps + { + wdba_search_acc_loop(const tgba* det_a, + unsigned scc_n, scc_map& sm, + power_map& pm, const state* dest) + : bfs_steps(det_a), scc_n(scc_n), sm(sm), pm(pm), dest(dest) + { + seen.insert(dest); + } + + virtual + ~wdba_search_acc_loop() + { + hash_set::const_iterator i = seen.begin(); + while (i != seen.end()) + { + hash_set::const_iterator old = i; + ++i; + delete *old; + } + } + + virtual const state* + filter(const state* s) + { + // Use the state from seen. + hash_set::const_iterator i = seen.find(s); + if (i == seen.end()) + { + seen.insert(s); + } + else + { + delete s; + s = *i; + } + // Ignore states outside SCC #n. + if (sm.scc_of_state(s) != scc_n) + return 0; + return s; + } + + virtual bool + match(tgba_run::step&, const state* to) + { + return to == dest; + } + + unsigned scc_n; + scc_map& sm; + power_map& pm; + const state* dest; + hash_set seen; + }; + + + bool + wdba_scc_is_accepting(const tgba_explicit_number* det_a, unsigned scc_n, + const tgba* orig_a, scc_map& sm, power_map& pm) + { + // Get some state from the SCC #n. + const state* start = sm.one_state_of(scc_n)->clone(); + + // Find a loop around START in SCC #n. + wdba_search_acc_loop wsal(det_a, scc_n, sm, pm, start); + tgba_run::steps loop; + const state* reached = wsal.search(start, loop); + assert(reached == start); + (void)reached; + + // Build an automaton representing this loop. + tgba_explicit_number loop_a(det_a->get_dict()); + tgba_run::steps::const_iterator i; + int loop_size = loop.size(); + int n; + for (n = 1, i = loop.begin(); n < loop_size; ++n, ++i) + { + loop_a.create_transition(n - 1, n)->condition = i->label; + delete i->s; + } + assert(i != loop.end()); + loop_a.create_transition(n - 1, 0)->condition = i->label; + delete i->s; + assert(++i == loop.end()); + + const state* loop_a_init = loop_a.get_init_state(); + assert(loop_a.get_label(loop_a_init) == 0); + + // Check if the loop is accepting in the original automaton. + bool accepting = false; + + // Iterate on each original state corresponding to start. + const power_map::power_state& ps = pm.states_of(det_a->get_label(start)); + for (power_map::power_state::const_iterator it = ps.begin(); + it != ps.end() && !accepting; ++it) + { + // Contrustruct a product between + // LOOP_A, and ORIG_A starting in *IT. + + tgba* p = new tgba_product_init(&loop_a, orig_a, + loop_a_init, *it); + + emptiness_check* ec = couvreur99(p); + emptiness_check_result* res = ec->check(); + + if (res) + accepting = true; + delete res; + delete ec; + delete p; + } + + delete loop_a_init; + return accepting; + } + + } + + + tgba_explicit* minimize(const tgba* a, bool monitor) { - // The list of accepting states of a. - std::list acc_list; std::queue todo; // The list of equivalent states. std::list done; - tgba_explicit* det_a = tgba_powerset(a, monitor ? 0 : &acc_list); hash_set* final = new hash_set; hash_set* non_final = new hash_set; hash_map state_set_map; - bdd_dict* dict = det_a->get_dict(); - std::list::iterator li; - for (li = acc_list.begin(); li != acc_list.end(); ++li) - final->insert(*li); + + tgba_explicit_number* det_a; + + { + power_map pm; + det_a = tgba_powerset(a, pm); + if (!monitor) + { + // For each SCC of the deterministic automaton, determine if + // it is accepting or not. + scc_map sm(det_a); + sm.build_map(); + unsigned scc_count = sm.scc_count(); + for (unsigned n = 0; n < scc_count; ++n) + { + // Trivial SCCs are not accepting. + if (sm.trivial(n)) + continue; + if (wdba_scc_is_accepting(det_a, n, a, sm, pm)) + { + std::list l = sm.states_of(n); + std::list::const_iterator il; + for (il = l.begin(); il != l.end(); ++il) + final->insert((*il)->clone()); + } + } + } + } init_sets(det_a, *final, *non_final); // Size of det_a unsigned size = final->size() + non_final->size(); // Use bdd variables to number sets. set_num is the first variable // available. - unsigned set_num = dict->register_anonymous_variables(size, det_a); + unsigned set_num = + det_a->get_dict()->register_anonymous_variables(size, det_a); std::set free_var; for (unsigned i = set_num; i < set_num + size; ++i) diff --git a/src/tgbaalgos/powerset.cc b/src/tgbaalgos/powerset.cc index 3dff3f6f4..84124bb28 100644 --- a/src/tgbaalgos/powerset.cc +++ b/src/tgbaalgos/powerset.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -22,46 +22,33 @@ // 02111-1307, USA. #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, - std::list* acc_list) + tgba_explicit_number* + tgba_powerset(const tgba* aut, power_map& pm) { - typedef Sgi::hash_set state_set; - typedef std::set power_state; - typedef std::map power_set; - typedef std::deque todo_list; + typedef power_map::power_state power_state; + typedef std::map power_set; + typedef std::deque todo_list; power_set seen; todo_list todo; - scc_map m(aut); tgba_explicit_number* res = new tgba_explicit_number(aut->get_dict()); - state_set states; - { power_state ps; state* s = aut->get_init_state(); - states.insert(s); + pm.states.insert(s); ps.insert(s); todo.push_back(ps); seen[ps] = 1; - if (acc_list) - { - m.build_map(); - if (m.accepting(m.scc_of_state(s))) - acc_list->push_front(new state_explicit(res->add_state(1))); - } + pm.map_[1] = ps; } unsigned state_num = 1; @@ -86,30 +73,13 @@ 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); for (si->first(); !si->done(); si->next()) if ((cond >> si->current_condition()) == bddtrue) { - const state* s = si->current_state(); - state_set::const_iterator i = states.find(s); - if (i != states.end()) - { - delete s; - s = *i; - } - else - { - states.insert(s); - } - if (acc_list) - { - unsigned scc_num = m.scc_of_state(s); - if (m.accepting(scc_num)) - accepting = true; - } + const state* s = pm.canonicalize(si->current_state()); dest.insert(s); } delete si; @@ -129,29 +99,21 @@ namespace spot { dest_num = ++state_num; seen[dest] = dest_num; + pm.map_[dest_num] = dest; todo.push_back(dest); t = res->create_transition(seen[src], dest_num); - if (accepting) - { - const state* dst = new state_explicit(t->dest); - acc_list->push_front(dst); - } } res->add_conditions(t, cond); } } res->merge_transitions(); - - // Release all states. - state_set::const_iterator i = states.begin(); - while (i != states.end()) - { - // Advance the iterator before deleting the key. - const state* s = *i; - ++i; - delete s; - } - return res; } + + tgba_explicit_number* + tgba_powerset(const tgba* aut) + { + power_map pm; + return tgba_powerset(aut, pm); + } } diff --git a/src/tgbaalgos/powerset.hh b/src/tgbaalgos/powerset.hh index 84af72cf0..96add97d3 100644 --- a/src/tgbaalgos/powerset.hh +++ b/src/tgbaalgos/powerset.hh @@ -1,4 +1,6 @@ -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2011 Laboratoire de Recherche et Développement de +// l'Epita. +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -23,21 +25,72 @@ # define SPOT_TGBAALGOS_POWERSET_HH # include +# include # include "tgba/tgbaexplicit.hh" namespace spot { + + struct power_map + { + typedef std::set power_state; + typedef std::map power_map_data; + typedef Sgi::hash_set state_set; + + ~power_map() + { + // Release all states. + state_set::const_iterator i = states.begin(); + while (i != states.end()) + { + // Advance the iterator before deleting the key. + const state* s = *i; + ++i; + delete s; + } + } + + const power_state& + states_of(int s) const + { + return map_.find(s)->second; + } + + const state* + canonicalize(const state* s) + { + state_set::const_iterator i = states.find(s); + if (i != states.end()) + { + delete s; + s = *i; + } + else + { + states.insert(s); + } + return s; + } + + power_map_data map_; + state_set states; + }; + + /// \brief Build a deterministic automaton, ignoring acceptance conditions. /// \ingroup tgba_misc /// - /// This create a deterministic automaton that recognize the + /// This create a deterministic automaton that recognizes the /// same language as \a aut would if its acceptance conditions /// were ignored. This is the classical powerset algorithm. - /// 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); + /// + /// If \a pm is supplied it will be filled with the set of original states + /// associated to each state of the deterministic automaton. + //@{ + tgba_explicit_number* tgba_powerset(const tgba* aut, power_map& pm); + tgba_explicit_number* tgba_powerset(const tgba* aut); + //@} } #endif // SPOT_TGBAALGOS_POWERSET_HH