org.objectweb.dsrg.sofa.cushion.jpfcheck
Class JPFCheckerSearch

java.lang.Object
  extended by gov.nasa.jpf.search.Search
      extended by org.objectweb.dsrg.sofa.cushion.jpfcheck.JPFCheckerSearch

public class JPFCheckerSearch
extends gov.nasa.jpf.search.Search

Modified version of the DFSearch class distributed with JPF.


Field Summary
 
Fields inherited from class gov.nasa.jpf.search.Search
depth, DEPTH_CONSTRAINT, depthLimit, doBacktrack, done, errors, isEndState, isIgnoredState, isNewState, lastSearchConstraint, matchDepth, minFreeMemory, QUEUE_CONSTRAINT, SIZE_CONSTRAINT, vm
 
Constructor Summary
JPFCheckerSearch(gov.nasa.jpf.Config config, gov.nasa.jpf.jvm.JVM vm)
           
 
Method Summary
 boolean requestBacktrack()
           
 void search()
          Extended version of the search method from the DFSearch class that supports coordination of backtracking.
 void setJPFTraverser(org.ow2.dsrg.fm.origbp.DFSR.JPFTraverser jt)
           
 boolean supportsBacktrack()
           
 
Methods inherited from class gov.nasa.jpf.search.Search
addListener, addProperty, backtrack, error, error, forward, getDepth, getDepthLimit, getErrors, getLastError, getMaxSearchDepth, getProperties, getSearchConstraint, getSearchState, getStateNumber, getTransition, getVM, hasNextState, hasPropertyTermination, isEndState, isNewState, isVisitedState, notifyPropertyViolated, notifySearchConstraintHit, notifySearchFinished, notifySearchStarted, notifyStateAdvanced, notifyStateBacktracked, notifyStateProcessed, notifyStateRestored, notifyStateStored, removeListener, removeProperty, restoreState, setIgnoredState, supportsRestoreState, terminate
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

JPFCheckerSearch

public JPFCheckerSearch(gov.nasa.jpf.Config config,
                        gov.nasa.jpf.jvm.JVM vm)
Method Detail

requestBacktrack

public boolean requestBacktrack()
Overrides:
requestBacktrack in class gov.nasa.jpf.search.Search

setJPFTraverser

public void setJPFTraverser(org.ow2.dsrg.fm.origbp.DFSR.JPFTraverser jt)

search

public void search()
Extended version of the search method from the DFSearch class that supports coordination of backtracking.

Specified by:
search in class gov.nasa.jpf.search.Search

supportsBacktrack

public boolean supportsBacktrack()
Overrides:
supportsBacktrack in class gov.nasa.jpf.search.Search