Iterable Union-Find for parallel reachability algorithms. More...

#include <spot/mc/bloemen.hh>

Collaboration diagram for spot::iterable_uf< 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. More...

Public Member Functions
	iterable_uf (const iterable_uf< State, StateHash, StateEqual > &uf)
	Copy constructor. More...

	iterable_uf (shared_map &map, unsigned tid)
	Constructor from shared map and thread ID. More...

	~iterable_uf ()
	Destructor. More...

std::pair< claim_status, uf_element * >	make_claim (State a)
	Try to claim a state; returns status and element pointer. More...

uf_element *	find (uf_element *a)
	Find root of element using path compression. More...

bool	sameset (uf_element a, uf_element b)
	Check if elements are in same set. More...

bool	lock_root (uf_element *a)
	Lock root element if live; return true if successful. More...

void	unlock_root (uf_element *a)
	Unlock root element. More...

uf_element *	lock_list (uf_element *a)
	Lock next element in list. More...

void	unlock_list (uf_element *a)
	Unlock list element. More...

void	unite (uf_element a, uf_element b)
	Unite two sets. More...

uf_element *	pick_from_list (uf_element u, bool sccfound)
	Pick element from list; mark SCC as dead if complete. More...

void	remove_from_list (uf_element *a)
	Mark element as removed from list. More...

unsigned	inserted ()
	Return number of successfully inserted states. More...

Detailed Description

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

Iterable Union-Find for parallel reachability algorithms.

Member Typedef Documentation

◆ shared_map

template<typename State , typename StateHash , typename StateEqual >

using spot::iterable_uf< 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 spot::iterable_uf::claim_status

strong

Status values for claim operations.

◆ list_status

template<typename State , typename StateHash , typename StateEqual >

enum spot::iterable_uf::list_status

strong

Status values for list operations.

◆ uf_status

template<typename State , typename StateHash , typename StateEqual >

enum spot::iterable_uf::uf_status

strong

Status values for union-find elements.

Constructor & Destructor Documentation

◆ iterable_uf() [1/2]

template<typename State , typename StateHash , typename StateEqual >

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

inline

Copy constructor.

◆ iterable_uf() [2/2]

template<typename State , typename StateHash , typename StateEqual >

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

inline

Constructor from shared map and thread ID.

◆ ~iterable_uf()

template<typename State , typename StateHash , typename StateEqual >

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

inline

Destructor.

Member Function Documentation

◆ find()

template<typename State , typename StateHash , typename StateEqual >

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

inline

Find root of element using path compression.

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

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

◆ inserted()

template<typename State , typename StateHash , typename StateEqual >

unsigned spot::iterable_uf< 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< State, StateHash, StateEqual >::lock_list ( uf_element * a )

inline

Lock next element in list.

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

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

◆ lock_root()

template<typename State , typename StateHash , typename StateEqual >

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

inline

Lock root element if live; return true if successful.

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

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

◆ make_claim()

template<typename State , typename StateHash , typename StateEqual >

std::pair<claim_status, uf_element*> spot::iterable_uf< State, StateHash, StateEqual >::make_claim ( State a )

inline

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

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

◆ pick_from_list()

template<typename State , typename StateHash , typename StateEqual >

uf_element* spot::iterable_uf< 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< State, StateHash, StateEqual >::find(), spot::iterable_uf< State, StateHash, StateEqual >::uf_element::list_status_, spot::iterable_uf< State, StateHash, StateEqual >::uf_element::next_, and spot::iterable_uf< State, StateHash, StateEqual >::uf_element::uf_status_.

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

◆ remove_from_list()

template<typename State , typename StateHash , typename StateEqual >

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

inline

Mark element as removed from list.

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

◆ sameset()

template<typename State , typename StateHash , typename StateEqual >

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

inline

Check if elements are in same set.

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

◆ unite()

template<typename State , typename StateHash , typename StateEqual >

void spot::iterable_uf< State, StateHash, StateEqual >::unite	(	uf_element *	a,
		uf_element *	b
	)

inline

Unite two sets.

◆ unlock_list()

template<typename State , typename StateHash , typename StateEqual >

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

inline

Unlock list element.

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

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

◆ unlock_root()

template<typename State , typename StateHash , typename StateEqual >

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

inline

Unlock root element.

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

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

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

spot/mc/bloemen.hh

Classes

Public Types

Public Member Functions

Detailed Description

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

Member Typedef Documentation

◆ shared_map

Member Enumeration Documentation

◆ claim_status

◆ list_status

◆ uf_status

Constructor & Destructor Documentation

◆ iterable_uf() [1/2]

◆ iterable_uf() [2/2]

◆ ~iterable_uf()

Member Function Documentation

◆ find()

◆ inserted()

◆ lock_list()

◆ lock_root()

◆ make_claim()

◆ pick_from_list()

◆ remove_from_list()

◆ sameset()

◆ unite()

◆ unlock_list()

◆ unlock_root()

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