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

ltsmin: update usage of brick-hashset

Browse source 
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.
This commit is contained in:
Etienne Renault 2017-03-15 08:44:29 +01:00
parent 1a37a08ba4
commit 6d282bbc6b
1 changed files with 5 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

10
spot/ltsmin/ltsmin.cc
View file

@ -1237,7 +1237,7 @@ namespace spot
{
cspins_state_manager* manager; // The state manager
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* uncompressed_;
int default_value_;
@ -1266,7 +1266,7 @@ namespace spot
{
successors_.reserve(10);
inner.manager = &manager;
inner.map = &map;
inner.map = map;
inner.succ = &successors_;
inner.default_value_ = defvalue;
inner.compress = compress;
@ -1285,7 +1285,7 @@ namespace spot
cspins_state s =
inner->manager->alloc_setup(dst, inner->compressed_,
inner->manager->size() * 2);
auto it = inner->map->insert(s);
auto it = inner->map.insert(s);
inner->succ->push_back(*it);
if (!it.isnew())
inner->manager->dealloc(s);
@ -1317,7 +1317,7 @@ namespace spot
successors_.clear();
inner.manager = &manager;
inner.succ = &successors_;
inner.map = &map;
inner.map = map;
inner.default_value_ = defvalue;
inner.compress = compress;
inner.selfloopize = selfloopize;
@ -1335,7 +1335,7 @@ namespace spot
cspins_state s =
inner->manager->alloc_setup(dst, inner->compressed_,
inner->manager->size() * 2);
auto it = inner->map->insert(s);
auto it = inner->map.insert(s);
inner->succ->push_back(*it);
if (!it.isnew())
inner->manager->dealloc(s);