Package edu.udel.cis.vsl.gmc.seq

package edu.udel.cis.vsl.gmc.seq

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
  • Class
    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.
    An EnablerIF tells you which transitions should be explored from a given state.
    A Node in the state graph for the sequential depth first search.
    The factory to get a GMC search SequentialNode, if the SequentialNode has been seen before, the seen SequentialNode will be returned, otherwise, a new SequentialNode will be created and returned.
    The stack entry that is going to be pushed onto the stack during the search.
    A StateManagerIF provides part of a generic interface to a state-transition system.