diff --git a/src/tgba/state.hh b/src/tgba/state.hh index deaeb19da..309f27576 100644 --- a/src/tgba/state.hh +++ b/src/tgba/state.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011, 2013 Laboratoire de Recherche et +// Copyright (C) 2009, 2011, 2013, 2014 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -176,6 +176,64 @@ namespace spot state_ptr_hash, state_ptr_equal> state_set; + /// \ingroup tgba_essentials + /// \brief Render state pointers unique via a hash table. + class SPOT_API state_unicity_table + { + state_set m; + public: + + /// \brief Canonicalize state pointer. + /// + /// If this is the first time a state is seen, this return the + /// state pointer as-is, otherwise it frees the state and returns + /// a point to the previously seen copy. + /// + /// States are owned by the table and will be freed on + /// destruction. + const state* operator()(const state* s) + { + auto p = m.insert(s); + if (!p.second) + s->destroy(); + return *p.first; + } + + /// \brief Canonicalize state pointer. + /// + /// Same as operator(), except that a nullptr + /// is returned if the state is not new. + const state* is_new(const state* s) + { + auto p = m.insert(s); + if (!p.second) + { + s->destroy(); + return nullptr; + } + return *p.first; + } + + ~state_unicity_table() + { + for (state_set::iterator i = m.begin(); i != m.end();) + { + // Advance the iterator before destroying its key. This + // avoid issues with old g++ implementations. + state_set::iterator old = i++; + (*old)->destroy(); + } + } + + size_t + size() + { + return m.size(); + } + }; + + + // Functions related to shared_ptr. ////////////////////////////////////////////////// diff --git a/src/tgbaalgos/cutscc.cc b/src/tgbaalgos/cutscc.cc index 8565db4e3..28bc5aecc 100644 --- a/src/tgbaalgos/cutscc.cc +++ b/src/tgbaalgos/cutscc.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011, 2012, 2013 Laboratoire de Recherche et -// Developpement de l'Epita (LRDE). +// Copyright (C) 2009, 2011, 2012, 2013, 2014 Laboratoire de Recherche +// et Developpement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -33,12 +33,10 @@ namespace spot const std::set& s) { tgba_explicit_string* sub_a = new tgba_explicit_string(a->get_dict()); - state* cur = a->get_init_state(); - std::queue tovisit; - typedef std::unordered_set hash_type; + const state* cur = a->get_init_state(); + std::queue tovisit; // Setup - hash_type seen; + state_unicity_table seen; unsigned scc_number; std::string cur_format = a->format_state(cur); std::set::iterator it; @@ -46,8 +44,7 @@ namespace spot for (it = s.begin(); it != s.end() && !m.accepting(*it); ++it) continue; assert(it != s.end()); - tovisit.push(cur); - seen.insert(cur); + tovisit.push(seen(cur)); sub_a->add_state(cur_format); sub_a->copy_acceptance_conditions_of(a); // If the initial is not part of one of the desired SCC, exit @@ -68,15 +65,8 @@ namespace spot // Is the successor included in one of the desired SCC ? if (s.find(scc_number) != s.end()) { - if (seen.find(dst) == seen.end()) - { - tovisit.push(dst); - seen.insert(dst); // has_state? - } - else - { - dst->destroy(); - } + if (seen.is_new(dst)) + tovisit.push(dst); state_explicit_string::transition* t = sub_a->create_transition(cur_format, dst_format); sub_a->add_conditions(t, sit->current_condition()); @@ -90,11 +80,6 @@ namespace spot } delete sit; } - - hash_type::iterator it2; - // Free visited states. - for (it2 = seen.begin(); it2 != seen.end(); ++it2) - (*it2)->destroy(); return sub_a; } diff --git a/src/tgbaalgos/cycles.cc b/src/tgbaalgos/cycles.cc index 4b52b743f..e67a66b26 100644 --- a/src/tgbaalgos/cycles.cc +++ b/src/tgbaalgos/cycles.cc @@ -1,4 +1,5 @@ -// Copyright (C) 2012 Laboratoire de Recherche et Developpement de +// -*- coding: utf-8 -*- +// Copyright (C) 2012, 2014 Laboratoire de Recherche et Developpement de // l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -47,14 +48,12 @@ namespace spot q.pop_back(); y->second.mark = false; - for (set_type::iterator i = y->second.b.begin(); - i != y->second.b.end(); ++i) + for (auto s: y->second.b) { - tagged_state x = tags_.find(*i); + tagged_state x = tags_.find(s); assert(x != tags_.end()); // insert y in A(x) x->second.del.erase(y->first); - // unmark x recursively if marked if (x->second.mark) q.push_back(x); diff --git a/src/tgbaalgos/cycles.hh b/src/tgbaalgos/cycles.hh index 64a2fec1d..63ffc7ddd 100644 --- a/src/tgbaalgos/cycles.hh +++ b/src/tgbaalgos/cycles.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -79,9 +79,6 @@ namespace spot class SPOT_API enumerate_cycles { protected: - typedef std::unordered_set set_type; - // Extra information required for the algorithm for each state. struct state_info { @@ -98,10 +95,10 @@ namespace spot // that a contributed to a contributed to a cycle. bool mark; // Deleted successors (in the paper, states deleted from A(x)) - set_type del; + state_set del; // Predecessors of the current states, that could not yet // contribute to a cycle. - set_type b; + state_set b; }; // Store the state_info for all visited states. diff --git a/src/tgbaalgos/degen.cc b/src/tgbaalgos/degen.cc index 47bab85f3..c649b52e5 100644 --- a/src/tgbaalgos/degen.cc +++ b/src/tgbaalgos/degen.cc @@ -67,37 +67,6 @@ namespace spot // Queue of state to be processed. typedef std::deque queue_t; - // Memory management for the input states. - class unicity_table - { - state_set m; - public: - const state* operator()(const state* s) - { - auto p = m.insert(s); - if (!p.second) - s->destroy(); - return *p.first; - } - - ~unicity_table() - { - for (state_set::iterator i = m.begin(); i != m.end();) - { - // Advance the iterator before destroying its key. This - // avoid issues with old g++ implementations. - state_set::iterator old = i++; - (*old)->destroy(); - } - } - - size_t - size() - { - return m.size(); - } - }; - // Acceptance set common to all outgoing transitions (of the same // SCC -- we do not care about the other) of some state. class outgoing_acc @@ -165,10 +134,10 @@ namespace spot typedef std::unordered_map cache_t; cache_t cache_; - unicity_table& uniq_; + state_unicity_table& uniq_; public: - has_acc_loop(const tgba* a, unicity_table& uniq): + has_acc_loop(const tgba* a, state_unicity_table& uniq): a_(a), uniq_(uniq) { @@ -329,7 +298,7 @@ namespace spot // Make sure we always use the same pointer for identical states // from the input automaton. - unicity_table uniq; + state_unicity_table uniq; // Accepting loop checker, for some heuristics. has_acc_loop acc_loop(a, uniq); diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc index 4e28e1fd3..a5248f161 100644 --- a/src/tgbaalgos/minimize.cc +++ b/src/tgbaalgos/minimize.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -52,6 +52,8 @@ namespace spot { + // FIXME: do we really want to use unordered_set instead of set here? + // This calls for benchmarking. typedef std::unordered_set hash_set; typedef std::unordered_mapdestroy(); - } + seen(dest); } 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 - { - s->destroy(); - s = *i; - } - // Ignore states outside SCC #n. + s = seen(s); if (sm.scc_of_state(s) != scc_n) return 0; return s; @@ -229,7 +208,7 @@ namespace spot scc_map& sm; power_map& pm; const state* dest; - hash_set seen; + state_unicity_table seen; }; diff --git a/src/tgbaalgos/powerset.cc b/src/tgbaalgos/powerset.cc index 9f0a6b625..1dedc06a1 100644 --- a/src/tgbaalgos/powerset.cc +++ b/src/tgbaalgos/powerset.cc @@ -1,7 +1,8 @@ -// Copyright (C) 2009, 2010, 2011, 2013 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2010, 2011, 2013, 2014 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 +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -54,8 +55,7 @@ namespace spot { power_state ps; - state* s = aut->get_init_state(); - pm.states.insert(s); + const state* s = pm.canonicalize(aut->get_init_state()); ps.insert(s); todo.push_back(ps); seen[ps] = 1; @@ -325,7 +325,7 @@ namespace spot tgba_explicit_number* det = tgba_powerset(aut, pm, false); if ((threshold_states > 0) - && (pm.map_.size() > pm.states.size() * threshold_states)) + && (pm.map_.size() > pm.states_.size() * threshold_states)) { delete det; return 0; diff --git a/src/tgbaalgos/powerset.hh b/src/tgbaalgos/powerset.hh index a0b6831ca..a8dd4a33b 100644 --- a/src/tgbaalgos/powerset.hh +++ b/src/tgbaalgos/powerset.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013 Laboratoire de Recherche et Développement -// de l'Epita. +// Copyright (C) 2011, 2013, 2014 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. @@ -34,21 +34,6 @@ namespace spot { typedef std::set power_state; typedef std::map power_map_data; - typedef std::unordered_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; - s->destroy(); - } - } const power_state& states_of(int s) const @@ -59,21 +44,11 @@ namespace spot const state* canonicalize(const state* s) { - state_set::const_iterator i = states.find(s); - if (i != states.end()) - { - s->destroy(); - s = *i; - } - else - { - states.insert(s); - } - return s; + return states_(s); } power_map_data map_; - state_set states; + state_unicity_table states_; }; diff --git a/src/tgbaalgos/safety.cc b/src/tgbaalgos/safety.cc index e7f390cf9..7d61cc531 100644 --- a/src/tgbaalgos/safety.cc +++ b/src/tgbaalgos/safety.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2013 Laboratoire de Recherche et +// Copyright (C) 2010, 2011, 2013, 2014 Laboratoire de Recherche et // Développement de l'Epita (LRDE) // // This file is part of Spot, a model checking library. @@ -72,16 +72,10 @@ namespace spot bool is_safety_mwdba(const tgba* aut) { - typedef std::unordered_set seen_map; - seen_map seen; // States already seen. + state_unicity_table seen; // States already seen. std::deque todo; // A queue of states yet to explore. - { - state* s = aut->get_init_state(); - todo.push_back(s); - seen.insert(s); - } + todo.push_back(seen(aut->get_init_state())); bdd all_acc = aut->all_acceptance_conditions(); @@ -100,28 +94,11 @@ namespace spot all_accepting = false; break; } - state* d = it->current_state(); - if (seen.find(d) != seen.end()) - { - d->destroy(); - } - else - { - seen.insert(d); - todo.push_back(d); - } + if (const state* d = seen.is_new(it->current_state())) + todo.push_back(d); } delete it; } - - seen_map::const_iterator it = seen.begin(); - while (it != seen.end()) - { - seen_map::const_iterator old = it; - ++it; - (*old)->destroy(); - } - return all_accepting; }