alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

ltsmin: remove shared table at model level

Browse source 
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.
This commit is contained in:
Etienne Renault 2017-09-29 14:10:45 +02:00
parent d2549334f9
commit 1d4cb26235
2 changed files with 2 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

6
spot/ltsmin/spins_kripke.hh
View file

@ -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 /// \brief The management of states (i.e. allocation/deallocation) can
/// be painless since every time we have to consider wether the state will /// be painless since every time we have to consider wether the state will
/// be compressed or not. This class aims to simplify this management /// be compressed or not. This class aims to simplify this management
@ -113,7 +109,6 @@ namespace spot
{ {
cspins_state_manager* manager; // The state manager cspins_state_manager* manager; // The state manager
std::vector<cspins_state>* succ; // The successors of a state 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* compressed_;
int* uncompressed_; int* uncompressed_;
bool compress; bool compress;
@ -215,7 +210,6 @@ namespace spot
bool selfloopize_; bool selfloopize_;
int dead_idx_; int dead_idx_;
std::vector<std::string> aps_; std::vector<std::string> aps_;
cspins_state_map map_;
unsigned int nb_threads_; unsigned int nb_threads_;
}; };

12
spot/ltsmin/spins_kripke.hxx
View file

@ -129,10 +129,7 @@ namespace spot
cspins_state s = cspins_state s =
inner->manager->alloc_setup(dst, inner->compressed_, inner->manager->alloc_setup(dst, inner->compressed_,
inner->manager->size() * 2); inner->manager->size() * 2);
auto it = inner->map.insert(s); inner->succ->push_back(s);
inner->succ->push_back(*it);
if (!it.isnew())
inner->manager->dealloc(s);
}, },
&inner); &inner);
if (!n && selfloopize) if (!n && selfloopize)
@ -175,10 +172,7 @@ namespace spot
cspins_state s = cspins_state s =
inner->manager->alloc_setup(dst, inner->compressed_, inner->manager->alloc_setup(dst, inner->compressed_,
inner->manager->size() * 2); inner->manager->size() * 2);
auto it = inner->map.insert(s); inner->succ->push_back(s);
inner->succ->push_back(*it);
if (!it.isnew())
inner->manager->dealloc(s);
}, },
&inner); &inner);
if (!n && selfloopize) if (!n && selfloopize)
@ -230,7 +224,6 @@ namespace spot
selfloopize_(selfloopize), aps_(visible_aps), selfloopize_(selfloopize), aps_(visible_aps),
nb_threads_(nb_threads) nb_threads_(nb_threads)
{ {
map_.initialSize(2000000);
manager_ = static_cast<cspins_state_manager*> manager_ = static_cast<cspins_state_manager*>
(::operator new(sizeof(cspins_state_manager) * nb_threads)); (::operator new(sizeof(cspins_state_manager) * nb_threads));
inner_ = new inner_callback_parameters[nb_threads_]; inner_ = new inner_callback_parameters[nb_threads_];
@ -242,7 +235,6 @@ namespace spot
cspins_state_manager(d_->get_state_size(), compress); cspins_state_manager(d_->get_state_size(), compress);
inner_[i].compressed_ = new int[d_->get_state_size() * 2]; inner_[i].compressed_ = new int[d_->get_state_size() * 2];
inner_[i].uncompressed_ = new int[d_->get_state_size()+30]; inner_[i].uncompressed_ = new int[d_->get_state_size()+30];
inner_[i].map = map_; // Must be a copy per thread
} }
dead_idx_ = -1; dead_idx_ = -1;
match_aps(visible_aps, dead_prop); match_aps(visible_aps, dead_prop);