diff --git a/spot/ltsmin/spins_kripke.hh b/spot/ltsmin/spins_kripke.hh index 33362d0a0..5cd7cfc03 100644 --- a/spot/ltsmin/spins_kripke.hh +++ b/spot/ltsmin/spins_kripke.hh @@ -79,10 +79,6 @@ namespace spot } }; - /// \brief Shortcut to avoid long names... - typedef brick::hashset::FastConcurrent - cspins_state_map; - /// \brief The management of states (i.e. allocation/deallocation) can /// be painless since every time we have to consider wether the state will /// be compressed or not. This class aims to simplify this management @@ -113,7 +109,6 @@ namespace spot { cspins_state_manager* manager; // The state manager std::vector* succ; // The successors of a state - cspins_state_map map; // Must be a copy and only one copy/thread int* compressed_; int* uncompressed_; bool compress; @@ -215,7 +210,6 @@ namespace spot bool selfloopize_; int dead_idx_; std::vector aps_; - cspins_state_map map_; unsigned int nb_threads_; }; diff --git a/spot/ltsmin/spins_kripke.hxx b/spot/ltsmin/spins_kripke.hxx index 2e579ae18..eb2e370ca 100644 --- a/spot/ltsmin/spins_kripke.hxx +++ b/spot/ltsmin/spins_kripke.hxx @@ -129,10 +129,7 @@ namespace spot cspins_state s = inner->manager->alloc_setup(dst, inner->compressed_, inner->manager->size() * 2); - auto it = inner->map.insert(s); - inner->succ->push_back(*it); - if (!it.isnew()) - inner->manager->dealloc(s); + inner->succ->push_back(s); }, &inner); if (!n && selfloopize) @@ -175,10 +172,7 @@ namespace spot cspins_state s = inner->manager->alloc_setup(dst, inner->compressed_, inner->manager->size() * 2); - auto it = inner->map.insert(s); - inner->succ->push_back(*it); - if (!it.isnew()) - inner->manager->dealloc(s); + inner->succ->push_back(s); }, &inner); if (!n && selfloopize) @@ -230,7 +224,6 @@ namespace spot selfloopize_(selfloopize), aps_(visible_aps), nb_threads_(nb_threads) { - map_.initialSize(2000000); manager_ = static_cast (::operator new(sizeof(cspins_state_manager) * nb_threads)); inner_ = new inner_callback_parameters[nb_threads_]; @@ -242,7 +235,6 @@ namespace spot cspins_state_manager(d_->get_state_size(), compress); inner_[i].compressed_ = new int[d_->get_state_size() * 2]; inner_[i].uncompressed_ = new int[d_->get_state_size()+30]; - inner_[i].map = map_; // Must be a copy per thread } dead_idx_ = -1; match_aps(visible_aps, dead_prop);