This package provides concurrent generic model checking functionality. It is intended to be used as a set of utilities for constructing concurrent model checking applications.
Some of the services provided include:
- Concurrent depth first searcher of an arbitrary state-transition system
TRANSITION>This ConcurrentDfsSearcher is implemented based on Alfons Laarman's algorithm in paper "Partial-Order Reduction for Multi-Core LTL Model Checking", but there are improvements being made.ConcurrentNode<STATE>ConcurrentNodeFactory<STATE, TRANSITION>ConcurrentStateManagerIF<STATE, TRANSITION>The threadPool That is used to manage the threads used in the algorithm.This enumeration stores the result of checking "stack proviso" of a STATE in the STATE-TRANSITION system.StackEntry<STATE, TRANSITION>The stack entry that is going to be pushed onto the stack during the search.