spot::iterable_uf_ec< State, StateHash, StateEqual > Class Template Reference

Iterable Union-Find for parallel emptiness-check algorithms. More...

#include <spot/mc/bloemen_ec.hh>

Collaboration diagram for spot::iterable_uf_ec< State, StateHash, StateEqual >:

Classes
struct	uf_element
	Represents a Union-Find element. More...
struct	uf_element_hasher
	Hasher for union-find elements. More...

Public Types
enum class	uf_status { LIVE , LOCK , DEAD }
	Status values for union-find elements. More...
enum class	list_status { BUSY , LOCK , DONE }
	Status values for list operations. More...
enum class	claim_status { CLAIM_FOUND , CLAIM_NEW , CLAIM_DEAD }
	Status values for claim operations. More...
using	shared_map = brick::hashset::FastConcurrent< uf_element *, uf_element_hasher >
	Concurrent hashset for shared state storage.

Public Member Functions
	iterable_uf_ec (const iterable_uf_ec< State, StateHash, StateEqual > &uf)
	Copy constructor.
	iterable_uf_ec (shared_map &map, unsigned tid)
	Constructor from shared map and thread ID.
	~iterable_uf_ec ()
	Destructor.
std::pair< claim_status, uf_element * >	make_claim (State kripke, unsigned prop)
	Try to claim a state; returns status and element pointer.
uf_element *	find (uf_element *a)
	Find root of element using path compression.
bool	sameset (uf_element *a, uf_element *b)
	Check if elements are in same set.
bool	lock_root (uf_element *a)
	Lock root element if live; return true if successful.
void	unlock_root (uf_element *a)
	Unlock root element.
uf_element *	lock_list (uf_element *a)
	Lock next element in list.
void	unlock_list (uf_element *a)
	Unlock list element.
acc_cond::mark_t	unite (uf_element *a, uf_element *b, acc_cond::mark_t acc)
	Unite two sets with acceptance condition; return new acc.
uf_element *	pick_from_list (uf_element *u, bool *sccfound)
	Pick element from list; mark SCC as dead if complete.
void	remove_from_list (uf_element *a)
	Mark element as removed from list.
unsigned	inserted ()
	Return number of successfully inserted states.

Detailed Description

template<typename State, typename StateHash, typename StateEqual>
class spot::iterable_uf_ec< State, StateHash, StateEqual >

Iterable Union-Find for parallel emptiness-check algorithms.

Member Typedef Documentation

shared_map

template<typename State , typename StateHash , typename StateEqual >

using spot::iterable_uf_ec< State, StateHash, StateEqual >::shared_map = brick::hashset::FastConcurrent <uf_element*, uf_element_hasher>

Concurrent hashset for shared state storage.

Member Enumeration Documentation

claim_status

template<typename State , typename StateHash , typename StateEqual >

enum class spot::iterable_uf_ec::claim_status

strong

Status values for claim operations.

list_status

template<typename State , typename StateHash , typename StateEqual >

enum class spot::iterable_uf_ec::list_status

strong

Status values for list operations.

uf_status

template<typename State , typename StateHash , typename StateEqual >

enum class spot::iterable_uf_ec::uf_status

strong

Status values for union-find elements.

Constructor & Destructor Documentation

iterable_uf_ec() [1/2]

template<typename State , typename StateHash , typename StateEqual >

spot::iterable_uf_ec< State, StateHash, StateEqual >::iterable_uf_ec ( const iterable_uf_ec< State, StateHash, StateEqual > &  uf )

inline

Copy constructor.

iterable_uf_ec() [2/2]

template<typename State , typename StateHash , typename StateEqual >

spot::iterable_uf_ec< State, StateHash, StateEqual >::iterable_uf_ec ( shared_map &  map, unsigned  tid  )

inline

Constructor from shared map and thread ID.

~iterable_uf_ec()

template<typename State , typename StateHash , typename StateEqual >

spot::iterable_uf_ec< State, StateHash, StateEqual >::~iterable_uf_ec ( )

inline

Destructor.

Member Function Documentation

find()

template<typename State , typename StateHash , typename StateEqual >

uf_element * spot::iterable_uf_ec< State, StateHash, StateEqual >::find ( uf_element *  a )

inline

Find root of element using path compression.

References spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element::parent.

Referenced by spot::iterable_uf_ec< State, StateHash, StateEqual >::make_claim(), spot::iterable_uf_ec< State, StateHash, StateEqual >::pick_from_list(), spot::iterable_uf_ec< State, StateHash, StateEqual >::sameset(), and spot::iterable_uf_ec< State, StateHash, StateEqual >::unite().

inserted()

template<typename State , typename StateHash , typename StateEqual >

unsigned spot::iterable_uf_ec< State, StateHash, StateEqual >::inserted ( )

inline

Return number of successfully inserted states.

lock_list()

template<typename State , typename StateHash , typename StateEqual >

uf_element * spot::iterable_uf_ec< State, StateHash, StateEqual >::lock_list ( uf_element *  a )

inline

Lock next element in list.

References spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element::list_status_, spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element::next_, and spot::iterable_uf_ec< State, StateHash, StateEqual >::pick_from_list().

Referenced by spot::iterable_uf_ec< State, StateHash, StateEqual >::unite().

lock_root()

template<typename State , typename StateHash , typename StateEqual >

bool spot::iterable_uf_ec< State, StateHash, StateEqual >::lock_root ( uf_element *  a )

inline

Lock root element if live; return true if successful.

References spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element::parent, spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element::uf_status_, and spot::iterable_uf_ec< State, StateHash, StateEqual >::unlock_root().

Referenced by spot::iterable_uf_ec< State, StateHash, StateEqual >::unite().

make_claim()

template<typename State , typename StateHash , typename StateEqual >

std::pair< claim_status, uf_element * > spot::iterable_uf_ec< State, StateHash, StateEqual >::make_claim ( State  kripke, unsigned  prop  )

inline

Try to claim a state; returns status and element pointer.

References spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element::acc, spot::fixed_size_pool< Kind >::allocate(), spot::fixed_size_pool< Kind >::deallocate(), spot::iterable_uf_ec< State, StateHash, StateEqual >::find(), spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element::list_status_, spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element::next_, spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element::parent, spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element::st_kripke, spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element::st_prop, spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element::uf_status_, and spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element::worker_.

pick_from_list()

template<typename State , typename StateHash , typename StateEqual >

uf_element * spot::iterable_uf_ec< State, StateHash, StateEqual >::pick_from_list ( uf_element *  u, bool *  sccfound  )

inline

Pick element from list; mark SCC as dead if complete.

References spot::iterable_uf_ec< State, StateHash, StateEqual >::find(), spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element::list_status_, spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element::next_, and spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element::uf_status_.

Referenced by spot::iterable_uf_ec< State, StateHash, StateEqual >::lock_list().

remove_from_list()

template<typename State , typename StateHash , typename StateEqual >

void spot::iterable_uf_ec< State, StateHash, StateEqual >::remove_from_list ( uf_element *  a )

inline

Mark element as removed from list.

References spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element::list_status_.

sameset()

template<typename State , typename StateHash , typename StateEqual >

bool spot::iterable_uf_ec< State, StateHash, StateEqual >::sameset ( uf_element *  a, uf_element *  b  )

inline

Check if elements are in same set.

References spot::iterable_uf_ec< State, StateHash, StateEqual >::find(), and spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element::parent.

unite()

template<typename State , typename StateHash , typename StateEqual >

acc_cond::mark_t spot::iterable_uf_ec< State, StateHash, StateEqual >::unite ( uf_element *  a, uf_element *  b, acc_cond::mark_t  acc  )

inline

Unite two sets with acceptance condition; return new acc.

References spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element::acc, spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element::acc_mutex_, spot::iterable_uf_ec< State, StateHash, StateEqual >::find(), spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element::list_status_, spot::iterable_uf_ec< State, StateHash, StateEqual >::lock_list(), spot::iterable_uf_ec< State, StateHash, StateEqual >::lock_root(), spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element::next_, spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element::parent, spot::iterable_uf_ec< State, StateHash, StateEqual >::unlock_list(), spot::iterable_uf_ec< State, StateHash, StateEqual >::unlock_root(), and spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element::worker_.

unlock_list()

template<typename State , typename StateHash , typename StateEqual >

void spot::iterable_uf_ec< State, StateHash, StateEqual >::unlock_list ( uf_element *  a )

inline

Unlock list element.

References spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element::list_status_.

Referenced by spot::iterable_uf_ec< State, StateHash, StateEqual >::unite().

unlock_root()

template<typename State , typename StateHash , typename StateEqual >

void spot::iterable_uf_ec< State, StateHash, StateEqual >::unlock_root ( uf_element *  a )

inline

Unlock root element.

References spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element::uf_status_.

Referenced by spot::iterable_uf_ec< State, StateHash, StateEqual >::lock_root(), and spot::iterable_uf_ec< State, StateHash, StateEqual >::unite().

---

The documentation for this class was generated from the following file:

• spot/mc/bloemen_ec.hh