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