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

ltsmin: use FastConcurrent map

Browse source 
* spot/ltsmin/ltsmin.cc: here.
This commit is contained in:
Etienne Renault 2016-04-11 13:02:40 +02:00
parent 01f66642f1
commit 681c2b2011
1 changed files with 38 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

59
spot/ltsmin/ltsmin.cc
View file

@ -42,6 +42,8 @@
#include <string.h> #include <string.h>
#include <spot/twacube/cube.hh> #include <spot/twacube/cube.hh>
#include <spot/mc/utils.hh> #include <spot/mc/utils.hh>
#include <bricks/brick-hashset.h>
#include <bricks/brick-hash.h>
using namespace std::string_literals; using namespace std::string_literals;
@ -1115,12 +1117,36 @@ namespace spot
} }
}; };
typedef std::unordered_map<const cspins_state, int, cspins_state_hash, struct both
cspins_state_equal> cspins_state_map; {
cspins_state first;
int second;
};
typedef std::unordered_set<cspins_state, cspins_state_hash, struct cspins_state_hasher
cspins_state_equal> cspins_state_set; {
cspins_state_hasher(cspins_state&)
{ }
cspins_state_hasher() = default;
brick::hash::hash128_t
hash(cspins_state t) const
{
// FIXME we should compute a better hash value for this particular
// case. Shall we use two differents hash functions?
return std::make_pair(t[0], t[0]);
}
bool equal(cspins_state lhs, cspins_state rhs) const
{
return 0 == memcmp(lhs, rhs, (2+rhs[1])* sizeof(int));
}
};
//brick::hashset::FastConcurrent<both , both_hasher> ht2;
typedef brick::hashset::FastConcurrent<cspins_state,
cspins_state_hasher> cspins_state_map;
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
// A manager for Cspins states. // A manager for Cspins states.
@ -1255,12 +1281,10 @@ 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->default_value_}); auto it = inner->map->insert({s});
inner->succ->push_back((*(it.first)).first); inner->succ->push_back(*it);
if (!it.second) if (!it.isnew())
{ inner->manager->dealloc(s);
inner->manager->dealloc(s);
}
}, },
&inner); &inner);
if (!n && selfloopize) if (!n && selfloopize)
@ -1306,9 +1330,9 @@ 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->default_value_}); auto it = inner->map->insert({s});
inner->succ->push_back((*(it.first)).first); inner->succ->push_back(*it);
if (!it.second) if (!it.isnew())
inner->manager->dealloc(s); inner->manager->dealloc(s);
}, },
&inner); &inner);
@ -1387,7 +1411,7 @@ namespace spot
compress_(compress), cubeset_(visible_aps.size()), compress_(compress), cubeset_(visible_aps.size()),
selfloopize_(selfloopize), aps_(visible_aps) selfloopize_(selfloopize), aps_(visible_aps)
{ {
map_.reserve(2000000); map_.setSize(2000000);
recycle_.reserve(2000000); recycle_.reserve(2000000);
inner_.compressed_ = new int[d_->get_state_size() * 2]; inner_.compressed_ = new int[d_->get_state_size() * 2];
inner_.uncompressed_ = new int[d_->get_state_size()+30]; inner_.uncompressed_ = new int[d_->get_state_size()+30];
@ -1396,13 +1420,6 @@ namespace spot
} }
~kripkecube() ~kripkecube()
{ {
typename cspins_state_map::const_iterator s = map_.begin();
while (s != map_.end())
{
manager_.dealloc(s->first);
++s;
}
map_.clear();
for (auto i: recycle_) for (auto i: recycle_)
{ {
cubeset_.release(i->condition()); cubeset_.release(i->condition());