Commit 9b95b697 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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.
parent 6230f320
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de // Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire
// Recherche et Développement de l'Epita (LRDE). // de Recherche et Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
...@@ -74,9 +74,7 @@ namespace spot ...@@ -74,9 +74,7 @@ namespace spot
trace trace
<< "PASS 1" << std::endl; << "PASS 1" << std::endl;
std::unordered_map<const state*, state_map<std::set<const state*, state_ptr_less_than>> liveset;
std::set<const state*, state_ptr_less_than>,
state_ptr_hash, state_ptr_equal> liveset;
std::stack<spot::state*> livelock_roots; std::stack<spot::state*> livelock_roots;
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2008, 2012, 2013, 2014 Laboratoire de Recherche et // Copyright (C) 2008, 2012, 2013, 2014, 2016 Laboratoire de Recherche
// Dévelopment de l'Epita (LRDE). // et Dévelopment de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie. // Université Pierre et Marie Curie.
...@@ -86,8 +86,7 @@ namespace spot ...@@ -86,8 +86,7 @@ namespace spot
/// See the paper cited above. /// See the paper cited above.
class SPOT_API ta_check : public ec_statistics class SPOT_API ta_check : public ec_statistics
{ {
typedef std::unordered_map<const state*, int, typedef state_map<int> hash_type;
state_ptr_hash, state_ptr_equal> hash_type;
public: public:
ta_check(const const_ta_product_ptr& a, option_map o = option_map()); ta_check(const const_ta_product_ptr& a, option_map o = option_map());
virtual virtual
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de // Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire
// Recherche et Développement de l'Epita (LRDE). // de Recherche et Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
...@@ -39,10 +39,8 @@ ...@@ -39,10 +39,8 @@
namespace spot namespace spot
{ {
typedef std::unordered_set<const state*, typedef state_set hash_set;
state_ptr_hash, state_ptr_equal> hash_set; typedef state_map<unsigned> hash_map;
typedef std::unordered_map<const state*, unsigned,
state_ptr_hash, state_ptr_equal> hash_map;
typedef std::list<hash_set*> partition_t; typedef std::list<hash_set*> partition_t;
namespace namespace
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2010, 2012, 2014, 2015 Laboratoire de Recherche et // Copyright (C) 2010, 2012, 2014, 2015, 2016 Laboratoire de Recherche
// Développement de l'Epita (LRDE). // et Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
...@@ -34,7 +34,7 @@ namespace spot ...@@ -34,7 +34,7 @@ namespace spot
} }
ta_reachable_iterator::~ta_reachable_iterator() ta_reachable_iterator::~ta_reachable_iterator()
{ {
seen_map::const_iterator s = seen.begin(); auto s = seen.begin();
while (s != seen.end()) while (s != seen.end())
{ {
// Advance the iterator before deleting the "key" pointer. // Advance the iterator before deleting the "key" pointer.
...@@ -81,7 +81,7 @@ namespace spot ...@@ -81,7 +81,7 @@ namespace spot
for (si->first(); !si->done(); si->next()) for (si->first(); !si->done(); si->next())
{ {
const state* current = si->dst(); const state* current = si->dst();
seen_map::const_iterator s = seen.find(current); auto s = seen.find(current);
bool ws = want_state(current); bool ws = want_state(current);
if (s == seen.end()) if (s == seen.end())
{ {
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche // Copyright (C) 2010, 2011, 2012, 2013, 2014, 2016 Laboratoire de
// et Développement de l'Epita (LRDE). // Recherche et Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
...@@ -88,9 +88,7 @@ namespace spot ...@@ -88,9 +88,7 @@ namespace spot
const_ta_ptr t_automata_; ///< The spot::ta to explore. const_ta_ptr t_automata_; ///< The spot::ta to explore.
typedef std::unordered_map<const state*, int, state_map<int> seen; ///< States already seen.
state_ptr_hash, state_ptr_equal> seen_map;
seen_map seen; ///< States already seen.
}; };
/// \ingroup ta_generic /// \ingroup ta_generic
......
// -*- coding: utf-8 -*- // -*- 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). // Recherche et Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
...@@ -160,9 +160,7 @@ namespace spot ...@@ -160,9 +160,7 @@ namespace spot
// * h: a hash of all visited nodes, with their order, // * h: a hash of all visited nodes, with their order,
// (it is called "Hash" in Couvreur's paper) // (it is called "Hash" in Couvreur's paper)
typedef std::unordered_map<const state*, int, state_map<int> h; ///< Heap of visited states.
state_ptr_hash, state_ptr_equal> hash_type;
hash_type h; ///< Heap of visited states.
// * num: the number of visited nodes. Used to set the order of each // * num: the number of visited nodes. Used to set the order of each
// visited node, // visited node,
......
...@@ -172,9 +172,20 @@ namespace spot ...@@ -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<const state*, typedef std::unordered_set<const state*,
state_ptr_hash, state_ptr_equal> state_set; state_ptr_hash, state_ptr_equal> state_set;
/// \brief Unordered map of abstract states
///
/// Destroying each state if needed is the user's responsibility.
template<class val>
using state_map = std::unordered_map<const state*, val,
state_ptr_hash, state_ptr_equal>;
/// \ingroup twa_essentials /// \ingroup twa_essentials
/// \brief Render state pointers unique via a hash table. /// \brief Render state pointers unique via a hash table.
...@@ -270,7 +281,7 @@ namespace spot ...@@ -270,7 +281,7 @@ namespace spot
/// (shared_ptr<const state*>). /// (shared_ptr<const state*>).
/// ///
/// This is meant to be used as a comparison functor for /// 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 /// For instance here is how one could declare
/// a map of \c shared_state /// a map of \c shared_state
...@@ -280,6 +291,8 @@ namespace spot ...@@ -280,6 +291,8 @@ namespace spot
/// state_shared_ptr_hash, /// state_shared_ptr_hash,
/// state_shared_ptr_equal> seen; /// state_shared_ptr_equal> seen;
/// \endcode /// \endcode
///
/// \see shared_state_set
struct state_shared_ptr_equal struct state_shared_ptr_equal
{ {
bool bool
...@@ -307,6 +320,8 @@ namespace spot ...@@ -307,6 +320,8 @@ namespace spot
/// state_shared_ptr_hash, /// state_shared_ptr_hash,
/// state_shared_ptr_equal> seen; /// state_shared_ptr_equal> seen;
/// \endcode /// \endcode
///
/// \see shared_state_set
struct state_shared_ptr_hash struct state_shared_ptr_hash
{ {
size_t size_t
...@@ -317,6 +332,7 @@ namespace spot ...@@ -317,6 +332,7 @@ namespace spot
} }
}; };
/// Unordered set of shared states
typedef std::unordered_set<shared_state, typedef std::unordered_set<shared_state,
state_shared_ptr_hash, state_shared_ptr_hash,
state_shared_ptr_equal> shared_state_set; state_shared_ptr_equal> shared_state_set;
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire // Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016
// de Recherche et Développement de l'Epita (LRDE). // Laboratoire de Recherche et Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
...@@ -719,8 +719,7 @@ namespace spot ...@@ -719,8 +719,7 @@ namespace spot
////////////////////////////// //////////////////////////////
namespace test namespace test
{ {
typedef std::unordered_map<const state*, int, typedef state_map<int> stnum_t;
state_ptr_hash, state_ptr_equal> stnum_t;
void print_safra_tree(const safra_tree* this_node, void print_safra_tree(const safra_tree* this_node,
stnum_t& node_names, stnum_t& node_names,
......
...@@ -358,11 +358,6 @@ namespace spot ...@@ -358,11 +358,6 @@ namespace spot
std::map<path, int> pathid; std::map<path, int> pathid;
int nvars = 0; int nvars = 0;
//typedef std::unordered_map<const state*, int,
//state_ptr_hash, state_ptr_equal> state_map;
//typedef std::unordered_map<int, const state*> int_map;
//state_map state_to_int;
// int_map int_to_state;
unsigned cand_size; unsigned cand_size;
unsigned int cand_nacc; unsigned int cand_nacc;
acc_cond::acc_code cand_acc; acc_cond::acc_code cand_acc;
......
// -*- coding: utf-8 -*- // -*- 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). // Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2004, 2005 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
...@@ -455,9 +455,7 @@ namespace spot ...@@ -455,9 +455,7 @@ namespace spot
std::string in; std::string in;
acc_cond::mark_t all_acc = 0U; acc_cond::mark_t all_acc = 0U;
bool all_acc_seen = false; bool all_acc_seen = false;
typedef std::unordered_map<const state*, std::set<int>, state_map<std::set<int>> seen;
state_ptr_hash, state_ptr_equal> state_map;
state_map seen;
if (prefix.empty()) if (prefix.empty())
{ {
...@@ -493,7 +491,7 @@ namespace spot ...@@ -493,7 +491,7 @@ namespace spot
{ {
// Keep track of the serial associated to each state so we // Keep track of the serial associated to each state so we
// can note duplicate states and make the replay easier to read. // 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; std::ostringstream msg;
if (o != seen.end()) if (o != seen.end())
{ {
...@@ -648,7 +646,7 @@ namespace spot ...@@ -648,7 +646,7 @@ namespace spot
return false; return false;
} }
state_map::const_iterator o = seen.begin(); auto o = seen.begin();
while (o != seen.end()) while (o != seen.end())
{ {
// Advance the iterator before deleting the "key" pointer. // Advance the iterator before deleting the "key" pointer.
...@@ -674,9 +672,7 @@ namespace spot ...@@ -674,9 +672,7 @@ namespace spot
const twa_run::steps* l; const twa_run::steps* l;
acc_cond::mark_t seen_acc = 0U; acc_cond::mark_t seen_acc = 0U;
typedef std::unordered_map<const state*, unsigned, state_map<unsigned> seen;
state_ptr_hash, state_ptr_equal> state_map;
state_map seen;
if (prefix.empty()) if (prefix.empty())
l = &cycle; l = &cycle;
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2014 Laboratoire de Recherche et Développement de // Copyright (C) 2014, 2016 Laboratoire de Recherche et Développement
// l'Epita (LRDE). // de l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // 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. // et Marie Curie.
...@@ -32,7 +32,7 @@ namespace spot ...@@ -32,7 +32,7 @@ namespace spot
couvreur99_check_status::~couvreur99_check_status() couvreur99_check_status::~couvreur99_check_status()
{ {
hash_type::iterator i = h.begin(); auto i = h.begin();
while (i != h.end()) while (i != h.end())
{ {
// Advance the iterator before deleting the key. // Advance the iterator before deleting the key.
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement // Copyright (C) 2013, 2014, 2016 Laboratoire de Recherche et
// de l'Epita (LRDE). // Développement de l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // 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. // et Marie Curie.
...@@ -43,9 +43,7 @@ namespace spot ...@@ -43,9 +43,7 @@ namespace spot
const_twa_ptr aut; const_twa_ptr aut;
scc_stack root; scc_stack root;
typedef std::unordered_map<const state*, int, state_map<int> h;
state_ptr_hash, state_ptr_equal> hash_type;
hash_type h;
const state* cycle_seed; const state* cycle_seed;
......
// -*- coding: utf-8 -*- // -*- 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). // recherche et développement de l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6
// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
...@@ -55,13 +55,10 @@ namespace spot ...@@ -55,13 +55,10 @@ namespace spot
struct gv04: public emptiness_check, public ec_statistics struct gv04: public emptiness_check, public ec_statistics
{ {
// Map of visited states. // Map of visited states.
typedef std::unordered_map<const state*, size_t, state_map<size_t> h;
state_ptr_hash, state_ptr_equal> hash_type;
hash_type h;
// Stack of visited states on the path. // Stack of visited states on the path.
typedef std::vector<stack_entry> stack_type; std::vector<stack_entry> stack;
stack_type stack;
int top; // Top of SCC stack. int top; // Top of SCC stack.
int dftop; // Top of DFS stack. int dftop; // Top of DFS stack.
...@@ -75,9 +72,9 @@ namespace spot ...@@ -75,9 +72,9 @@ namespace spot
~gv04() ~gv04()
{ {
for (stack_type::iterator i = stack.begin(); i != stack.end(); ++i) for (auto i: stack)
a_->release_iter(i->lasttr); a_->release_iter(i.lasttr);
hash_type::const_iterator s = h.begin(); auto s = h.begin();
while (s != h.end()) while (s != h.end())
{ {
// Advance the iterator before deleting the "key" pointer. // Advance the iterator before deleting the "key" pointer.
...@@ -129,7 +126,7 @@ namespace spot ...@@ -129,7 +126,7 @@ namespace spot
<< a_->format_state(s_prime) << a_->format_state(s_prime)
<< (acc ? " (with accepting link)" : ""); << (acc ? " (with accepting link)" : "");
hash_type::const_iterator i = h.find(s_prime); auto i = h.find(s_prime);
if (i == h.end()) if (i == h.end())
{ {
...@@ -341,7 +338,7 @@ namespace spot ...@@ -341,7 +338,7 @@ namespace spot
filter(const state* s) filter(const state* s)
{ {
// Do not escape the SCC // 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. if (// This state was never visited so far.
j == data.h.end() j == data.h.end()
// Or it was discarded // Or it was discarded
......
// -*- coding: utf-8 -*- // -*- 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). // développement de l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2004, 2005 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
...@@ -458,7 +458,7 @@ namespace spot ...@@ -458,7 +458,7 @@ namespace spot
~explicit_magic_search_heap() ~explicit_magic_search_heap()
{ {
hash_type::const_iterator s = h.begin(); auto s = h.begin();
while (s != h.end()) while (s != h.end())
{ {
// Advance the iterator before deleting the "key" pointer. // Advance the iterator before deleting the "key" pointer.
...@@ -470,7 +470,7 @@ namespace spot ...@@ -470,7 +470,7 @@ namespace spot
color_ref get_color_ref(const state*& s) color_ref get_color_ref(const state*& s)
{ {
hash_type::iterator it = h.find(s); auto it = h.find(s);
if (it == h.end()) if (it == h.end())
return color_ref(nullptr); return color_ref(nullptr);
if (s != it->first) if (s != it->first)
...@@ -493,7 +493,7 @@ namespace spot ...@@ -493,7 +493,7 @@ namespace spot
bool has_been_visited(const state* s) const 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()); return (it != h.end());
} }
...@@ -504,10 +504,7 @@ namespace spot ...@@ -504,10 +504,7 @@ namespace spot
} }
private: private:
state_map<color> h;
typedef std::unordered_map<const state*, color,
state_ptr_hash, state_ptr_equal> hash_type;
hash_type h;
}; };
class bsh_magic_search_heap class bsh_magic_search_heap
......
// -*- coding: utf-8 -*- // -*- 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). // Recherche et Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
...@@ -51,10 +51,8 @@ namespace spot ...@@ -51,10 +51,8 @@ namespace spot
{ {
// FIXME: do we really want to use unordered_set instead of set here? // FIXME: do we really want to use unordered_set instead of set here?
// This calls for benchmarking. // This calls for benchmarking.
typedef std::unordered_set<const state*, typedef state_set hash_set;
state_ptr_hash, state_ptr_equal> hash_set; typedef state_map<unsigned> hash_map;
typedef std::unordered_map<const state*, unsigned,
state_ptr_hash, state_ptr_equal> hash_map;
namespace namespace
{ {
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de // Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016
// Recherche et Développement de l'Epita (LRDE). // Laboratoire de Recherche et Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
...@@ -41,7 +41,7 @@ namespace spot ...@@ -41,7 +41,7 @@ namespace spot
author = {Deian Tabakov and Moshe Y. Vardi}, author = {Deian Tabakov and Moshe Y. Vardi},
title = {Optimized Temporal Monitors for SystemC{$^*$}}, title = {Optimized Temporal Monitors for SystemC{$^*$}},
booktitle = {Proceedings of the 10th International Conferance booktitle = {Proceedings of the 10th International Conferance
on Runtime Verification}, on Runtime Verification},
pages = {436--451}, pages = {436--451},
year = 2010, year = 2010,
volume = {6418}, volume = {6418},
......
// -*- coding: utf-8 -*- // -*- 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). // et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre