spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element Struct Reference

Represents a Union-Find element. More...

#include <spot/mc/bloemen_ec.hh>

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

Public Attributes
State	st_kripke
	the kripke state handled by the element More...
unsigned	st_prop
	the prop state handled by the element More...
acc_cond::mark_t	acc
	acceptance conditions of the union More...
std::mutex	acc_mutex_
	mutex for acceptance condition More...
std::atomic< uf_element * >	parent
	reference to the pointer More...
std::atomic< unsigned >	worker_
	The set of worker for a given state. More...
std::atomic< uf_element * >	next_
	next element for work stealing More...
std::atomic< uf_status >	uf_status_
	current status for the element More...
std::atomic< list_status >	list_status_
	current status for the list More...

Detailed Description

template<typename State, typename StateHash, typename StateEqual>
struct spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element

Represents a Union-Find element.

Member Data Documentation

acc

template<typename State , typename StateHash , typename StateEqual >

acc_cond::mark_t spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element::acc

acceptance conditions of the union

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

acc_mutex_

template<typename State , typename StateHash , typename StateEqual >

std::mutex spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element::acc_mutex_

mutex for acceptance condition

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

list_status_

template<typename State , typename StateHash , typename StateEqual >

std::atomic<list_status> spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element::list_status_

current status for the list

Referenced by spot::iterable_uf_ec< State, StateHash, StateEqual >::lock_list(), 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 >::remove_from_list(), spot::iterable_uf_ec< State, StateHash, StateEqual >::unite(), and spot::iterable_uf_ec< State, StateHash, StateEqual >::unlock_list().

next_

template<typename State , typename StateHash , typename StateEqual >

std::atomic<uf_element*> spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element::next_

next element for work stealing

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

parent

template<typename State , typename StateHash , typename StateEqual >

std::atomic<uf_element*> spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element::parent

reference to the pointer

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

st_kripke

template<typename State , typename StateHash , typename StateEqual >

State spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element::st_kripke

the kripke state handled by the element

Referenced by spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element_hasher::equal(), spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element_hasher::hash(), and spot::iterable_uf_ec< State, StateHash, StateEqual >::make_claim().

st_prop

template<typename State , typename StateHash , typename StateEqual >

unsigned spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element::st_prop

the prop state handled by the element

Referenced by spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element_hasher::equal(), spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element_hasher::hash(), and spot::iterable_uf_ec< State, StateHash, StateEqual >::make_claim().

uf_status_

template<typename State , typename StateHash , typename StateEqual >

std::atomic<uf_status> spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element::uf_status_

current status for the element

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

worker_

template<typename State , typename StateHash , typename StateEqual >

std::atomic<unsigned> spot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element::worker_

The set of worker for a given state.

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

---

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

• spot/mc/bloemen_ec.hh