This package provides sequential generic model checking functionality. It is intended to be used as a set of utilities for constructing sequential model checking applications.
Some of the services provided include:
- depth-first search of an arbitrary state-transition system
- minimal counterexample search
TRANSITION>A DfsSearcher performs a depth-first search of the state space of a transition system, stopping immediately if it finds a state satisfying the given predicate.EnablerIF<STATE, TRANSITION>An EnablerIF tells you which transitions should be explored from a given state.SequentialNode<STATE>A Node in the state graph for the sequential depth first search.SequentialNodeFactory<STATE, TRANSITION>StackEntry<STATE, TRANSITION>The stack entry that is going to be pushed onto the stack during the search.StateManager<STATE, TRANSITION>A StateManagerIF provides part of a generic interface to a state-transition system.