|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectgov.nasa.jpf.search.Search
org.objectweb.dsrg.sofa.cushion.jpfcheck.JPFCheckerSearch
public class JPFCheckerSearch
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 |
---|
public JPFCheckerSearch(gov.nasa.jpf.Config config, gov.nasa.jpf.jvm.JVM vm)
Method Detail |
---|
public boolean requestBacktrack()
requestBacktrack
in class gov.nasa.jpf.search.Search
public void setJPFTraverser(org.ow2.dsrg.fm.origbp.DFSR.JPFTraverser jt)
public void search()
search
in class gov.nasa.jpf.search.Search
public boolean supportsBacktrack()
supportsBacktrack
in class gov.nasa.jpf.search.Search
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |