Refined and expanded the javadoc for SearchListener.java and SearchListenerAdapter...

Fixed up some of the spelling mistakes in the documentation for SearchListener.java. Added verbosity to the documentation for the class and method descriptions as well as extra details regarding each method and its usage.

diff --git a/src/main/gov/nasa/jpf/search/SearchListener.java b/src/main/gov/nasa/jpf/search/SearchListener.java
index c137ecc010d8a71814d9f7f4ca53299cbc9f4db7..12dc691112f6763a76cf62e696374299bf6fdf06 100644 (file)
--- a/src/main/gov/nasa/jpf/search/SearchListener.java
+++ b/src/main/gov/nasa/jpf/search/SearchListener.java
@@ -20,72 +20,156 @@ package gov.nasa.jpf.search;
 import gov.nasa.jpf.JPFListener;
 
 /**
 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.
+ * 
+ * <p>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.
+ * 
+ *  <p>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 {
 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.)
+        * 
+        * <p>{@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.)
+        * 
+        * <p>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.)
+        * 
+        * <p>The restored state is guaranteed to have been visited and explored in the past. 
+        * 
+        * <p>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.)
+        * 
+        * <p>Notification of {@code stateAdvanced(Search search)} will always precede notifications of 
+        * {@code propertyViolated(Search search)}
+        * 
+        * <p>The JPF search loop will notify {@code SearchListener} of the property violation before resetting the violation
+        * 
+        * <p>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.)
+        * 
+        * <p>{@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.)
+        * 
+        * <p>The constraint being reached may have also been turned into a property but is usually an attribute of the search, not the application.
+        * 
+        * <p>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.)
+        * 
+        * <p>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 1493336152728263ea6a41b74499121afe9c6387..9f46462d463628b5b681320882a7aaa3553dcb36 100644 (file)
--- 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;
 
 /**
 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.
+ * 
+ * <p>Any desired methods will require implementing logic in child classes, however unwanted methods can be left uninstantiated in order to aid in
+ * code readability.
+ * 
+ *  <p>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 {
 
  */
 public class SearchListenerAdapter implements SearchListener {