Commit e9c274ec authored by Etienne Renault's avatar Etienne Renault

ltsmin: remove shared table at model level

Experiments shows  that this table slows down algorithms
since the management is also tracked at higher lever by
algorithms

* spot/ltsmin/spins_kripke.hh,
spot/ltsmin/spins_kripke.hxx: here.
parent 7a06b33e
......@@ -79,10 +79,6 @@ namespace spot
}
};
/// \brief Shortcut to avoid long names...
typedef brick::hashset::FastConcurrent<cspins_state, cspins_state_hasher>
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<cspins_state>* 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<std::string> aps_;
cspins_state_map map_;
unsigned int nb_threads_;
};
......
......@@ -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<cspins_state_manager*>
(::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);
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment