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

This class aims to explore a model to detect whether it contains a deadlock. This deadlock detection performs a DFS traversal sharing information shared among multiple threads. If Deadlock equals std::true_type performs deadlock algorithm, otherwise perform a simple reachability. More...

#include <spot/mc/deadlock.hh>

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

Public Types
using	shared_map = brick::hashset::FastConcurrent< deadlock_pair *, pair_hasher >
	Concurrent hashset for shared state storage. More...
using	shared_struct = shared_map
	Type alias for shared structure. More...

Public Member Functions
	swarmed_deadlock (kripkecube< State, SuccIterator > &sys, twacube_ptr, shared_map &map, shared_struct *, unsigned tid, std::atomic< bool > &stop)
	Constructor for parallel deadlock detection. More...
void	run ()
	Run the algorithm. More...
void	setup ()
	Setup thread resources. More...
bool	push (State s)
	Push state onto stack. More...
bool	pop ()
	Pop state from stack. 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 (returns -1) More...
mc_rvalue	result ()
	Return deadlock detection result. More...
std::string	trace ()
	Return trace. More...

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

Detailed Description

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

This class aims to explore a model to detect whether it contains a deadlock. This deadlock detection performs a DFS traversal sharing information shared among multiple threads. If Deadlock equals std::true_type performs deadlock algorithm, otherwise perform a simple reachability.

Member Typedef Documentation

shared_map

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

using spot::swarmed_deadlock< State, SuccIterator, StateHash, StateEqual, Deadlock >::shared_map = brick::hashset::FastConcurrent <deadlock_pair*, pair_hasher>

Concurrent hashset for shared state storage.

shared_struct

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

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

Type alias for shared structure.

Constructor & Destructor Documentation

swarmed_deadlock()

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

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

inline

Constructor for parallel deadlock detection.

Member Function Documentation

finalize()

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

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

inline

Finalize thread resources.

finisher()

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

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

inline

Check if this thread finished the search.

make_shared_structure()

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

static shared_struct * spot::swarmed_deadlock< State, SuccIterator, StateHash, StateEqual, Deadlock >::make_shared_structure ( shared_map  , unsigned    )

inlinestatic

Create shared structure for thread tid.

name()

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

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

inline

Return algorithm name.

pop()

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

bool spot::swarmed_deadlock< State, SuccIterator, StateHash, StateEqual, Deadlock >::pop ( )

inline

Pop state from stack.

push()

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

bool spot::swarmed_deadlock< State, SuccIterator, StateHash, StateEqual, Deadlock >::push ( State  s )

inline

Push state onto stack.

result()

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

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

inline

Return deadlock detection result.

References spot::DEADLOCK, spot::NO_DEADLOCK, and spot::SUCCESS.

run()

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

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

inline

Run the algorithm.

sccs()

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

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

inline

Return number of SCCs found (returns -1)

setup()

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

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

inline

Setup thread resources.

states()

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

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

inline

Return number of states visited.

trace()

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

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

inline

Return trace.

transitions()

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

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

inline

Return number of transitions traversed.

walltime()

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

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

inline

Return wall time in milliseconds.

---

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

• spot/mc/deadlock.hh