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

This class aims to explore a model to detect wether it contains a deadlock. This deadlock detection performs a DFS traversal sharing information shared among multiple threads. If Deadlock equals std::true_type performs dealock 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 >
	< More...
using	shared_struct = shared_map

Public Member Functions
	swarmed_deadlock (kripkecube< State, SuccIterator > &sys, twacube_ptr, shared_map &map, shared_struct *, unsigned tid, std::atomic< bool > &stop)
void	run ()
void	setup ()
bool	push (State s)
bool	pop ()
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, unsigned)

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 wether it contains a deadlock. This deadlock detection performs a DFS traversal sharing information shared among multiple threads. If Deadlock equals std::true_type performs dealock 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>

<

Shortcut to ease shared map manipulation

---

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

• spot/mc/deadlock.hh