Commit 2a854d55 authored by Etienne Renault's avatar Etienne Renault
Browse files

ltsmin: update usage of brick-hashset

From a discussion with Petr Rockai: "the possibly non-intuitive bit
that you probably didn't notice is that the hashset is supposed to be
passed to each thread by value. The copy semantics of the entire
hashset are that of a shared pointer: multiple copies share the same
underlying data. Each thread *must* have its own private copy of the
hashset object (there are bits of state that each thread needs for
bookkeeping and those must not be shared)."

*  spot/ltsmin/ltsmin.cc: here.
parent d8b6439c
...@@ -1233,7 +1233,7 @@ namespace spot ...@@ -1233,7 +1233,7 @@ 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; cspins_state_map map; // Must be a copy!
int* compressed_; int* compressed_;
int* uncompressed_; int* uncompressed_;
int default_value_; int default_value_;
...@@ -1262,7 +1262,7 @@ namespace spot ...@@ -1262,7 +1262,7 @@ namespace spot
{ {
successors_.reserve(10); successors_.reserve(10);
inner.manager = &manager; inner.manager = &manager;
inner.map = &map; inner.map = map;
inner.succ = &successors_; inner.succ = &successors_;
inner.default_value_ = defvalue; inner.default_value_ = defvalue;
inner.compress = compress; inner.compress = compress;
...@@ -1281,7 +1281,7 @@ namespace spot ...@@ -1281,7 +1281,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); auto it = inner->map.insert(s);
inner->succ->push_back(*it); inner->succ->push_back(*it);
if (!it.isnew()) if (!it.isnew())
inner->manager->dealloc(s); inner->manager->dealloc(s);
...@@ -1313,7 +1313,7 @@ namespace spot ...@@ -1313,7 +1313,7 @@ namespace spot
successors_.clear(); successors_.clear();
inner.manager = &manager; inner.manager = &manager;
inner.succ = &successors_; inner.succ = &successors_;
inner.map = &map; inner.map = map;
inner.default_value_ = defvalue; inner.default_value_ = defvalue;
inner.compress = compress; inner.compress = compress;
inner.selfloopize = selfloopize; inner.selfloopize = selfloopize;
...@@ -1331,7 +1331,7 @@ namespace spot ...@@ -1331,7 +1331,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); auto it = inner->map.insert(s);
inner->succ->push_back(*it); inner->succ->push_back(*it);
if (!it.isnew()) if (!it.isnew())
inner->manager->dealloc(s); inner->manager->dealloc(s);
......
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