Bloemen parallel SCC decomposition algorithm for reachability. More...

#include <spot/mc/bloemen.hh>

Collaboration diagram for spot::swarmed_bloemen< State, SuccIterator, StateHash, StateEqual >:

Public Types
using	uf = iterable_uf< State, StateHash, StateEqual >
	Type alias for iterable union-find. More...

using	uf_element = typename uf::uf_element
	Type alias for union-find element. More...

using	shared_struct = uf
	Type alias for shared structure. More...

using	shared_map = typename uf::shared_map
	Type alias for shared map. More...

Public Member Functions
	swarmed_bloemen (kripkecube< State, SuccIterator > &sys, twacube_ptr, shared_map &map, iterable_uf< State, StateHash, StateEqual > *uf, unsigned tid, std::atomic< bool > &stop)
	Constructor for parallel Bloemen algorithm. More...

void	run ()
	Run the algorithm. More...

void	setup ()
	Setup thread resources. More...

void	finalize ()
	Finalize thread resources. More...

bool	finisher ()
	Check if this thread finished the search. More...

unsigned	states ()
	Return number of states visited. More...

unsigned	transitions ()
	Return number of transitions traversed. More...

unsigned	walltime ()
	Return wall time in milliseconds. More...

std::string	name ()
	Return algorithm name. More...

int	sccs ()
	Return number of SCCs found. More...

mc_rvalue	result ()
	Return emptiness check result. More...

std::string	trace ()
	Return trace (returns empty string) More...

Static Public Member Functions
static shared_struct *	make_shared_structure (shared_map m, unsigned i)
	Create shared structure for thread tid. More...

Detailed Description

template<typename State, typename SuccIterator, typename StateHash, typename StateEqual>
class spot::swarmed_bloemen< State, SuccIterator, StateHash, StateEqual >

Bloemen parallel SCC decomposition algorithm for reachability.

This class implements the SCC decomposition algorithm of Bloemen as described in PPOPP'16. It uses a shared union-find augmented to manage work stealing between threads.

Member Typedef Documentation

◆ shared_map

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >

using spot::swarmed_bloemen< State, SuccIterator, StateHash, StateEqual >::shared_map = typename uf::shared_map

Type alias for shared map.

◆ shared_struct

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >

using spot::swarmed_bloemen< State, SuccIterator, StateHash, StateEqual >::shared_struct = uf

Type alias for shared structure.

◆ uf

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >

using spot::swarmed_bloemen< State, SuccIterator, StateHash, StateEqual >::uf = iterable_uf<State, StateHash, StateEqual>

Type alias for iterable union-find.

◆ uf_element

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >

using spot::swarmed_bloemen< State, SuccIterator, StateHash, StateEqual >::uf_element = typename uf::uf_element

Type alias for union-find element.

Constructor & Destructor Documentation

◆ swarmed_bloemen()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >

spot::swarmed_bloemen< State, SuccIterator, StateHash, StateEqual >::swarmed_bloemen	(	kripkecube< State, SuccIterator > &	sys,
		twacube_ptr	,
		shared_map &	map,
		iterable_uf< State, StateHash, StateEqual > *	uf,
		unsigned	tid,
		std::atomic< bool > &	stop
	)

inline

Constructor for parallel Bloemen algorithm.

Member Function Documentation

◆ finalize()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >

void spot::swarmed_bloemen< State, SuccIterator, StateHash, StateEqual >::finalize ( )

inline

Finalize thread resources.

References spot::timer_map::stop().

Referenced by spot::swarmed_bloemen< State, SuccIterator, StateHash, StateEqual >::run().

◆ finisher()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >

bool spot::swarmed_bloemen< State, SuccIterator, StateHash, StateEqual >::finisher ( )

inline

Check if this thread finished the search.

◆ make_shared_structure()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >

static shared_struct* spot::swarmed_bloemen< State, SuccIterator, StateHash, StateEqual >::make_shared_structure	(	shared_map	m,
		unsigned	i
	)

inlinestatic

Create shared structure for thread tid.

◆ name()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >

std::string spot::swarmed_bloemen< State, SuccIterator, StateHash, StateEqual >::name ( )

inline

Return algorithm name.

◆ result()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >

mc_rvalue spot::swarmed_bloemen< State, SuccIterator, StateHash, StateEqual >::result ( )

inline

Return emptiness check result.

References spot::SUCCESS.

◆ run()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >

void spot::swarmed_bloemen< State, SuccIterator, StateHash, StateEqual >::run ( )

inline

Run the algorithm.

References spot::swarmed_bloemen< State, SuccIterator, StateHash, StateEqual >::finalize(), and spot::swarmed_bloemen< State, SuccIterator, StateHash, StateEqual >::setup().

◆ sccs()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >

int spot::swarmed_bloemen< State, SuccIterator, StateHash, StateEqual >::sccs ( )

inline

Return number of SCCs found.

◆ setup()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >

void spot::swarmed_bloemen< State, SuccIterator, StateHash, StateEqual >::setup ( )

inline

Setup thread resources.

References spot::timer_map::start().

Referenced by spot::swarmed_bloemen< State, SuccIterator, StateHash, StateEqual >::run().

◆ states()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >

unsigned spot::swarmed_bloemen< State, SuccIterator, StateHash, StateEqual >::states ( )

inline

Return number of states visited.

◆ trace()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >

std::string spot::swarmed_bloemen< State, SuccIterator, StateHash, StateEqual >::trace ( )

inline

Return trace (returns empty string)

◆ transitions()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >

unsigned spot::swarmed_bloemen< State, SuccIterator, StateHash, StateEqual >::transitions ( )

inline

Return number of transitions traversed.

◆ walltime()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >

unsigned spot::swarmed_bloemen< State, SuccIterator, StateHash, StateEqual >::walltime ( )

inline

Return wall time in milliseconds.

References spot::timer_map::timer(), and spot::timer::walltime().

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

spot/mc/bloemen.hh

Public Types

Public Member Functions

Static Public Member Functions

Detailed Description

template<typename State, typename SuccIterator, typename StateHash, typename StateEqual> class spot::swarmed_bloemen< State, SuccIterator, StateHash, StateEqual >

Member Typedef Documentation

◆ shared_map

◆ shared_struct

◆ uf

◆ uf_element

Constructor & Destructor Documentation

◆ swarmed_bloemen()

Member Function Documentation

◆ finalize()

◆ finisher()

◆ make_shared_structure()

◆ name()

◆ result()

◆ run()

◆ sccs()

◆ setup()

◆ states()

◆ trace()

◆ transitions()

◆ walltime()

template<typename State, typename SuccIterator, typename StateHash, typename StateEqual>
class spot::swarmed_bloemen< State, SuccIterator, StateHash, StateEqual >