Commit f7c913c5 authored by Thibault Allançon's avatar Thibault Allançon

mc: update algorithms using bricks latest release

This is the continuation of b1a28932 and 078990a7 (updating bricks
library), in order to fix existing mc algorithms compilation using the
latest bricks interface.
Co-authored-by: Etienne Renault's avatarEtienne Renault <renault@lrde.epita.fr>

* spot/mc/bloemen.hh,
spot/mc/bloemen_ec.hh,
spot/mc/cndfs.hh,
spot/mc/deadlock.hh: implementation here
parent 3e611d50
......@@ -65,20 +65,19 @@ namespace spot
};
/// \brief The haser for the previous uf_element.
struct uf_element_hasher
struct uf_element_hasher : brq::hash_adaptor<uf_element*>
{
uf_element_hasher(const uf_element*)
{ }
uf_element_hasher() = default;
brick::hash::hash128_t
hash(const uf_element* lhs) const
auto hash(const uf_element* lhs) const
{
StateHash hash;
// Not modulo 31 according to brick::hashset specifications.
unsigned u = hash(lhs->st_) % (1<<30);
return {u, u};
return u;
}
bool equal(const uf_element* lhs,
......@@ -87,11 +86,20 @@ namespace spot
StateEqual equal;
return equal(lhs->st_, rhs->st_);
}
// WARNING: temporary technical fix to have pointers in brick hash table
using hash64_t = uint64_t;
template<typename cell>
typename cell::pointer match(cell &c, const uf_element* t,
hash64_t h) const
{
// NOT very sure that dereferencing will not kill some brick property
return c.match(h) && equal(c.fetch() , t) ? c.value() : nullptr;
}
};
///< \brief Shortcut to ease shared map manipulation
using shared_map = brick::hashset::FastConcurrent <uf_element*,
uf_element_hasher>;
using shared_map = brq::concurrent_hash_set<uf_element*>;
iterable_uf(const iterable_uf<State, StateHash, StateEqual>& uf):
map_(uf.map_), tid_(uf.tid_), size_(std::thread::hardware_concurrency()),
......@@ -123,7 +131,7 @@ namespace spot
v->uf_status_ = uf_status::LIVE;
v->list_status_ = list_status::BUSY;
auto it = map_.insert({v});
auto it = map_.insert(v, uf_element_hasher());
bool b = it.isnew();
// Insertion failed, delete element
......
......@@ -72,22 +72,21 @@ namespace spot
};
/// \brief The haser for the previous uf_element.
struct uf_element_hasher
struct uf_element_hasher : brq::hash_adaptor<uf_element*>
{
uf_element_hasher(const uf_element*)
{ }
uf_element_hasher() = default;
brick::hash::hash128_t
hash(const uf_element* lhs) const
auto hash(const uf_element* lhs) const
{
StateHash hash;
// Not modulo 31 according to brick::hashset specifications.
unsigned u = hash(lhs->st_kripke) % (1<<30);
u = wang32_hash(lhs->st_prop) ^ u;
u = u % (1<<30);
return {u, u};
return u;
}
bool equal(const uf_element* lhs,
......@@ -97,11 +96,20 @@ namespace spot
return (lhs->st_prop == rhs->st_prop)
&& equal(lhs->st_kripke, rhs->st_kripke);
}
// WARNING: temporary technical fix to have pointers in brick hash table
using hash64_t = uint64_t;
template<typename cell>
typename cell::pointer match(cell &c, const uf_element* t,
hash64_t h) const
{
// NOT very sure that dereferencing will not kill some brick property
return c.match(h) && equal(c.fetch() , t) ? c.value() : nullptr;
}
};
///< \brief Shortcut to ease shared map manipulation
using shared_map = brick::hashset::FastConcurrent <uf_element*,
uf_element_hasher>;
using shared_map = brq::concurrent_hash_set<uf_element*>;
iterable_uf_ec(const iterable_uf_ec<State, StateHash, StateEqual>& uf):
map_(uf.map_), tid_(uf.tid_), size_(std::thread::hardware_concurrency()),
......@@ -134,7 +142,7 @@ namespace spot
v->uf_status_ = uf_status::LIVE;
v->list_status_ = list_status::BUSY;
auto it = map_.insert({v});
auto it = map_.insert(v, uf_element_hasher());
bool b = it.isnew();
// Insertion failed, delete element
......
......@@ -56,33 +56,31 @@ namespace spot
State st_kripke;
unsigned st_prop;
cndfs_colors* colors;
bool operator==(const product_state& other) const
{
StateEqual equal;
return (st_prop == other.st_prop)
&& equal(st_kripke, other.st_kripke);
}
};
/// \brief The hasher for the previous state.
struct state_hasher
struct state_hasher : brq::hash_adaptor<product_state>
{
state_hasher(const product_state&)
{ }
state_hasher() = default;
brick::hash::hash128_t
hash(const product_state& lhs) const
auto hash(const product_state& lhs) const
{
StateHash hash;
// Not modulo 31 according to brick::hashset specifications.
unsigned u = hash(lhs.st_kripke) % (1<<30);
u = wang32_hash(lhs.st_prop) ^ u;
u = u % (1<<30);
return {u, u};
}
bool equal(const product_state& lhs,
const product_state& rhs) const
{
StateEqual equal;
return (lhs.st_prop == rhs.st_prop)
&& equal(lhs.st_kripke, rhs.st_kripke);
return u;
}
};
......@@ -97,8 +95,7 @@ namespace spot
public:
///< \brief Shortcut to ease shared map manipulation
using shared_map = brick::hashset::FastConcurrent <product_state,
state_hasher>;
using shared_map = brq::concurrent_hash_set<product_state>;
using shared_struct = shared_map;
static shared_struct* make_shared_structure(shared_map m, unsigned i)
......@@ -162,7 +159,7 @@ namespace spot
s.colors = c;
// Try to insert the new state in the shared map.
auto it = map_.insert(s);
auto it = map_.insert(s, state_hasher());
bool b = it.isnew();
// Insertion failed, delete element
......@@ -190,7 +187,7 @@ namespace spot
push_red(product_state s, bool ignore_cyan)
{
// Try to insert the new state in the shared map.
auto it = map_.insert(s);
auto it = map_.insert(s, state_hasher());
bool b = it.isnew();
SPOT_ASSERT(!b); // should never be new in a red DFS
......@@ -489,7 +486,7 @@ namespace spot
}
else if (acc && res.second.colors->l[tid_].is_in_Rp)
{
auto it = map_.insert(s);
auto it = map_.insert(s, state_hasher());
Rp_acc_.push_back(*it);
}
}
......
......@@ -61,20 +61,19 @@ namespace spot
};
/// \brief The haser for the previous state.
struct pair_hasher
struct pair_hasher : brq::hash_adaptor<deadlock_pair*>
{
pair_hasher(const deadlock_pair*)
{ }
pair_hasher() = default;
brick::hash::hash128_t
hash(const deadlock_pair* lhs) const
auto hash(const deadlock_pair* lhs) const
{
StateHash hash;
// Not modulo 31 according to brick::hashset specifications.
unsigned u = hash(lhs->st) % (1<<30);
return {u, u};
return u;
}
bool equal(const deadlock_pair* lhs,
......@@ -83,6 +82,16 @@ namespace spot
StateEqual equal;
return equal(lhs->st, rhs->st);
}
// WARNING: temporary technical fix to have pointers in brick hash table
using hash64_t = uint64_t;
template<typename cell>
typename cell::pointer match(cell &c, const deadlock_pair* t,
hash64_t h) const
{
// NOT very sure that dereferencing will not kill some brick property
return c.match(h) && equal(c.fetch() , t) ? c.value() : nullptr;
}
};
static constexpr bool compute_deadlock =
......@@ -91,8 +100,7 @@ namespace spot
public:
///< \brief Shortcut to ease shared map manipulation
using shared_map = brick::hashset::FastConcurrent <deadlock_pair*,
pair_hasher>;
using shared_map = brq::concurrent_hash_set<deadlock_pair*>;
using shared_struct = shared_map;
static shared_struct* make_shared_structure(shared_map, unsigned)
......@@ -182,7 +190,7 @@ namespace spot
deadlock_pair* v = (deadlock_pair*) p_pair_.allocate();
v->st = s;
v->colors = ref;
auto it = map_.insert(v);
auto it = map_.insert(v, pair_hasher());
bool b = it.isnew();
// Insertion failed, delete element
......
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