Search

java.lang.Object
- gov.nasa.jpf.search.Search

Direct Known Subclasses:

DFSearch, HeuristicSearch, NewHeuristicSearch, PathSearch, RandomSearch, Simulation
```
public abstract class Search
extends java.lang.Object
```
the mother of all search classes. Mostly takes care of listeners, keeping track of state attributes and errors. This class mainly keeps the general search info like depth, configured properties etc.

Field Summary

Fields
Modifier and Type	Field and Description
`protected Config`	`config`
`protected Error`	`currentError` error encountered during last transition, null otherwise
`protected int`	`depth`
`protected int`	`depthLimit`
`protected boolean`	`doBacktrack`
`protected boolean`	`done`
`protected java.util.ArrayList<Error>`	`errors`
`protected boolean`	`getAllErrors`
`protected java.lang.String`	`lastSearchConstraint`
`protected SearchListener[]`	`listeners` search listeners.
`protected static JPFLogger`	`log`
`protected boolean`	`matchDepth`
`protected long`	`minFreeMemory`
`protected java.util.concurrent.atomic.AtomicBoolean`	`notifyProbeListeners`
`protected java.util.ArrayList<Property>`	`properties`
`protected Reporter`	`reporter` this is a special SearchListener that is always notified last, so that PublisherExtensions can be sure the notification has been processed by all listeners
`protected IntVector`	`stateDepth` storage to keep track of state depths
`protected VM`	`vm`

Constructor Summary

Constructors
Modifier Constructor and Description

protected Search(Config config, VM vm)

Constructors
Modifier	Constructor and Description
`protected`	`Search(Config config, VM vm)`

Method Summary

All Methods Instance Methods Abstract Methods Concrete Methods
Modifier and Type	Method and Description
`void`	`addListener(SearchListener newListener)`
`void`	`addProperty(Property newProperty)`
`protected boolean`	`backtrack()`
`protected boolean`	`checkAndResetBacktrackRequest()`
`void`	`checkAndResetProbeRequest()` this does the actual notification and resets the request, hence this call should only happen from within JPFs main thread
`protected boolean`	`checkPropertyViolation()`
`boolean`	`checkStateSpaceLimit()` check if we have a minimum amount of free memory left.
`void`	`cleanUp()` called after the JPF run is finished.
`void`	`error(Property property)`
`void`	`error(Property property, Path path, ThreadList threadList)`
`protected boolean`	`forward()`
`Config`	`getConfig()`
`Error`	`getCurrentError()`
`int`	`getDepth()`
`int`	`getDepthLimit()`
`java.util.List<Error>`	`getErrors()`
`Error`	`getLastError()`
`java.lang.String`	`getLastSearchConstraint()`
`<T> T`	`getNextListenerOfType(java.lang.Class<T> type, T prev)`
`int`	`getNumberOfErrors()`
`protected java.util.ArrayList<Property>`	`getProperties(Config config)` return set of configured properties note there is a name clash here - JPF 'properties' have nothing to do with Java properties (java.util.Properties)
`int`	`getPurgedStateId()`
`java.lang.String`	`getSearchConstraint()`
`protected SearchState`	`getSearchState()`
`int`	`getStateDepth(int stateId)`
`int`	`getStateId()`
`Transition`	`getTransition()`
`VM`	`getVM()`
`boolean`	`hasErrors()`
`boolean`	`hasListenerOfType(java.lang.Class<?> listenerCls)`
`boolean`	`hasNextState()`
`protected boolean`	`hasPropertyTermination()`
`protected void`	`initialize(Config conf)`
`boolean`	`isDone()`
`boolean`	`isEndState()`
`boolean`	`isErrorState()`
`boolean`	`isIgnoredState()`
`boolean`	`isNewState()`
`boolean`	`isProcessedState()`
`boolean`	`isVisitedState()`
`protected void`	`notifyPropertyViolated()`
`void`	`notifySearchConstraintHit(java.lang.String details)`
`protected void`	`notifySearchFinished()`
`void`	`notifySearchProbed()`
`protected void`	`notifySearchStarted()`
`protected void`	`notifyStateAdvanced()`
`protected void`	`notifyStateBacktracked()`
`protected void`	`notifyStateProcessed()`
`protected void`	`notifyStatePurged()`
`protected void`	`notifyStateRestored()`
`protected void`	`notifyStateStored()`
`void`	`probeSearch()` request a probe This does not do the actual listener notification, it only stores the request, which is then processed from within JPFs inner execution loop.
`void`	`removeListener(SearchListener removeListener)`
`void`	`removeProperty(Property oldProperty)`
`boolean`	`requestBacktrack()` this is somewhat redundant to SystemState.setIgnored(), but we don't want to mix the case of overriding state matching with backtracking when searching for multiple errors
`void`	`resetProperties()`
`protected void`	`restoreState(State state)`
`abstract void`	`search()`
`void`	`setDepthLimit(int limit)`
`void`	`setIgnoredState(boolean cond)`
`void`	`setReporter(Reporter reporter)`
`protected void`	`setStateDepth(int stateId, int depth)`
`boolean`	`supportsBacktrack()`
`boolean`	`supportsRestoreState()`
`void`	`terminate()` this can be used by listeners to terminate the search
`boolean`	`transitionOccurred()`

Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

log
```
protected static JPFLogger log
```

currentError
```
protected Error currentError
```
error encountered during last transition, null otherwise

errors

protected java.util.ArrayList<Error> errors

depth
```
protected int depth
```

vm
```
protected VM vm
```

properties

protected java.util.ArrayList<Property> properties

matchDepth
```
protected boolean matchDepth
```

minFreeMemory
```
protected long minFreeMemory
```

depthLimit
```
protected int depthLimit
```

getAllErrors
```
protected boolean getAllErrors
```

lastSearchConstraint

protected java.lang.String lastSearchConstraint

done
```
protected boolean done
```

doBacktrack
```
protected boolean doBacktrack
```

notifyProbeListeners

protected java.util.concurrent.atomic.AtomicBoolean notifyProbeListeners

listeners
```
protected SearchListener[] listeners
```
search listeners. We keep them in a simple array to avoid creating objects on each notification

reporter
```
protected Reporter reporter
```
this is a special SearchListener that is always notified last, so that PublisherExtensions can be sure the notification has been processed by all listeners

config
```
protected final Config config
```

stateDepth
```
protected final IntVector stateDepth
```
storage to keep track of state depths

Constructor Detail

Search

protected Search(Config config,
                 VM vm)

Method Detail

initialize

protected void initialize(Config conf)

cleanUp
```
public void cleanUp()
```
called after the JPF run is finished. Shouldn't be public, but is called by JPF

getConfig
```
public Config getConfig()
```

search
```
public abstract void search()
```

setReporter

public void setReporter(Reporter reporter)

addListener

public void addListener(SearchListener newListener)

hasListenerOfType

public boolean hasListenerOfType(java.lang.Class<?> listenerCls)

getNextListenerOfType

public <T> T getNextListenerOfType(java.lang.Class<T> type,
                                   T prev)

removeListener

public void removeListener(SearchListener removeListener)

addProperty

public void addProperty(Property newProperty)

removeProperty

public void removeProperty(Property oldProperty)

getProperties
```
protected java.util.ArrayList<Property> getProperties(Config config)
```
return set of configured properties note there is a name clash here - JPF 'properties' have nothing to do with Java properties (java.util.Properties)

hasPropertyTermination

protected boolean hasPropertyTermination()

checkPropertyViolation

protected boolean checkPropertyViolation()

getErrors

public java.util.List<Error> getErrors()

getNumberOfErrors
```
public int getNumberOfErrors()
```

getLastSearchConstraint

public java.lang.String getLastSearchConstraint()

probeSearch
```
public void probeSearch()
```
request a probe This does not do the actual listener notification, it only stores the request, which is then processed from within JPFs inner execution loop. As a consequence, probeSearch() can be called async, and searchProbed() listeners don't have to bother with synchronization or inconsistent JPF states (notification happens from within JPFs main thread after a completed Instruction execution)

checkAndResetProbeRequest
```
public void checkAndResetProbeRequest()
```
this does the actual notification and resets the request, hence this call should only happen from within JPFs main thread

getCurrentError
```
public Error getCurrentError()
```
Returns:

error encountered during *last* transition (null otherwise)

getLastError
```
public Error getLastError()
```

hasErrors
```
public boolean hasErrors()
```

getVM
```
public VM getVM()
```

isEndState
```
public boolean isEndState()
```

isErrorState
```
public boolean isErrorState()
```

hasNextState
```
public boolean hasNextState()
```

transitionOccurred
```
public boolean transitionOccurred()
```

isNewState
```
public boolean isNewState()
```

isVisitedState
```
public boolean isVisitedState()
```

isIgnoredState
```
public boolean isIgnoredState()
```

isProcessedState
```
public boolean isProcessedState()
```

isDone
```
public boolean isDone()
```

getDepth
```
public int getDepth()
```

getSearchConstraint

public java.lang.String getSearchConstraint()

getTransition
```
public Transition getTransition()
```

getStateId
```
public int getStateId()
```

getPurgedStateId
```
public int getPurgedStateId()
```

requestBacktrack
```
public boolean requestBacktrack()
```
this is somewhat redundant to SystemState.setIgnored(), but we don't want to mix the case of overriding state matching with backtracking when searching for multiple errors

checkAndResetBacktrackRequest

protected boolean checkAndResetBacktrackRequest()

supportsBacktrack
```
public boolean supportsBacktrack()
```

supportsRestoreState
```
public boolean supportsRestoreState()
```

getDepthLimit
```
public int getDepthLimit()
```

setDepthLimit
```
public void setDepthLimit(int limit)
```

getSearchState

protected SearchState getSearchState()

error
```
public void error(Property property)
```

error

public void error(Property property,
                  Path path,
                  ThreadList threadList)

resetProperties
```
public void resetProperties()
```

notifyStateAdvanced
```
protected void notifyStateAdvanced()
```

notifyStateProcessed
```
protected void notifyStateProcessed()
```

notifyStateStored
```
protected void notifyStateStored()
```

notifyStateRestored
```
protected void notifyStateRestored()
```

notifyStateBacktracked

protected void notifyStateBacktracked()

notifyStatePurged
```
protected void notifyStatePurged()
```

notifySearchProbed
```
public void notifySearchProbed()
```

notifyPropertyViolated

protected void notifyPropertyViolated()

notifySearchStarted
```
protected void notifySearchStarted()
```

notifySearchConstraintHit

public void notifySearchConstraintHit(java.lang.String details)

notifySearchFinished
```
protected void notifySearchFinished()
```

forward
```
protected boolean forward()
```

backtrack
```
protected boolean backtrack()
```

setIgnoredState

public void setIgnoredState(boolean cond)

restoreState

protected void restoreState(State state)

terminate
```
public void terminate()
```
this can be used by listeners to terminate the search

setStateDepth

protected void setStateDepth(int stateId,
                             int depth)

getStateDepth

public int getStateDepth(int stateId)

checkStateSpaceLimit
```
public boolean checkStateSpaceLimit()
```
check if we have a minimum amount of free memory left. If not, we rather want to stop in time (with a threshold amount left) so that we can report something useful, and not just die silently with a OutOfMemoryError (which isn't handled too gracefully by most VMs)

Class Search

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Field Detail

log

currentError

errors

depth

vm

properties

matchDepth

minFreeMemory

depthLimit

getAllErrors

lastSearchConstraint

done

doBacktrack

notifyProbeListeners

listeners

reporter

config

stateDepth

Constructor Detail

Search

Method Detail

initialize

cleanUp

getConfig

search

setReporter

addListener

hasListenerOfType

getNextListenerOfType

removeListener

addProperty

removeProperty

getProperties

hasPropertyTermination

checkPropertyViolation

getErrors

getNumberOfErrors

getLastSearchConstraint

probeSearch

checkAndResetProbeRequest

getCurrentError

getLastError

hasErrors

getVM

isEndState

isErrorState

hasNextState

transitionOccurred

isNewState

isVisitedState

isIgnoredState

isProcessedState

isDone

getDepth

getSearchConstraint

getTransition

getStateId

getPurgedStateId

requestBacktrack

checkAndResetBacktrackRequest

supportsBacktrack

supportsRestoreState

getDepthLimit

setDepthLimit

getSearchState

error

error

resetProperties

notifyStateAdvanced

notifyStateProcessed

notifyStateStored

notifyStateRestored

notifyStateBacktracked

notifyStatePurged