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
    Description
    DfsSearcher<STATE,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>
    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.
    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.