spot::swarmed_bloemen_ec< State, SuccIterator, StateHash, StateEqual > Class Template Reference

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. More...

#include <spot/mc/bloemen_ec.hh>

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

Public Types
using	uf = iterable_uf_ec< State, StateHash, StateEqual >
using	uf_element = typename uf::uf_element
using	shared_struct = uf
using	shared_map = typename uf::shared_map

Public Member Functions
	swarmed_bloemen_ec (kripkecube< State, SuccIterator > &sys, twacube_ptr twa, shared_map &map, iterable_uf_ec< State, StateHash, StateEqual > *uf, unsigned tid, std::atomic< bool > &stop)
void	run ()
void	setup ()
void	finalize ()
bool	finisher ()
unsigned	states ()
unsigned	transitions ()
unsigned	walltime ()
std::string	name ()
int	sccs ()
mc_rvalue	result ()
std::string	trace ()

Static Public Member Functions
static shared_struct *	make_shared_structure (shared_map m, unsigned i)

Detailed Description

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

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.

---

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

• spot/mc/bloemen_ec.hh