Parallel Model Checking

Classes
class	spot::iterable_uf< State, StateHash, StateEqual >
	Iterable Union-Find for parallel reachability algorithms. More...
class	spot::swarmed_bloemen< State, SuccIterator, StateHash, StateEqual >
	Bloemen parallel SCC decomposition algorithm for reachability. More...
class	spot::iterable_uf_ec< State, StateHash, StateEqual >
	Iterable Union-Find for parallel emptiness-check algorithms. More...
class	spot::swarmed_bloemen_ec< State, SuccIterator, StateHash, StateEqual >
	Bloemen parallel SCC decomposition algorithm for emptiness check. More...
class	spot::swarmed_cndfs< State, SuccIterator, StateHash, StateEqual >
	Swarmed variant of the CNDFS parallel emptiness-check algorithm. More...
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. 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::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 optimizations (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.