Parallel Model Checking

Classes
class	spot::swarmed_bloemen< 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. More...
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. More...
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 deadlock algorithm, otherwise perform a simple reachability. More...
class	spot::lpar13< State, SuccIterator, StateHash, StateEqual >
	This class implements the sequential emptiness check as presented in "Three SCC-based Emptiness Checks for Generalized Büchi Automata" (Renault et al, LPAR 2013). Among the three emptiness checks that have been proposed, we opted to implement yGabow's one. More...
class	spot::is_a_mc_algorithm< T >
	This class allows to ensure (at compile time) if a given parameter can be considered as a modelchecking algorithm (i.e., usable by instantiate) More...
class	spot::int_unionfind
	This Union-Find data structure is a particular union-find, dedicated for emptiness checks below, see ec.hh. The key of this union-find is int. Moreover, we suppose that only consecutive int are inserted. This union-find includes most of the classical optimisations (IPC, LR, PC, MS). More...
class	spot::kripkecube_to_twa< State, SuccIterator, StateHash, StateEqual >
	convert a (cube) model into a twa. Note that this algorithm cannot be run in parallel but could. More...
class	spot::product_to_twa< State, SuccIterator, StateHash, StateEqual >
	convert a (cube) product automaton into a twa Note that this algorithm cannot be run in parallel. More...

Detailed Description

Algorithms and data structures for parallel model checking, including deadlock detection, reachability, and SCC computation.