From 9b95b697a5a1618795b359139d39a5228037d110 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 28 Jan 2016 13:15:48 +0100 Subject: [PATCH] twa: introduce the state_map template alias * spot/twa/twa.hh: Introduce the type. * spot/taalgos/emptinessta.cc, spot/taalgos/emptinessta.hh, spot/taalgos/minimize.cc, spot/taalgos/reachiter.cc, spot/taalgos/reachiter.hh, spot/taalgos/tgba2ta.cc, spot/twa/twasafracomplement.cc, spot/twaalgos/dtwasat.cc, spot/twaalgos/emptiness.cc, spot/twaalgos/gtec/status.cc, spot/twaalgos/gtec/status.hh, spot/twaalgos/gv04.cc, spot/twaalgos/magic.cc, spot/twaalgos/minimize.cc, spot/twaalgos/minimize.hh, spot/twaalgos/reachiter.cc, spot/twaalgos/reachiter.hh, spot/twaalgos/se05.cc, spot/twaalgos/tau03.cc, spot/twaalgos/tau03opt.cc: Use it. --- spot/taalgos/emptinessta.cc | 8 +++----- spot/taalgos/emptinessta.hh | 7 +++---- spot/taalgos/minimize.cc | 10 ++++------ spot/taalgos/reachiter.cc | 8 ++++---- spot/taalgos/reachiter.hh | 8 +++----- spot/taalgos/tgba2ta.cc | 6 ++---- spot/twa/twa.hh | 18 +++++++++++++++++- spot/twa/twasafracomplement.cc | 7 +++---- spot/twaalgos/dtwasat.cc | 5 ----- spot/twaalgos/emptiness.cc | 14 +++++--------- spot/twaalgos/gtec/status.cc | 6 +++--- spot/twaalgos/gtec/status.hh | 8 +++----- spot/twaalgos/gv04.cc | 19 ++++++++----------- spot/twaalgos/magic.cc | 13 +++++-------- spot/twaalgos/minimize.cc | 8 +++----- spot/twaalgos/minimize.hh | 6 +++--- spot/twaalgos/reachiter.cc | 8 ++++---- spot/twaalgos/reachiter.hh | 12 ++++-------- spot/twaalgos/se05.cc | 10 ++++------ spot/twaalgos/tau03.cc | 17 ++++++----------- spot/twaalgos/tau03opt.cc | 8 ++------ 21 files changed, 89 insertions(+), 117 deletions(-) diff --git a/spot/taalgos/emptinessta.cc b/spot/taalgos/emptinessta.cc index 20afa9675..37fb73944 100644 --- a/spot/taalgos/emptinessta.cc +++ b/spot/taalgos/emptinessta.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de -// Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire +// de Recherche et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -74,9 +74,7 @@ namespace spot trace << "PASS 1" << std::endl; - std::unordered_map, - state_ptr_hash, state_ptr_equal> liveset; + state_map> liveset; std::stack livelock_roots; diff --git a/spot/taalgos/emptinessta.hh b/spot/taalgos/emptinessta.hh index 4298a6015..a6c334567 100644 --- a/spot/taalgos/emptinessta.hh +++ b/spot/taalgos/emptinessta.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2012, 2013, 2014 Laboratoire de Recherche et -// Dévelopment de l'Epita (LRDE). +// Copyright (C) 2008, 2012, 2013, 2014, 2016 Laboratoire de Recherche +// et Dévelopment de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -86,8 +86,7 @@ namespace spot /// See the paper cited above. class SPOT_API ta_check : public ec_statistics { - typedef std::unordered_map hash_type; + typedef state_map hash_type; public: ta_check(const const_ta_product_ptr& a, option_map o = option_map()); virtual diff --git a/spot/taalgos/minimize.cc b/spot/taalgos/minimize.cc index ded2a3d3b..2c086c77b 100644 --- a/spot/taalgos/minimize.cc +++ b/spot/taalgos/minimize.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de -// Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire +// de Recherche et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -39,10 +39,8 @@ namespace spot { - typedef std::unordered_set hash_set; - typedef std::unordered_map hash_map; + typedef state_set hash_set; + typedef state_map hash_map; typedef std::list partition_t; namespace diff --git a/spot/taalgos/reachiter.cc b/spot/taalgos/reachiter.cc index 3efe7de1b..f7833fb4c 100644 --- a/spot/taalgos/reachiter.cc +++ b/spot/taalgos/reachiter.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2012, 2014, 2015 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2010, 2012, 2014, 2015, 2016 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -34,7 +34,7 @@ namespace spot } ta_reachable_iterator::~ta_reachable_iterator() { - seen_map::const_iterator s = seen.begin(); + auto s = seen.begin(); while (s != seen.end()) { // Advance the iterator before deleting the "key" pointer. @@ -81,7 +81,7 @@ namespace spot for (si->first(); !si->done(); si->next()) { const state* current = si->dst(); - seen_map::const_iterator s = seen.find(current); + auto s = seen.find(current); bool ws = want_state(current); if (s == seen.end()) { diff --git a/spot/taalgos/reachiter.hh b/spot/taalgos/reachiter.hh index 242e1fbcf..91cd6a668 100644 --- a/spot/taalgos/reachiter.hh +++ b/spot/taalgos/reachiter.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2016 Laboratoire de +// Recherche et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -88,9 +88,7 @@ namespace spot const_ta_ptr t_automata_; ///< The spot::ta to explore. - typedef std::unordered_map seen_map; - seen_map seen; ///< States already seen. + state_map seen; ///< States already seen. }; /// \ingroup ta_generic diff --git a/spot/taalgos/tgba2ta.cc b/spot/taalgos/tgba2ta.cc index 62d46052b..1d98e93de 100644 --- a/spot/taalgos/tgba2ta.cc +++ b/spot/taalgos/tgba2ta.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de +// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de // Recherche et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -160,9 +160,7 @@ namespace spot // * h: a hash of all visited nodes, with their order, // (it is called "Hash" in Couvreur's paper) - typedef std::unordered_map hash_type; - hash_type h; ///< Heap of visited states. + state_map h; ///< Heap of visited states. // * num: the number of visited nodes. Used to set the order of each // visited node, diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh index 1605d76c6..fa90a1948 100644 --- a/spot/twa/twa.hh +++ b/spot/twa/twa.hh @@ -172,9 +172,20 @@ namespace spot } }; + /// \brief Unordered set of abstract states + /// + /// Destroying each state if needed is the user's responsibility. + /// + /// \see state_unicity_table typedef std::unordered_set state_set; + /// \brief Unordered map of abstract states + /// + /// Destroying each state if needed is the user's responsibility. + template + using state_map = std::unordered_map; /// \ingroup twa_essentials /// \brief Render state pointers unique via a hash table. @@ -270,7 +281,7 @@ namespace spot /// (shared_ptr). /// /// This is meant to be used as a comparison functor for - /// un \c unordered_map whose key are of type \c shared_state. + /// an \c unordered_map whose key are of type \c shared_state. /// /// For instance here is how one could declare /// a map of \c shared_state @@ -280,6 +291,8 @@ namespace spot /// state_shared_ptr_hash, /// state_shared_ptr_equal> seen; /// \endcode + /// + /// \see shared_state_set struct state_shared_ptr_equal { bool @@ -307,6 +320,8 @@ namespace spot /// state_shared_ptr_hash, /// state_shared_ptr_equal> seen; /// \endcode + /// + /// \see shared_state_set struct state_shared_ptr_hash { size_t @@ -317,6 +332,7 @@ namespace spot } }; + /// Unordered set of shared states typedef std::unordered_set shared_state_set; diff --git a/spot/twa/twasafracomplement.cc b/spot/twa/twasafracomplement.cc index 91d2420ce..955f5fa3c 100644 --- a/spot/twa/twasafracomplement.cc +++ b/spot/twa/twasafracomplement.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire -// de Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016 +// Laboratoire de Recherche et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -719,8 +719,7 @@ namespace spot ////////////////////////////// namespace test { - typedef std::unordered_map stnum_t; + typedef state_map stnum_t; void print_safra_tree(const safra_tree* this_node, stnum_t& node_names, diff --git a/spot/twaalgos/dtwasat.cc b/spot/twaalgos/dtwasat.cc index 485007b21..4526f5fdc 100644 --- a/spot/twaalgos/dtwasat.cc +++ b/spot/twaalgos/dtwasat.cc @@ -358,11 +358,6 @@ namespace spot std::map pathid; int nvars = 0; - //typedef std::unordered_map state_map; - //typedef std::unordered_map int_map; - //state_map state_to_int; - // int_map int_to_state; unsigned cand_size; unsigned int cand_nacc; acc_cond::acc_code cand_acc; diff --git a/spot/twaalgos/emptiness.cc b/spot/twaalgos/emptiness.cc index 7fe7fc72a..5b486866f 100644 --- a/spot/twaalgos/emptiness.cc +++ b/spot/twaalgos/emptiness.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011, 2012, 2013, 2014, 2015 Laboratoire de +// Copyright (C) 2009, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de // Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -455,9 +455,7 @@ namespace spot std::string in; acc_cond::mark_t all_acc = 0U; bool all_acc_seen = false; - typedef std::unordered_map, - state_ptr_hash, state_ptr_equal> state_map; - state_map seen; + state_map> seen; if (prefix.empty()) { @@ -493,7 +491,7 @@ namespace spot { // Keep track of the serial associated to each state so we // can note duplicate states and make the replay easier to read. - state_map::iterator o = seen.find(s); + auto o = seen.find(s); std::ostringstream msg; if (o != seen.end()) { @@ -648,7 +646,7 @@ namespace spot return false; } - state_map::const_iterator o = seen.begin(); + auto o = seen.begin(); while (o != seen.end()) { // Advance the iterator before deleting the "key" pointer. @@ -674,9 +672,7 @@ namespace spot const twa_run::steps* l; acc_cond::mark_t seen_acc = 0U; - typedef std::unordered_map state_map; - state_map seen; + state_map seen; if (prefix.empty()) l = &cycle; diff --git a/spot/twaalgos/gtec/status.cc b/spot/twaalgos/gtec/status.cc index 8dc6c3c16..fb6e93ca7 100644 --- a/spot/twaalgos/gtec/status.cc +++ b/spot/twaalgos/gtec/status.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2014, 2016 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 // et Marie Curie. @@ -32,7 +32,7 @@ namespace spot couvreur99_check_status::~couvreur99_check_status() { - hash_type::iterator i = h.begin(); + auto i = h.begin(); while (i != h.end()) { // Advance the iterator before deleting the key. diff --git a/spot/twaalgos/gtec/status.hh b/spot/twaalgos/gtec/status.hh index f6e38b92e..708bf8631 100644 --- a/spot/twaalgos/gtec/status.hh +++ b/spot/twaalgos/gtec/status.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2013, 2014, 2016 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 // et Marie Curie. @@ -43,9 +43,7 @@ namespace spot const_twa_ptr aut; scc_stack root; - typedef std::unordered_map hash_type; - hash_type h; + state_map h; const state* cycle_seed; diff --git a/spot/twaalgos/gv04.cc b/spot/twaalgos/gv04.cc index c4d8f631a..bfe1628e3 100644 --- a/spot/twaalgos/gv04.cc +++ b/spot/twaalgos/gv04.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2010, 2011, 2013, 2014, 2015 Laboratoire de +// Copyright (C) 2008, 2010, 2011, 2013, 2014, 2015, 2016 Laboratoire de // recherche et développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -55,13 +55,10 @@ namespace spot struct gv04: public emptiness_check, public ec_statistics { // Map of visited states. - typedef std::unordered_map hash_type; - hash_type h; + state_map h; // Stack of visited states on the path. - typedef std::vector stack_type; - stack_type stack; + std::vector stack; int top; // Top of SCC stack. int dftop; // Top of DFS stack. @@ -75,9 +72,9 @@ namespace spot ~gv04() { - for (stack_type::iterator i = stack.begin(); i != stack.end(); ++i) - a_->release_iter(i->lasttr); - hash_type::const_iterator s = h.begin(); + for (auto i: stack) + a_->release_iter(i.lasttr); + auto s = h.begin(); while (s != h.end()) { // Advance the iterator before deleting the "key" pointer. @@ -129,7 +126,7 @@ namespace spot << a_->format_state(s_prime) << (acc ? " (with accepting link)" : ""); - hash_type::const_iterator i = h.find(s_prime); + auto i = h.find(s_prime); if (i == h.end()) { @@ -341,7 +338,7 @@ namespace spot filter(const state* s) { // Do not escape the SCC - hash_type::const_iterator j = data.h.find(s); + auto j = data.h.find(s); if (// This state was never visited so far. j == data.h.end() // Or it was discarded diff --git a/spot/twaalgos/magic.cc b/spot/twaalgos/magic.cc index eaec533d2..92fe4f766 100644 --- a/spot/twaalgos/magic.cc +++ b/spot/twaalgos/magic.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013, 2014, 2015 Laboratoire de recherche et +// Copyright (C) 2011, 2013, 2014, 2015, 2016 Laboratoire de recherche et // développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -458,7 +458,7 @@ namespace spot ~explicit_magic_search_heap() { - hash_type::const_iterator s = h.begin(); + auto s = h.begin(); while (s != h.end()) { // Advance the iterator before deleting the "key" pointer. @@ -470,7 +470,7 @@ namespace spot color_ref get_color_ref(const state*& s) { - hash_type::iterator it = h.find(s); + auto it = h.find(s); if (it == h.end()) return color_ref(nullptr); if (s != it->first) @@ -493,7 +493,7 @@ namespace spot bool has_been_visited(const state* s) const { - hash_type::const_iterator it = h.find(s); + auto it = h.find(s); return (it != h.end()); } @@ -504,10 +504,7 @@ namespace spot } private: - - typedef std::unordered_map hash_type; - hash_type h; + state_map h; }; class bsh_magic_search_heap diff --git a/spot/twaalgos/minimize.cc b/spot/twaalgos/minimize.cc index c69e30c5e..7fc6ded58 100644 --- a/spot/twaalgos/minimize.cc +++ b/spot/twaalgos/minimize.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de +// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de // Recherche et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -51,10 +51,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_map hash_map; + typedef state_set hash_set; + typedef state_map hash_map; namespace { diff --git a/spot/twaalgos/minimize.hh b/spot/twaalgos/minimize.hh index 72c94d673..9fc3d61e7 100644 --- a/spot/twaalgos/minimize.hh +++ b/spot/twaalgos/minimize.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de -// Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016 +// Laboratoire de Recherche et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -41,7 +41,7 @@ namespace spot author = {Deian Tabakov and Moshe Y. Vardi}, title = {Optimized Temporal Monitors for SystemC{$^*$}}, booktitle = {Proceedings of the 10th International Conferance - on Runtime Verification}, + on Runtime Verification}, pages = {436--451}, year = 2010, volume = {6418}, diff --git a/spot/twaalgos/reachiter.cc b/spot/twaalgos/reachiter.cc index 0fd5a5a89..b07ffbd1a 100644 --- a/spot/twaalgos/reachiter.cc +++ b/spot/twaalgos/reachiter.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011, 2013, 2014, 2015 Laboratoire de Recherche +// Copyright (C) 2009, 2011, 2013, 2014, 2015, 2016 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é Pierre @@ -35,7 +35,7 @@ namespace spot tgba_reachable_iterator::~tgba_reachable_iterator() { - seen_map::const_iterator s = seen.begin(); + auto s = seen.begin(); while (s != seen.end()) { // Advance the iterator before deleting the "key" pointer. @@ -65,7 +65,7 @@ namespace spot do { const state* current = si->dst(); - seen_map::const_iterator s = seen.find(current); + auto s = seen.find(current); bool ws = want_state(current); if (s == seen.end()) { @@ -154,7 +154,7 @@ namespace spot tgba_reachable_iterator_depth_first::~tgba_reachable_iterator_depth_first() { - seen_map::const_iterator s = seen.begin(); + auto s = seen.begin(); while (s != seen.end()) { // Advance the iterator before deleting the "key" pointer. diff --git a/spot/twaalgos/reachiter.hh b/spot/twaalgos/reachiter.hh index a6d614641..d7f11906e 100644 --- a/spot/twaalgos/reachiter.hh +++ b/spot/twaalgos/reachiter.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2011, 2013 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2008, 2009, 2011, 2013, 2016 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é // Pierre et Marie Curie. @@ -90,9 +90,7 @@ namespace spot protected: const_twa_ptr aut_; ///< The spot::tgba to explore. - typedef std::unordered_map seen_map; - seen_map seen; ///< States already seen. + state_map seen; ///< States already seen. }; /// \ingroup twa_generic @@ -160,9 +158,7 @@ namespace spot protected: const_twa_ptr aut_; ///< The spot::tgba to explore. - typedef std::unordered_map seen_map; - seen_map seen; ///< States already seen. + state_map seen; ///< States already seen. struct stack_item { const state* src; diff --git a/spot/twaalgos/se05.cc b/spot/twaalgos/se05.cc index 26befea04..13df110fd 100644 --- a/spot/twaalgos/se05.cc +++ b/spot/twaalgos/se05.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013, 2014, 2015 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2011, 2013, 2014, 2015, 2016 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -438,10 +438,8 @@ namespace spot class explicit_se05_search_heap { - typedef std::unordered_set hcyan_type; - typedef std::unordered_map hash_type; + typedef state_set hcyan_type; + typedef state_map hash_type; public: enum { Safe = 1 }; diff --git a/spot/twaalgos/tau03.cc b/spot/twaalgos/tau03.cc index 7cb6bee20..874f816b6 100644 --- a/spot/twaalgos/tau03.cc +++ b/spot/twaalgos/tau03.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013, 2014, 2015 Laboratoire de Recherche et -// Developpement de l'Epita (LRDE). +// Copyright (C) 2011, 2013, 2014, 2015, 2016 Laboratoire de Recherche +// et Developpement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -319,7 +319,7 @@ namespace spot ~explicit_tau03_search_heap() { - hash_type::const_iterator s = h.begin(); + auto s = h.begin(); while (s != h.end()) { // Advance the iterator before deleting the "key" pointer. @@ -331,7 +331,7 @@ namespace spot color_ref get_color_ref(const state*& s) { - hash_type::iterator it = h.find(s); + auto it = h.find(s); if (it == h.end()) return color_ref(nullptr, nullptr); if (s != it->first) @@ -356,8 +356,7 @@ namespace spot bool has_been_visited(const state* s) const { - hash_type::const_iterator it = h.find(s); - return (it != h.end()); + return h.find(s) != h.end(); } enum { Has_Size = 1 }; @@ -366,11 +365,7 @@ namespace spot return h.size(); } private: - - typedef std::unordered_map, - state_ptr_hash, state_ptr_equal> hash_type; - hash_type h; + state_map> h; }; } // anonymous diff --git a/spot/twaalgos/tau03opt.cc b/spot/twaalgos/tau03opt.cc index f485dc3d5..ea8e25437 100644 --- a/spot/twaalgos/tau03opt.cc +++ b/spot/twaalgos/tau03opt.cc @@ -397,12 +397,8 @@ namespace spot class explicit_tau03_opt_search_heap { - typedef std::unordered_map, - state_ptr_hash, state_ptr_equal> hcyan_type; - typedef std::unordered_map, - state_ptr_hash, state_ptr_equal> hash_type; + typedef state_map> hcyan_type; + typedef state_map> hash_type; public: class color_ref {