The main purpose of the {@code Search} class is to track general search information such as depth, configured properties, + * errors, etc. as well as to define how the search algorithm functions. In its simplest form, a search algorithm can be defined + * using the abstract method {@code search} with a series of {@code forward} and {@code backtrack}. More complex search + * algorithms can also make use of the state storing functionality of the {@code Search} class, as well as ignoring states and + * removing states from the search tree. + * + *
Another very important aspect of the {@code Search} class is not only to implement search algorithms, but also to define + * the information that describes the current search loop. This is crucial in order to enable the {@code SearchListener} and + * {@code SearchListenerAdapter} classes responsible for extracting crucial data from the search loop during its verification + * efforts. */ public abstract class Search { + /** The {@code JPFLogger} object assigned to the {@code gov.nasa.jpf.search} subsystem + * @see gov.nasa.jpf.util.JPFLogger + */ protected static JPFLogger log = JPF.getLogger("gov.nasa.jpf.search"); - /** error encountered during last transition, null otherwise */ + /** The value of {@code currentError} will either be the error encountered during last + * transition or null if no error was encountered */ protected Error currentError = null; + + /** A running list of all errors encountered during verification. The list will always + * contain the current and past values of {@code currentError}. Errors are set added + * during verification in the {@code error} + * method. + * + *
{@code errors} will only hold one error before verification stops unless {@code getAllErrors}
+ * is set to true
+ *
+ * @see #error(Property, Path, ThreadList)
+ * @see #getAllErrors
+ */
protected ArrayList The default value for {@code minFreeMemory} is 1024 << 10 bytes. */
protected long minFreeMemory;
+ /** A property set by the user to define what the maximum depth allowed during verification is.
+ *
+ * By default the value is set to {@code Integer.MAX_VALUE}*/
protected int depthLimit;
+
+ /** A property set by the user to define whether to halt execution after encountering the first error during verification.
+ * If {@code getAllErrors} is set to true, verification will not stop after the first error, and every possible error
+ * during verification will be logged as a result. */
protected boolean getAllErrors;
- // message explaining the last search constraint hit
+ /** A {@code String} set to contain details on what the constraint that caused verification to halt was. Will generally be
+ * used by the {@code searchContraintHit} methods in {@code SearchListeners}.
+ *
+ * @see gov.nasa.jpf.search.SearchListener#searchConstraintHit(Search) */
protected String lastSearchConstraint;
- // these states control the search loop
+ /** {@code done} is a flag set during verification to notify the search loop when verification has finished. */
protected boolean done = false;
+ /** {@code doBacktrack} is a flag set during verification in order to request that the search loop backtracks
+ * one state.*/
protected boolean doBacktrack = false;
- // do we have a probe request
+ /** {@code notifyProbeListeners} is a flag set during verification stating whether or not a probe has been
+ * requested. When a probe is requested, relevant {@code SearchListeners} will be notified via {@code checkAndResetProbeRequest}*/
protected AtomicBoolean notifyProbeListeners = new AtomicBoolean(false);
- /** search listeners. We keep them in a simple array to avoid
+ /** {@code listeners} is an array used to hold {@code SearchListener} objects. We keep them in a simple array to avoid
creating objects on each notification */
protected SearchListener[] listeners = new SearchListener[0];
- /** this is a special SearchListener that is always notified last, so that
- * PublisherExtensions can be sure the notification has been processed by all listeners */
+ /** {@code reporter} is a special listener that is always notified last in order to ensure all other listeners have been notified
+ * beforehand. {@code reporter} is used to report information about the search loop to whichever output method the user has
+ * specified.
+ *
+ * By default, the output method is to console.*/
protected Reporter reporter;
- protected final Config config; // to later-on access settings that are only used once (not ideal)
+ /** {@code config} is an object passed in during instantiation of the {@code Search} object and it specifies the properties and
+ * configurations the search loop should run under. The value behind {@code config} is only ever used once and stored within this
+ * object.*/
+ protected final Config config;
- // don't forget to unregister or we have a HUGE memory leak if the same Config object is
- // reused for several JPF runs
+ /**
+ * {@code ConfigListener} is an implementation of the interface {@code ConfigChangeListener} and is used to subscribe to changes
+ * that occur to the configuration of JPF in order to update the {@code config} object. While highly useful, one should always
+ * remember to unregister the {@code config} object from each {@code ConfigListener} once it is no longer needed. Failure to
+ * do this will cause massive memory leaks to begin piling up as a result of the same {@code Config} object being used across
+ * several JPF executions.
+ *
+ */
class ConfigListener implements ConfigChangeListener {
@Override
@@ -109,9 +172,19 @@ public void jpfRunTerminated (Config config){
}
}
- /** storage to keep track of state depths */
+ /** {@code stateDepth} is an int vector storage system (akin to a map) that is responsible for associating states with their
+ * corresponding depths.
+ *
+ * {@code stateDepth} maps the state id of every state to the corresponding depth, in a one to one mapping.*/
protected final IntVector stateDepth = new IntVector();
+ /**
+ * Constructs a {@code Search} object using the configuration specified by the user in {@code config} and a virtual machine
+ * that will be used for verification.
+ *
+ * @param config The configuration and properties that the search loop will be required to commence verification under
+ * @param vm The virtual machine that the search loop will traverse and verify states from
+ */
protected Search (Config config, VM vm) {
this.vm = vm;
this.config = config;
@@ -126,6 +199,12 @@ protected Search (Config config, VM vm) {
config.addChangeListener( new ConfigListener());
}
+ /**
+ * Initializes the properties that the search loop will need to run under in order to make sure that each iteration of the search
+ * loop is in compliance with the properties set by JPF and the user.
+ *
+ * @param conf The configuration object ({@code config}) that contains the necessary information to initialize the property values
+ */
protected void initialize( Config conf){
depthLimit = conf.getInt("search.depth_limit", Integer.MAX_VALUE);
matchDepth = conf.getBoolean("search.match_depth");
@@ -134,53 +213,103 @@ protected void initialize( Config conf){
}
/**
- * called after the JPF run is finished. Shouldn't be public, but is called by JPF
+ * Called after the JPF run is finished. Should not be public, but is called by JPF
*/
public void cleanUp(){
// nothing here, the ConfigListener removes itself
}
+ /**
+ * Returns the {@code config} object that is used by the {@code Search} class.
+ *
+ * @return The configuration object that is used for verification
+ */
public Config getConfig() {
return config;
}
+ /**
+ * One of the most important methods in the {@code Search} class. {@code search} is used to specify what the algorithm and behavior
+ * for verification are. When the term "search loop" is brought up in other documentation, it generally means the loop that is used
+ * running in the {@code search} method.
+ */
public abstract void search ();
+ /**
+ * Sets the {@code reporter} object used during verification to the specified {@code reporter}.
+ *
+ * @param reporter The reporter used to replace the current reporter object in the {@code Search} class
+ */
public void setReporter(Reporter reporter){
this.reporter = reporter;
}
+ /**
+ * Appends a {@code SearchListener} object to the {@code listener} array. In addition to appending the search listener, the action is also logged
+ * to the JPFLog {@code log} used in the {@code Search} class.
+ *
+ * @param newListener A new {@code SearchListener} to append to the {@code listener} array
+ */
public void addListener (SearchListener newListener) {
log.info("SearchListener added: ", newListener);
listeners = Misc.appendElement(listeners, newListener);
}
+ /**
+ * Checks whether a listener of the same type as {@code listenerCls} exists in {@code listeners} already.
+ *
+ * @param listenerCls The object type to check {@code listeners} against
+ * @return true if an element of the same type as the input parameter exists in {@code listeners}. False otherwise
+ */
public boolean hasListenerOfType (Class listenerCls) {
return Misc.hasElementOfType(listeners, listenerCls);
}
+ /**
+ * Returns the next element in {@code listeners} after the element matching {@code prev} that is of the same type as {@code type}.
+ *
+ * @param type The type of element to search for and return
+ * @param prev The previous element to begin the search from
+ * @return An element of the same class as {@code type} and coming after {@code prev} in the {@code listeners} array
+ */
public Note there is a name clash here - JPF 'properties' have nothing to do with Java properties (java.util.Properties)
+ *
+ * @param config The config object to retrieve the properties list from
+ * @return The list of configured properties
*/
protected ArrayList This does not perform 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
+ * As a consequence, {@code probeSearch} can be called asynchronously, and {@code 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)
*/
@@ -243,8 +397,7 @@ public void probeSearch(){
}
/**
- * this does the actual notification and resets the request, hence this call
- * should only happen from within JPFs main thread
+ * Performs the actual notification and resets the request, hence this call should only happen from within JPFs main thread
*/
public void checkAndResetProbeRequest(){
if (notifyProbeListeners.compareAndSet(true, false)){
@@ -253,12 +406,19 @@ public void checkAndResetProbeRequest(){
}
/**
- * @return error encountered during *last* transition (null otherwise)
+ * Returns the most recent error encountered during the last transition
+ *
+ * @return The error encountered during the last transition or null if none was encountered
*/
public Error getCurrentError(){
return currentError;
}
+ /**
+ * Returns the most recent error encountered in the past
+ *
+ * @return The most recent error encountered in the past or none if no error has been encountered during verification
+ */
public Error getLastError() {
int i=errors.size()-1;
if (i >=0) {
@@ -268,30 +428,69 @@ public Error getLastError() {
}
}
+ /**
+ * Returns whether or not the search loop has encountered an error yet
+ *
+ * @return true if an error has been encountered, false otherwise
+ */
public boolean hasErrors(){
return !errors.isEmpty();
}
+ /**
+ * Returns the {@code vm} object used by the search loop
+ *
+ * @return the {@code vm} object used by {@code Search}
+ */
public VM getVM() {
return vm;
}
+ /**
+ * Returns true if the search loop has transitioned into an end state in the virtual machine
+ *
+ * @return true if the current state of the {@code vm} is an end state
+ */
public boolean isEndState () {
return vm.isEndState();
}
+ /**
+ * Returns if an error has been encountered during the transition into the current state
+ *
+ * @return true if an error has been encountered during the most recent transition, false otherwise
+ */
public boolean isErrorState(){
return (currentError != null);
}
+ /**
+ * Returns whether of not the current state is an end state in the virtual machine
+ *
+ * @return true if this is not an end state of the {@code vm}, false otherwise
+ */
public boolean hasNextState () {
return !isEndState();
}
+ /**
+ * Returns whether a transition has occurred from the previous state or not
+ *
+ * @return true if a transition has occurred, false otherwise
+ */
public boolean transitionOccurred(){
return vm.transitionOccurred();
}
+ /**
+ * Returns whether the current state in the search loop is a new state and false otherwise.
+ *
+ * However, if {@code matchDepth} is set to true,
+ * then it will true if the state is new or if the states depth is less than the previously recorded depth. If the state is new, the states
+ * depth will also be recorded for future use.
+ *
+ * @return true if the current state is a new state and false otherwise (behaviour changes if {@code matchDepth} is true
+ */
public boolean isNewState () {
boolean isNew = vm.isNewState();
@@ -308,53 +507,111 @@ public boolean isNewState () {
return isNew;
}
+ /**
+ * Returns whether the current state has been visited yet. The opposite of {@code isNewState}
+ *
+ * @return true if the state has been visited, false otherwise (behavior changes if {@code matchDepth} is true)
+ * @see #isNewState()
+ */
public boolean isVisitedState () {
return !isNewState();
}
+ /**
+ * Returns whether the current state is an ignored state in the virtual machine
+ *
+ * @return true if the current state is an ignored state, false otherwise
+ */
public boolean isIgnoredState(){
return vm.isIgnoredState();
}
+ /**
+ * Returns whether the current state has been fully explored by the search loop.
+ *
+ * @return true if the current state has been fully explored and processed, false otherwise
+ */
public boolean isProcessedState(){
return vm.getChoiceGenerator().isProcessed();
}
+ /**
+ * Return whether the search loop has finished verification
+ *
+ * @return true if the search loop has finished verification, false otherwise
+ */
public boolean isDone(){
return done;
}
+ /**
+ * Return the current depth of the search loop
+ *
+ * @return The current depth inside the search tree.
+ */
public int getDepth () {
return depth;
}
+ /**
+ * Returns the most recent search constraint that was encountered
+ *
+ * @return A String detailing the most recent search constraint that was encountered
+ */
public String getSearchConstraint () {
return lastSearchConstraint;
}
+ /**
+ * Returns the most recent transition that has occurred
+ *
+ * @return The last transition that occurred during verification, or null if none has occurred
+ */
public Transition getTransition () {
return vm.getLastTransition();
}
+ /**
+ * Returns the state id of the current state
+ *
+ * @return The state id of the current state
+ */
public int getStateId () {
return vm.getStateId();
}
+ /**
+ * Returns the purged states id
+ *
+ * Note that while it should return the purged states id, it currently only returns -1 as a
+ * result of many searches not utilizing this functionality. If it is required, {@code getPurgedStateId}
+ * should be overridden and changed in subsequent child classes.
+ *
+ * @return The purged states id (currently only returns -1)
+ */
public int getPurgedStateId () {
return -1; // a lot of Searches don't purge any states
}
/**
- * this is somewhat redundant to SystemState.setIgnored(), but we don't
+ * Requests that the search loop backtracks one step
+ *
+ * This is somewhat redundant to {@code SystemState.setIgnored}, but we don't
* want to mix the case of overriding state matching with backtracking when
- * searching for multiple errors
+ * searching for multiple errors.
+ *
+ * @return The value of {@code doBacktrack} after is has been set to true (i.e. always true)
*/
public boolean requestBacktrack () {
return doBacktrack = true;
}
-
+ /**
+ * Returns the value of {@code doBacktrack} as well as resetting {@code doBacktrack} to false
+ *
+ * @return the value of {@code doBackTrack}
+ */
protected boolean checkAndResetBacktrackRequest() {
if (doBacktrack){
doBacktrack = false;
@@ -364,32 +621,82 @@ protected boolean checkAndResetBacktrackRequest() {
}
}
+ /**
+ * Returns whether the search algorithm supports backtracking or not
+ *
+ * @return true if the search algorithm supports backtracking, false otherwise (by default the return
+ * is true unless overridden)
+ */
public boolean supportsBacktrack () {
return true;
}
+ /**
+ * Returns whether the search algorithm supports restoring states that have been stored (a useful method in
+ * BreadthFirstSearch)
+ *
+ * @return true if the search algorithm supports restoring states, false otherwise (by default the return
+ * is false as the function is unsupported)
+ */
public boolean supportsRestoreState () {
// not supported by default
return false;
}
+ /**
+ * Returns the depth limit set at the beginning of verification
+ *
+ * @return The {@code depthLimit} property
+ */
public int getDepthLimit () {
return depthLimit;
}
+ /**
+ * Sets a new value for the {@code depthLimit} property
+ *
+ * @param limit The new limit to set {@code depthLimit} to
+ */
public void setDepthLimit(int limit){
depthLimit = limit;
}
+ /**
+ * Returns a {@code SearchState} object with information describing the current state in the search loop
+ *
+ * @return A {@code SearchState} object with information about the current state
+ */
protected SearchState getSearchState () {
return new SearchState(this);
}
- // can be used by SearchListeners to create path-less errors (liveness)
+ /**
+ * Creates a new error with the corresponding {@code Property} that causes the error. Does not provide a {@code Path} or {@code ThreadList}, and
+ * can therefore be used by {@code SearchListeners} to create path-less errors to ensure liveness.
+ *
+ * @param property the property that caused the error
+ * @see #error(Property, Path, ThreadList)
+ */
public void error (Property property) {
error(property, null, null);
}
+ /**
+ * Creates an error with the corresponding {@code Property} that causes the error, alongside the {@code Path}, and {@code ThreadList}.
+ *
+ * Will set {@code done} to true and halt the search loop if {@code getAllErrors} is false. If {@code getAllErrors} is true, it will
+ * clone the {@code Property}, {@code Path}, and {@code ThreadList} objects that were passed in (as not cloning them may cause subsequent
+ * operations to overwrite information still in use) and add them to the {@code errors} list
+ * and continue verification.
+ *
+ * The property that caused the error is not reset here as the listeners attached to the search should be notified of the error first.
+ * This becomes especially problematic if one of the listeners caused the property violation, as which point it would get confused
+ * if the {@code propertyViolated()} notification happens after the property is reset.
+ *
+ * @param property The property that causes the error
+ * @param path The path corresponding to the error
+ * @param threadList The list of thread information corresponding to the error
+ */
public void error (Property property, Path path, ThreadList threadList) {
if (getAllErrors) {
@@ -411,17 +718,20 @@ public void error (Property property, Path path, ThreadList threadList) {
errors.add(currentError);
- // we should not reset the property until listeners have been notified
- // (the listener might be the property itself, in which case it could get
- // confused if propertyViolated() notifications happen after a reset)
}
+ /**
+ * Resets all properties, returning violated properties to their default states.
+ */
public void resetProperties(){
for (Property p : properties) {
p.reset();
}
}
+ /**
+ * Notifies the {@code SearchListener} objects in the {@code listeners} list that the search loop has advanced states.
+ */
protected void notifyStateAdvanced () {
try {
for (int i = 0; i < listeners.length; i++) {
@@ -436,6 +746,10 @@ protected void notifyStateAdvanced () {
}
}
+ /**
+ * Notifies the {@code SearchListener} objects in the {@code listeners} list that the search loop has finished processing
+ * the current state.
+ */
protected void notifyStateProcessed() {
try {
for (int i = 0; i < listeners.length; i++) {
@@ -449,6 +763,9 @@ protected void notifyStateProcessed() {
}
}
+ /**
+ * Notifies the {@code SearchListener} objects in the {@code listeners} list that the search loop has stored the current state.
+ */
protected void notifyStateStored() {
try {
for (int i = 0; i < listeners.length; i++) {
@@ -462,6 +779,10 @@ protected void notifyStateStored() {
}
}
+ /**
+ * Notifies the {@code SearchListener} objects in the {@code listeners} list that the search loop has restored a currently
+ * stored state.
+ */
protected void notifyStateRestored() {
try {
for (int i = 0; i < listeners.length; i++) {
@@ -475,6 +796,10 @@ protected void notifyStateRestored() {
}
}
+ /**
+ * Notifies the {@code SearchListener} objects in the {@code listeners} list that the search loop has backtracked to a
+ * previous state.
+ */
protected void notifyStateBacktracked() {
try {
for (int i = 0; i < listeners.length; i++) {
@@ -488,6 +813,9 @@ protected void notifyStateBacktracked() {
}
}
+ /**
+ * Notifies the {@code SearchListener} objects in the {@code listeners} list that the search loop has purged the current state.
+ */
protected void notifyStatePurged() {
try {
for (int i = 0; i < listeners.length; i++) {
@@ -501,6 +829,10 @@ protected void notifyStatePurged() {
}
}
+ /**
+ * Notifies the {@code SearchListener} objects in the {@code listeners} list that a probe request has been triggered during
+ * verification.
+ */
public void notifySearchProbed() {
try {
for (int i = 0; i < listeners.length; i++) {
@@ -515,6 +847,10 @@ public void notifySearchProbed() {
}
+ /**
+ * Notifies the {@code SearchListener} objects in the {@code listeners} list that the search loop has encountered a property
+ * violation
+ */
protected void notifyPropertyViolated() {
try {
for (int i = 0; i < listeners.length; i++) {
@@ -533,6 +869,9 @@ protected void notifyPropertyViolated() {
}
}
+ /**
+ * Notifies the {@code SearchListener} objects in the {@code listeners} list that the search loop has begun verification.
+ */
protected void notifySearchStarted() {
try {
for (int i = 0; i < listeners.length; i++) {
@@ -546,6 +885,13 @@ protected void notifySearchStarted() {
}
}
+ /**
+ * Notifies the {@code SearchListener} objects in the {@code listeners} list that the search loop has encountered a
+ * search constraint. The {@code details} String outlines the search constraint that was hit as well as any other
+ * relevant information.
+ *
+ * @param details Information regarding the recent search constraint that was encountered.
+ */
public void notifySearchConstraintHit(String details) {
try {
lastSearchConstraint = details;
@@ -560,6 +906,9 @@ public void notifySearchConstraintHit(String details) {
}
}
+ /**
+ * Notifies the {@code SearchListener} objects in the {@code listeners} list that the search loop has finished verification.
+ */
protected void notifySearchFinished() {
try {
for (int i = 0; i < listeners.length; i++) {
@@ -573,6 +922,15 @@ protected void notifySearchFinished() {
}
}
+ /**
+ * Requests that the virtual machine move to the next unvisited state below the current one in the search tree.
+ * {@code forward} along with {@code backtrack} constitute the two methods that are generally used to advance
+ * the search algorithm during verification.
+ *
+ * @return true if a state exists and the virtual machine can move to it, false if the state does not exist
+ * or if it was previously explored.
+ * @see #backtrack()
+ */
protected boolean forward () {
currentError = null;
@@ -581,28 +939,76 @@ protected boolean forward () {
checkPropertyViolation();
return ret;
}
-
+
+ /**
+ * Requests that the virtual machine move to the previous state in the search tree. {@code backtrack} along
+ * with {@code forward} constitute the two methods that are generally used to advance the search algorithm
+ * during verification.
+ *
+ * @return true if the backtrack to the previous state was successful, false otherwise
+ */
protected boolean backtrack () {
return vm.backtrack();
}
+ /**
+ * Requests that the virtual machine sets whether the current state should be ignored in all future iterations
+ * of the search loop. This should not be used without cause as it causes the search tree to be pruned whenever
+ * it is called, which is expensive, especially in larger trees.
+ *
+ * @param cond Whether or not the current state should be ignored
+ */
public void setIgnoredState (boolean cond) {
vm.ignoreState(cond);
}
+ /**
+ * Restores a previously stored virtual machine state.
+ *
+ * By default this method is not supported, and therefore requires implementation logic in child classes.
+ *
+ * @param state The stored state to be restored
+ */
protected void restoreState (State state) {
// not supported by default
}
- /** this can be used by listeners to terminate the search */
+ /**
+ * Sets {@code done} to true in order to terminate the search loop.
+ *
+ * Can be used by listeners to terminate the search.
+ *
+ */
public void terminate () {
done = true;
}
+ /**
+ * Sets the depth of the specified state given its state id.
+ *
+ * When the depth of the state is set, it is set as depth + 1. This is to differentiate between
+ * states that have had their depths set, and states that have not (in which case their default depth
+ * will be 0).
+ *
+ * @param stateId The state in question
+ * @param depth The new depth to set for the state
+ */
protected void setStateDepth (int stateId, int depth) {
stateDepth.set(stateId, depth + 1);
}
+
+ /**
+ * Returns the saved depth of the specified state given its state id.
+ *
+ * If the state in question has not had its state depth set previously, then it will by default have
+ * a depth that is less than or equal to 0. Otherwise if the state has been visited, the depth will be
+ * returned.
+ *
+ * @param stateId The state to return the depth of
+ * @return The depth of the specified state
+ * @throws JPFException If the state has not been visited in the past
+ */
public int getStateDepth (int stateId) {
int depthPlusOne = stateDepth.get(stateId);
if (depthPlusOne <= 0) {
@@ -613,9 +1019,15 @@ public int getStateDepth (int stateId) {
}
/**
- * 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)
+ * Check if there is the minimum amount of free memory left or more. If not, we would rather stop in time
+ * (with a threshold amount left) in order to report something useful, and not just end verification silently
+ * with a OutOfMemoryError (which is not handled too gracefully by most VMs)
+ *
+ * If the minimum amount of memory has been reached, the method will first try to activate garbage collection
+ * and then check again if that made a difference. If the amount of memory available is still less than the
+ * minimum amount of memory, then we return false.
+ *
+ * @return true if we have more memory than the minimum free memory, false otherwise.
*/
public boolean checkStateSpaceLimit () {
Runtime rt = Runtime.getRuntime();
diff --git a/src/main/gov/nasa/jpf/search/SearchListener.java b/src/main/gov/nasa/jpf/search/SearchListener.java
index c137ecc0..12dc6911 100644
--- a/src/main/gov/nasa/jpf/search/SearchListener.java
+++ b/src/main/gov/nasa/jpf/search/SearchListener.java
@@ -20,72 +20,156 @@
import gov.nasa.jpf.JPFListener;
/**
- * interface to register for notification by the Search object.
- * Observer role in same-name pattern
+ * The {@code SearchListener} interface defines the methods available to register for notifications by the {@code Search} object.
+ *
+ * Any desired methods will require implementation logic in the child class, but unwanted methods can be instantiated without logic.
+ * {@code SearchListenerAdapter} instantiates all of the methods as an abstract class and does not require child classes to instantiate all methods.
+ * If the child class is not another {@code Listener} type interface, then {@code SearchListenerAdapter} would be a more appropriate parent class.
+ *
+ * This interface is to be used alongside classes that extend {@code Search} class functionality. {@code SearchListener} is capable of gauging
+ * {@code Search} attributes through the implemented methods and can receive information such as depth, configured properties, and other important {@code Search}
+ * properties.
*/
+
public interface SearchListener extends JPFListener {
-
- /**
- * got the next state
- * Note - this will be notified before any potential propertyViolated, in which
- * case the currentError will be already set
- */
- void stateAdvanced (Search search);
-
- /**
- * state is fully explored
- */
- void stateProcessed (Search search);
-
- /**
- * state was backtracked one step
- */
- void stateBacktracked (Search search);
- /**
- * some state is not going to appear in any path anymore
- */
- void statePurged (Search search);
+ /**
+ * Notified when the state in a {@code Search} child class is advanced forward
+ * one state in the search tree. The {@code Search} object that is passed as
+ * a parameter contains attributes describing the next state in the search
+ * loop as well as attributes describing the specifications of the search loop
+ * itself (e.g. current depth, depth limit, current error, etc.)
+ *
+ * {@code stateAdvanced(Search search)} will be notified and called before any potential
+ * property violations (in {@code propertyViolated(Search search)}, thus the currentError
+ * will already be set and may not reflect upcoming property violations.
+ *
+ * @param search a {@code Search} object that denotes current attributes in the next state
+ */
+ void stateAdvanced (Search search);
+
+ /**
+ * Notified when the search loop has fully explored the current state and is ready to move
+ * to a new state in the search tree. The {@code Search} object that is passed as a parameter
+ * contains attributes describing the current state in the search loop as well as attributes
+ * describing the specifications of the search loop itself (e.g. current depth, depth limit,
+ * current error, etc.)
+ *
+ * @param search a {@code Search} object that denotes current attributes in the current state
+ */
+ void stateProcessed (Search search);
+
+ /**
+ * Notified when the state in a {@code Search} child class is moved backwards
+ * one state in the search tree. The {@code Search} object that is passed as
+ * a parameter contains attributes describing the next state (which is also
+ * the previous state) in the search tree attributes as well as attributes
+ * describing the specifications of the search loop itself (e.g. current depth,
+ * depth limit, current error, etc.)
+ *
+ * @param search a {@code Search} object that denotes current attributes
+ * of the next (previous) state
+ */
+ void stateBacktracked (Search search);
+
+ /**
+ * Notified when a state is removed from the search tree and will not be appearing
+ * in the future. The {@code Search} object passed through contains details
+ * that describe the state and the current properties of the search loop
+ * (e.g. current depth, depth limit, current error, etc.)
+ *
+ * @param search a {@code Search} object that denotes current attributes of the purged state
+ */
+ void statePurged (Search search);
+
+ /**
+ * Notified when an explored state from the search state is stored to be accessed later. The
+ * {@code Search} object passed through contains details that describe the state and current
+ * properties of the search loop (e.g. current depth, depth limit, current error, etc.)
+ *
+ * The stored state may be restored later through {@code stateRestored(Search search)}
+ *
+ * @param search a {@code Search} object that denotes current attributes of the stored state
+ */
+ void stateStored (Search search);
+
+ /**
+ * Notified when a previously stored search state is restored for use in the search algorithm.
+ * The {@code Search} object passed through contains details that describe the restored state
+ * and current properties of the search loop (e.g. current depth, depth limit, current
+ * error, etc.)
+ *
+ * The restored state is guaranteed to have been visited and explored in the past.
+ *
+ * The restored state may be from a separate path than the previous state.
+ *
+ * @param search a {@code Search} object that denotes current attributes of the restored state
+ */
+ void stateRestored (Search search);
+
+ /**
+ * Notified when a probe request occurs (e.g. from a periodical timer). The {@code Search} object
+ * passed through contains details that describe the probe request, as well as the properties of
+ * the search loop (e.g. current depth, depth limit, current error, etc.)
+ *
+ * While probe requests in {@code Search} may be implemented and called asynchronously, the notification
+ * sent to {@code searchProbed(Search search)} will always be from the main JPF loop, and thus be synchronously
+ * called (i.e. after instruction execution).
+ *
+ * @param search a {@code Search} object that denotes current attributes of the probe request
+ */
+ void searchProbed (Search search);
+
+ /**
+ * Notified when JPF encounters a property violation of the application during the search loop. The
+ * {@code Search} object passed through contains details describing the properties of the search loop
+ * (e.g. current depth, depth limit, current error, etc.)
+ *
+ * Notification of {@code stateAdvanced(Search search)} will always precede notifications of
+ * {@code propertyViolated(Search search)}
+ *
+ * The JPF search loop will notify {@code SearchListener} of the property violation before resetting the violation
+ *
+ * Properties refers to jpf.Property and not java.util.Property
+ *
+ * @param search a {@code Search} object that denotes current attributes at the time of the property violation
+ */
+ void propertyViolated (Search search);
+
+ /**
+ * Notified when a search is started and the search loop is entered. The {@code Search} object passed through
+ * contains details describing the properties of the search loop (e.g. current depth, depth limit, current
+ * error, etc.)
+ *
+ * {@code searchStarted(Search search)} will always be called before the first {@code Search.forward()} call.
+ *
+ * @param search a {@code Search} object that denotes current attributes of search loop
+ */
+ void searchStarted (Search search);
+
+ /**
+ * Notified when a constraint is reached during the search loop. The {@code Search} object passed through contains details describing
+ * the properties of the search loop at the time of notification (e.g. current depth, depth limit, current error, etc.)
+ *
+ * The constraint being reached may have also been turned into a property but is usually an attribute of the search, not the application.
+ *
+ * Examples of constraints are depth limit or the amount of memory that the search loop is allowed to use being exceeded. These general constraints
+ * are usually specified in a properties file.
+ *
+ * @param search a {@code Search} object that denotes current attributes of search loop at the time of the constraint being hit
+ */
+ void searchConstraintHit (Search search);
- /**
- * somebody stored the state
- */
- void stateStored (Search search);
-
- /**
- * a previously generated state was restored
- * (can be on a completely different path)
- */
- void stateRestored (Search search);
-
- /**
- * there was a probe request, e.g. from a periodical timer
- * note this is called synchronously from within the JPF execution loop
- * (after instruction execution)
- */
- void searchProbed (Search search);
-
- /**
- * JPF encountered a property violation.
- * Note - this is always preceeded by a stateAdvanced
- */
- void propertyViolated (Search search);
-
- /**
- * we get this after we enter the search loop, but BEFORE the first forward
- */
- void searchStarted (Search search);
-
- /**
- * there was some contraint hit in the search, we back out
- * could have been turned into a property, but usually is an attribute of
- * the search, not the application
- */
- void searchConstraintHit (Search search);
-
- /**
- * we're done, either with or without a preceeding error
- */
- void searchFinished (Search search);
+ /**
+ * Notified when a search ends and the search loop is exited. The {@code Search} object passed through
+ * contains details describing the properties of the search loop and final state (e.g. current depth,
+ * depth limit, current error, etc.)
+ *
+ * If the search was finished prematurely due to some unexpected reason, a preceding error may antecede
+ * the {@code searchFinished(Search search)} call.
+ *
+ * @param search a {@code Search} object that denotes attributes of finalized search loop
+ */
+ void searchFinished (Search search);
}
diff --git a/src/main/gov/nasa/jpf/search/SearchListenerAdapter.java b/src/main/gov/nasa/jpf/search/SearchListenerAdapter.java
index 14933361..9f46462d 100644
--- a/src/main/gov/nasa/jpf/search/SearchListenerAdapter.java
+++ b/src/main/gov/nasa/jpf/search/SearchListenerAdapter.java
@@ -19,8 +19,14 @@
package gov.nasa.jpf.search;
/**
- * a no-action SearchListener which we can use to override only the
- * notifications we are interested in
+ * The {@code SearchListenerAdapter} abstract class instantiates the methods from {@code SearchListener} in order to create an adapter design pattern.
+ *
+ * Any desired methods will require implementing logic in child classes, however unwanted methods can be left uninstantiated in order to aid in
+ * code readability.
+ *
+ * This class is to be used alongside classes that extend {@code Search} class functionality. {@code SearchListenerAdapter} is capable of gauging
+ * Search attributes through the implemented methods and can receive information such as depth, configured properties, and other important {@code Search}
+ * attributes.
*/
public class SearchListenerAdapter implements SearchListener {