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

Swarmed variant of the CNDFS parallel emptiness-check algorithm. More...

#include <spot/mc/cndfs.hh>

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

Public Types
using	shared_map = brick::hashset::FastConcurrent< product_state, state_hasher >
	Concurrent hashset for shared state storage.
using	shared_struct = shared_map
	Type alias for shared structure.

Public Member Functions
	swarmed_cndfs (kripkecube< State, SuccIterator > &sys, twacube_ptr twa, shared_map &map, shared_struct *, unsigned tid, std::atomic< bool > &stop)
	Constructor for parallel CNDFS algorithm.
void	run ()
	Run the algorithm.
void	setup ()
	Setup thread resources.
std::pair< bool, product_state >	push_blue (product_state s, bool from_accepting)
	Push state to blue stack.
std::pair< bool, product_state >	push_red (product_state s, bool ignore_cyan)
	Push state to red stack.
bool	pop_blue ()
	Pop state from blue stack.
bool	pop_red ()
	Pop state from red stack.
void	finalize ()
	Finalize thread resources.
bool	finisher ()
	Check if this thread finished the search.
unsigned	states ()
	Return number of states visited.
unsigned	transitions ()
	Return number of transitions traversed.
unsigned	walltime ()
	Return wall time in milliseconds.
std::string	name ()
	Return algorithm name.
int	sccs ()
	Return number of SCCs found (returns -1)
mc_rvalue	result ()
	Return emptiness check result.
std::string	trace ()
	Return trace.

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

Detailed Description

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

Swarmed variant of the CNDFS parallel emptiness-check algorithm.

Member Typedef Documentation

shared_map

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

using spot::swarmed_cndfs< State, SuccIterator, StateHash, StateEqual >::shared_map = brick::hashset::FastConcurrent <product_state, state_hasher>

Concurrent hashset for shared state storage.

shared_struct

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

using spot::swarmed_cndfs< State, SuccIterator, StateHash, StateEqual >::shared_struct = shared_map

Type alias for shared structure.

Constructor & Destructor Documentation

swarmed_cndfs()

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

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

inline

Constructor for parallel CNDFS algorithm.

Member Function Documentation

finalize()

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

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

inline

Finalize thread resources.

finisher()

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

bool spot::swarmed_cndfs< 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_cndfs< 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_cndfs< State, SuccIterator, StateHash, StateEqual >::name ( )

inline

Return algorithm name.

pop_blue()

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

bool spot::swarmed_cndfs< State, SuccIterator, StateHash, StateEqual >::pop_blue ( )

inline

Pop state from blue stack.

pop_red()

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

bool spot::swarmed_cndfs< State, SuccIterator, StateHash, StateEqual >::pop_red ( )

inline

Pop state from red stack.

push_blue()

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

std::pair< bool, product_state > spot::swarmed_cndfs< State, SuccIterator, StateHash, StateEqual >::push_blue ( product_state  s, bool  from_accepting  )

inline

Push state to blue stack.

push_red()

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

std::pair< bool, product_state > spot::swarmed_cndfs< State, SuccIterator, StateHash, StateEqual >::push_red ( product_state  s, bool  ignore_cyan  )

inline

Push state to red stack.

result()

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

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

inline

Return emptiness check result.

run()

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

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

inline

Run the algorithm.

sccs()

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

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

inline

Return number of SCCs found (returns -1)

setup()

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

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

inline

Setup thread resources.

states()

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

unsigned spot::swarmed_cndfs< 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_cndfs< State, SuccIterator, StateHash, StateEqual >::trace ( )

inline

Return trace.

transitions()

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

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

inline

Return number of transitions traversed.

walltime()

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

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

inline

Return wall time in milliseconds.

---

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

• spot/mc/cndfs.hh