Updated Search.java documentation (#184)
[jpf-core.git] / src / main / gov / nasa / jpf / search / Search.java
1 /*
2  * Copyright (C) 2014, United States Government, as represented by the
3  * Administrator of the National Aeronautics and Space Administration.
4  * All rights reserved.
5  *
6  * The Java Pathfinder core (jpf-core) platform is licensed under the
7  * Apache License, Version 2.0 (the "License"); you may not use this file except
8  * in compliance with the License. You may obtain a copy of the License at
9  * 
10  *        http://www.apache.org/licenses/LICENSE-2.0. 
11  *
12  * Unless required by applicable law or agreed to in writing, software
13  * distributed under the License is distributed on an "AS IS" BASIS,
14  * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
15  * See the License for the specific language governing permissions and 
16  * limitations under the License.
17  */
18 package gov.nasa.jpf.search;
19
20 import gov.nasa.jpf.Config;
21 import gov.nasa.jpf.ConfigChangeListener;
22 import gov.nasa.jpf.Error;
23 import gov.nasa.jpf.JPF;
24 import gov.nasa.jpf.JPFException;
25 import gov.nasa.jpf.JPFListenerException;
26 import gov.nasa.jpf.Property;
27 import gov.nasa.jpf.State;
28 import gov.nasa.jpf.report.Reporter;
29 import gov.nasa.jpf.util.IntVector;
30 import gov.nasa.jpf.util.JPFLogger;
31 import gov.nasa.jpf.util.Misc;
32 import gov.nasa.jpf.vm.VM;
33 import gov.nasa.jpf.vm.Path;
34 import gov.nasa.jpf.vm.ThreadList;
35 import gov.nasa.jpf.vm.Transition;
36
37 import java.util.ArrayList;
38 import java.util.List;
39 import java.util.concurrent.atomic.AtomicBoolean;
40
41 /**
42  * The {@code Search} abstract class is at the heart of all search classes. Even when it is not extended by child classes, it will
43  * be embedded in the logic as an input for some of the methods. 
44  * 
45  * <p>The main purpose of the {@code Search} class is to track general search information such as depth, configured properties, 
46  * errors, etc. as well as to define how the search algorithm functions. In its simplest form, a search algorithm can be defined 
47  * using the abstract method {@code search} with a series of {@code forward} and {@code backtrack}. More complex search 
48  * algorithms can also make use of the state storing functionality of the {@code Search} class, as well as ignoring states and
49  * removing states from the search tree.
50  * 
51  * <p>Another very important aspect of the {@code Search} class is not only to implement search algorithms, but also to define
52  * the information that describes the current search loop. This is crucial in order to enable the {@code SearchListener} and 
53  * {@code SearchListenerAdapter} classes responsible for extracting crucial data from the search loop during its verification
54  * efforts.
55  */
56 public abstract class Search {
57   
58   /** The {@code JPFLogger} object assigned to the {@code gov.nasa.jpf.search} subsystem 
59    * @see gov.nasa.jpf.util.JPFLogger
60    */
61   protected static JPFLogger log = JPF.getLogger("gov.nasa.jpf.search");
62   
63   /** The value of {@code currentError} will either be the error encountered during last
64    *  transition or null if no error was encountered */
65   protected Error currentError = null;
66   
67   /** A running list of all errors encountered during verification. The list will always 
68    * contain the current and past values of {@code currentError}. Errors are set added
69    * during verification in the {@code error}
70    * method.
71    * 
72    * <p>{@code errors} will only hold one error before verification stops unless {@code getAllErrors}
73    * is set to true
74    * 
75    * @see #error(Property, Path, ThreadList)
76    * @see #getAllErrors
77    */
78   protected ArrayList<Error> errors = new ArrayList<Error>();
79
80   /**  {@code depth} represents the current depth of the search tree. */
81   protected int depth = 0;
82   /** {@code vm} represents the virtual machine that the search algorithm will be traversing*/
83   protected VM vm;
84
85   /** A list of properties provided from the search configuration at the start of verification. Every property has a {@code check}
86    * method that will be used during verification to tell if any of the properties have been violated.*/
87   protected ArrayList<Property> properties;
88
89   /** A property set by the user before verification. If {@code matchDepth} is true it will change the behavior of 
90    * {@code isNewState()}.
91    * @see #isNewState() */
92   protected boolean matchDepth;
93   /** A property set by the user to define what the minimum memory required to keep verifying is. The reason this is a non-zero
94    * value is to ensure some memory is left over to output a legible message before ending execution instead of simply throwing
95    * an {@code OutOfMemoryError}.
96    * 
97    * <p> The default value for {@code minFreeMemory} is 1024 << 10 bytes. */
98   protected long    minFreeMemory;
99   /** A property set by the user to define what the maximum depth allowed during verification is. 
100    * 
101    * <p>By default the value is set to {@code Integer.MAX_VALUE}*/
102   protected int     depthLimit;
103   
104   /** A property set by the user to define whether to halt execution after encountering the first error during verification.
105    * If {@code getAllErrors} is set to true, verification will not stop after the first error, and every possible error
106    * during verification will be logged as a result. */
107   protected boolean getAllErrors;
108
109   /** A {@code String} set to contain details on what the constraint that caused verification to halt was. Will generally be 
110    * used by the {@code searchContraintHit} methods in {@code SearchListeners}.
111    * 
112    * @see gov.nasa.jpf.search.SearchListener#searchConstraintHit(Search) */
113   protected String lastSearchConstraint;
114
115   /** {@code done} is a flag set during verification to notify the search loop when verification has finished. */
116   protected boolean done = false;
117   /** {@code doBacktrack} is a flag set during verification in order to request that the search loop backtracks
118    * one state.*/
119   protected boolean doBacktrack = false;
120
121  /** {@code notifyProbeListeners} is a flag set during verification stating whether or not a probe has been 
122   * requested. When a probe is requested, relevant {@code SearchListeners} will be notified via {@code checkAndResetProbeRequest}*/
123   protected AtomicBoolean notifyProbeListeners = new AtomicBoolean(false);
124
125   /** {@code listeners} is an array used to hold {@code SearchListener} objects. We keep them in a simple array to avoid
126    creating objects on each notification */
127   protected SearchListener[] listeners = new SearchListener[0];
128
129   /** {@code reporter} is a special listener that is always notified last in order to ensure all other listeners have been notified
130    * beforehand. {@code reporter} is used to report information about the search loop to whichever output method the user has 
131    * specified.
132    * 
133    *  <p>By default, the output method is to console.*/
134   protected Reporter reporter;
135
136   /** {@code config} is an object passed in during instantiation of the {@code Search} object and it specifies the properties and 
137    * configurations the search loop should run under. The value behind {@code config} is only ever used once and stored within this
138    * object.*/
139   protected final Config config;
140
141   /**
142    * {@code ConfigListener} is an implementation of the interface {@code ConfigChangeListener} and is used to subscribe to changes 
143    * that occur to the configuration of JPF in order to update the {@code config} object. While highly useful, one should always
144    * remember to unregister the {@code config} object from each {@code ConfigListener} once it is no longer needed. Failure to
145    * do this will cause massive memory leaks to begin piling up as a result of the same {@code Config} object being used across
146    * several JPF executions. 
147    *
148    */
149   class ConfigListener implements ConfigChangeListener {
150
151     @Override
152     public void propertyChanged(Config config, String key, String oldValue, String newValue) {
153       // Different Config instance
154       if (!config.equals(Search.this.config)) {
155         return;
156       }
157
158       // Check if Search configuration changed
159       if (key.startsWith("search.")){
160         String k = key.substring(7);
161         if ("match_depth".equals(k) ||
162             "min_free".equals(k) ||
163             "multiple_errors".equals(k)){
164           initialize(config);
165         }
166       }
167     }
168     
169     @Override
170     public void jpfRunTerminated (Config config){
171       config.removeChangeListener(this);
172     }
173   }
174   
175   /** {@code stateDepth} is an int vector storage system (akin to a map) that is responsible for associating states with their 
176    * corresponding depths. 
177    * 
178    * <p>{@code stateDepth} maps the state id of every state to the corresponding depth, in a one to one mapping.*/
179   protected final IntVector stateDepth = new IntVector();
180
181   /** 
182    * Constructs a {@code Search} object using the configuration specified by the user in {@code config} and a virtual machine
183    * that will be used for verification.
184    * 
185    *  @param config The configuration and properties that the search loop will be required to commence verification under
186    *  @param vm The virtual machine that the search loop will traverse and verify states from
187    */
188   protected Search (Config config, VM vm) {
189     this.vm = vm;
190     this.config = config;
191
192     initialize( config);
193
194     properties = getProperties(config);
195     if (properties.isEmpty()) {
196       log.severe("no property");
197     }
198     
199     config.addChangeListener( new ConfigListener());
200   }
201
202   /**
203    * Initializes the properties that the search loop will need to run under in order to make sure that each iteration of the search
204    * loop is in compliance with the properties set by JPF and the user.
205    * 
206    * @param conf The configuration object ({@code config}) that contains the necessary information to initialize the property values
207    */
208   protected void initialize( Config conf){
209     depthLimit = conf.getInt("search.depth_limit", Integer.MAX_VALUE);
210     matchDepth = conf.getBoolean("search.match_depth");
211     minFreeMemory = conf.getMemorySize("search.min_free", 1024<<10);    
212     getAllErrors = conf.getBoolean("search.multiple_errors");
213   }
214   
215   /**
216    * Called after the JPF run is finished. Should not be public, but is called by JPF
217    */
218   public void cleanUp(){
219     // nothing here, the ConfigListener removes itself
220   }
221   
222   /** 
223    * Returns the {@code config} object that is used by the {@code Search} class.
224    * 
225    * @return The configuration object that is used for verification
226    */
227   public Config getConfig() {
228     return config;
229   }
230   
231   /**
232    * One of the most important methods in the {@code Search} class. {@code search} is used to specify what the algorithm and behavior 
233    * for verification are. When the term "search loop" is brought up in other documentation, it generally means the loop that is used
234    * running in the {@code search} method.
235    */
236   public abstract void search ();
237
238   /**
239    * Sets the {@code reporter} object used during verification to the specified {@code reporter}.
240    * 
241    * @param reporter The reporter used to replace the current reporter object in the {@code Search} class
242    */
243   public void setReporter(Reporter reporter){
244     this.reporter = reporter;
245   }
246
247   /**
248    * Appends a {@code SearchListener} object to the {@code listener} array. In addition to appending the search listener, the action is also logged
249    * to the JPFLog {@code log} used in the {@code Search} class.
250    * 
251    * @param newListener A new {@code SearchListener} to append to the {@code listener} array
252    */
253   public void addListener (SearchListener newListener) {
254     log.info("SearchListener added: ", newListener);
255     listeners = Misc.appendElement(listeners, newListener);
256   }
257
258   /**
259    * Checks whether a listener of the same type as {@code listenerCls} exists in {@code listeners} already.
260    * 
261    * @param listenerCls The object type to check {@code listeners} against
262    * @return true if an element of the same type as the input parameter exists in {@code listeners}. False otherwise
263    */
264   public boolean hasListenerOfType (Class<?> listenerCls) {
265     return Misc.hasElementOfType(listeners, listenerCls);
266   }
267   
268   /**
269    * Returns the next element in {@code listeners} after the element matching {@code prev} that is of the same type as {@code type}.
270    * 
271    * @param type The type of element to search for and return
272    * @param prev The previous element to begin the search from
273    * @return An element of the same class as {@code type} and coming after {@code prev} in the {@code listeners} array
274    */
275   public <T> T getNextListenerOfType(Class<T> type, T prev){
276     return Misc.getNextElementOfType(listeners, type, prev);
277   }
278
279   /**
280    * Remove the specified {@code SearchListener} from the {@code listeners} array.
281    * 
282    * @param removeListener The element to remove from the {@code listeners} array
283    */
284   public void removeListener (SearchListener removeListener) {
285     listeners = Misc.removeElement(listeners, removeListener);
286   }
287
288   /**
289    * Add a new property to {@code properties}
290    * 
291    * @param newProperty The property to add to {@code properties}
292    */
293   public void addProperty (Property newProperty) {
294     properties.add(newProperty);
295   }
296
297   /**
298    * Remove the specified property from {@code properties}
299    * 
300    * @param oldProperty The property to remove from {@code properties}
301    */
302   public void removeProperty (Property oldProperty) {
303      properties.remove(oldProperty);
304   }
305
306   /**
307    * Returns the list of configured properties.
308    * 
309    * <p>Note there is a name clash here - JPF 'properties' have nothing to do with Java properties (java.util.Properties)
310    * 
311    * @param config The config object to retrieve the properties list from
312    * @return The list of configured properties
313    */
314   protected ArrayList<Property> getProperties (Config config) {
315     Class<?>[] argTypes = { Config.class, Search.class };
316     Object[] args = { config, this };
317
318     ArrayList<Property> list = config.getInstances("search.properties", Property.class,
319                                                    argTypes, args);
320
321     return list;
322   }
323
324   /**
325    * Check for property violations and return true if a property is violated and the search loop has finished running (i.e. {@code done} 
326    * is set to true). Returns false otherwise.
327    * 
328    * @return true if an a property has been violated (i.e. {@code currentError} is not null) and {@code done} is true
329    */
330   protected boolean hasPropertyTermination () {
331     if (currentError != null){
332       if (done){
333         return true;
334       } else { // we search for multiple errors, so we ignore and go on
335         doBacktrack = true;
336       }
337     }
338
339     return false;
340   }
341
342   /**
343    * Iterates through {@code properties} and checks for property violations. {@code checkPropertyViolation} should only be 
344    * called once per transition to avoid it adding the same error every time it is called.
345    * 
346    * @return true if a property violation is found, false otherwise
347    */
348   protected boolean checkPropertyViolation () {
349     for (Property p : properties) {
350       if (!p.check(this, vm)) {
351         error(p, vm.getClonedPath(), vm.getThreadList());
352         return true;
353       }
354     }
355
356     return false;
357   }
358
359   /**
360    * Returns the list of errors encountered during verification
361    * 
362    * @return The list of errors encountered during verification
363    */
364   public List<Error> getErrors () {
365     return errors;
366   }
367
368   /**
369    * Returns the number of errors encountered during verification. Will always return 1 if {@code getAllErrors} is false
370    * 
371    * @return The number of errors encountered during verification
372    */
373   public int getNumberOfErrors(){
374     return errors.size();
375   }
376
377   /**
378    * Returns the search constraint that was most recently encountered
379    * 
380    * @return A String detailing the search constraint most recently hit or null if none was encountered
381    */
382   public String getLastSearchConstraint() {
383     return lastSearchConstraint;
384   }
385
386   /**
387    * Request a probe
388    * 
389    * <p>This does not perform the actual listener notification, it only stores
390    * the request, which is then processed from within JPFs inner execution loop.
391    * As a consequence, {@code probeSearch} can be called asynchronously, and {@code searchProbed} listeners
392    * don't have to bother with synchronization or inconsistent JPF states (notification 
393    * happens from within JPFs main thread after a completed Instruction execution)
394    */
395   public void probeSearch(){
396     notifyProbeListeners.set(true);
397   }
398   
399   /**
400    * Performs the actual notification and resets the request, hence this call should only happen from within JPFs main thread
401    */
402   public void checkAndResetProbeRequest(){
403     if (notifyProbeListeners.compareAndSet(true, false)){
404       notifySearchProbed();
405     }
406   }
407   
408   /**
409    * Returns the most recent error encountered during the last transition
410    * 
411    * @return The error encountered during the last transition or null if none was encountered
412    */
413   public Error getCurrentError(){
414     return currentError;
415   }
416
417   /**
418    * Returns the most recent error encountered in the past
419    * 
420    * @return The most recent error encountered in the past or none if no error has been encountered during verification
421    */
422   public Error getLastError() {
423     int i=errors.size()-1;
424     if (i >=0) {
425       return errors.get(i);
426     } else {
427       return null;
428     }
429   }
430
431   /**
432    * Returns whether or not the search loop has encountered an error yet
433    * 
434    * @return true if an error has been encountered, false otherwise
435    */
436   public boolean hasErrors(){
437     return !errors.isEmpty();
438   }
439
440   /**
441    * Returns the {@code vm} object used by the search loop
442    * 
443    * @return the {@code vm} object used by {@code Search}
444    */
445   public VM getVM() {
446     return vm;
447   }
448
449   /**
450    * Returns true if the search loop has transitioned into an end state in the virtual machine
451    * 
452    * @return true if the current state of the {@code vm} is an end state
453    */
454   public boolean isEndState () {
455     return vm.isEndState();
456   }
457
458   /**
459    * Returns if an error has been encountered during the transition into the current state
460    * 
461    * @return true if an error has been encountered during the most recent transition, false otherwise
462    */
463   public boolean isErrorState(){
464     return (currentError != null);
465   }
466
467   /**
468    * Returns whether of not the current state is an end state in the virtual machine
469    * 
470    * @return true if this is not an end state of the {@code vm}, false otherwise
471    */
472   public boolean hasNextState () {
473     return !isEndState();
474   }
475
476   /**
477    * Returns whether a transition has occurred from the previous state or not
478    * 
479    * @return true if a transition has occurred, false otherwise
480    */
481   public boolean transitionOccurred(){
482     return vm.transitionOccurred();
483   }
484
485   /**
486    * Returns whether the current state in the search loop is a new state and false otherwise. 
487    * 
488    * <p>However, if {@code matchDepth} is set to true,
489    * 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
490    * depth will also be recorded for future use.
491    * 
492    * @return true if the current state is a new state and false otherwise (behaviour changes if {@code matchDepth} is true
493    */
494   public boolean isNewState () {
495     boolean isNew = vm.isNewState();
496
497     if (matchDepth) {
498       int id = vm.getStateId();
499
500       if (isNew) {
501         setStateDepth(id, depth);
502       } else {
503         return depth < getStateDepth(id);
504       }
505     }
506
507     return isNew;
508   }
509
510   /**
511    * Returns whether the current state has been visited yet. The opposite of {@code isNewState}
512    * 
513    * @return true if the state has been visited, false otherwise (behavior changes if {@code matchDepth} is true)
514    * @see #isNewState()
515    */
516   public boolean isVisitedState () {
517     return !isNewState();
518   }
519
520   /**
521    * Returns whether the current state is an ignored state in the virtual machine
522    * 
523    * @return true if the current state is an ignored state, false otherwise
524    */
525   public boolean isIgnoredState(){
526     return vm.isIgnoredState();
527   }
528
529   /**
530    * Returns whether the current state has been fully explored by the search loop.
531    * 
532    * @return true if the current state has been fully explored and processed, false otherwise
533    */
534   public boolean isProcessedState(){
535     return vm.getChoiceGenerator().isProcessed();
536   }
537
538   /**
539    * Return whether the search loop has finished verification
540    * 
541    * @return true if the search loop has finished verification, false otherwise
542    */
543   public boolean isDone(){
544     return done;
545   }
546
547   /**
548    * Return the current depth of the search loop
549    * 
550    * @return The current depth inside the search tree.
551    */
552   public int getDepth () {
553     return depth;
554   }
555
556   /**
557    * Returns the most recent search constraint that was encountered
558    * 
559    * @return A String detailing the most recent search constraint that was encountered
560    */
561   public String getSearchConstraint () {
562     return lastSearchConstraint;
563   }
564
565   /**
566    * Returns the most recent transition that has occurred
567    * 
568    * @return The last transition that occurred during verification, or null if none has occurred
569    */
570   public Transition getTransition () {
571     return vm.getLastTransition();
572   }
573
574   /**
575    * Returns the state id of the current state
576    * 
577    * @return The state id of the current state
578    */
579   public int getStateId () {
580     return vm.getStateId();
581   }
582
583   /**
584    * Returns the purged states id
585    * 
586    * <p>Note that while it should return the purged states id, it currently only returns -1 as a 
587    * result of many searches not utilizing this functionality. If it is required, {@code getPurgedStateId}
588    * should be overridden and changed in subsequent child classes.
589    * 
590    * @return The purged states id (currently only returns -1)
591    */
592   public int getPurgedStateId () {
593     return -1; // a lot of Searches don't purge any states
594   }
595
596
597   /**
598    * Requests that the search loop backtracks one step
599    * 
600    * <p>This is somewhat redundant to {@code SystemState.setIgnored}, but we don't
601    * want to mix the case of overriding state matching with backtracking when
602    * searching for multiple errors.
603    * 
604    * @return The value of {@code doBacktrack} after is has been set to true (i.e. always true)
605    */
606   public boolean requestBacktrack () {
607     return doBacktrack = true;
608   }
609
610   /**
611    * Returns the value of {@code doBacktrack} as well as resetting {@code doBacktrack} to false
612    * 
613    * @return the value of {@code doBackTrack}
614    */
615   protected boolean checkAndResetBacktrackRequest() {
616     if (doBacktrack){
617       doBacktrack = false;
618       return true;
619     } else {
620       return false;
621     }
622   }
623
624   /**
625    * Returns whether the search algorithm supports backtracking or not
626    * 
627    * @return true if the search algorithm supports backtracking, false otherwise (by default the return
628    * is true unless overridden)
629    */
630   public boolean supportsBacktrack () {
631     return true;
632   }
633
634   /**
635    * Returns whether the search algorithm supports restoring states that have been stored (a useful method in 
636    * BreadthFirstSearch)
637    * 
638    * @return true if the search algorithm supports restoring states, false otherwise (by default the return
639    * is false as the function is unsupported)
640    */
641   public boolean supportsRestoreState () {
642     // not supported by default
643     return false;
644   }
645
646   /**
647    * Returns the depth limit set at the beginning of verification
648    * 
649    * @return The {@code depthLimit} property
650    */
651   public int getDepthLimit () {
652     return depthLimit;
653   }
654   
655   /**
656    * Sets a new value for the {@code depthLimit} property
657    * 
658    * @param limit The new limit to set {@code depthLimit} to
659    */
660   public void setDepthLimit(int limit){
661     depthLimit = limit;
662   }
663
664   /**
665    * Returns a {@code SearchState} object with information describing the current state in the search loop
666    * 
667    * @return A {@code SearchState} object with information about the current state
668    */
669   protected SearchState getSearchState () {
670     return new SearchState(this);
671   }
672
673   /**
674    * Creates a new error with the corresponding {@code Property} that causes the error. Does not provide a {@code Path} or {@code ThreadList}, and
675    * can therefore be used by {@code SearchListeners} to create path-less errors to ensure liveness. 
676    * 
677    * @param property the property that caused the error
678    * @see #error(Property, Path, ThreadList)
679    */
680   public void error (Property property) {
681     error(property, null, null);
682   }
683
684   /**
685    * Creates an error with the corresponding {@code Property} that causes the error, alongside the {@code Path}, and {@code ThreadList}.
686    * 
687    * <p>Will set {@code done} to true and halt the search loop  if {@code getAllErrors} is false. If {@code getAllErrors} is true, it will 
688    * clone the {@code Property}, {@code Path}, and {@code ThreadList} objects that were passed in (as not cloning them may cause subsequent
689    * operations to overwrite information still in use) and add them to the {@code errors} list
690    * and continue verification.
691    * 
692    * <p>The property that caused the error is not reset here as the listeners attached to the search should be notified of the error first.
693    * This becomes especially problematic if one of the listeners caused the property violation, as which point it would get  confused
694    * if the {@code propertyViolated()} notification happens after the property is reset.
695    * 
696    * @param property The property that causes the error
697    * @param path The path corresponding to the error
698    * @param threadList The list of thread information corresponding to the error
699    */
700   public void error (Property property, Path path, ThreadList threadList) {
701
702     if (getAllErrors) {
703        // otherwise we are going to overwrite it if we go on
704       try {
705         property = property.clone();
706         path = path.clone();
707         threadList = (ThreadList) threadList.clone(); // this makes it a snapshot (deep) clone
708       } catch (CloneNotSupportedException cnsx){
709         throw new JPFException("failed to clone error information: " + cnsx);
710       }
711       done = false;
712       
713     } else {
714       done = true;
715     }
716
717     currentError = new Error(errors.size()+1, property, path, threadList);
718
719     errors.add(currentError);
720
721   }
722
723   /**
724    * Resets all properties, returning violated properties to their default states.
725    */
726   public void resetProperties(){
727     for (Property p : properties) {
728       p.reset();
729     }
730   }
731
732   /**
733    * Notifies the {@code SearchListener} objects in the {@code listeners} list that the search loop has advanced states.
734    */
735   protected void notifyStateAdvanced () {
736     try {
737       for (int i = 0; i < listeners.length; i++) {
738         listeners[i].stateAdvanced(this);
739       }
740       if (reporter != null){
741         // reporter always comes last to ensure all listeners have been notified
742         reporter.stateAdvanced(this);
743       }
744     } catch (Throwable t) {
745       throw new JPFListenerException("exception during stateAdvanced() notification", t);
746     }
747   }
748
749   /**
750    * Notifies the {@code SearchListener} objects in the {@code listeners} list that the search loop has finished processing
751    * the current state.
752    */
753   protected void notifyStateProcessed() {
754     try {
755       for (int i = 0; i < listeners.length; i++) {
756         listeners[i].stateProcessed(this);
757       }
758       if (reporter != null){
759         reporter.stateProcessed(this);
760       }
761     } catch (Throwable t) {
762       throw new JPFListenerException("exception during stateProcessed() notification", t);
763     }
764   }
765
766   /**
767    * Notifies the {@code SearchListener} objects in the {@code listeners} list that the search loop has stored the current state.
768    */
769   protected void notifyStateStored() {
770     try {
771       for (int i = 0; i < listeners.length; i++) {
772         listeners[i].stateStored(this);
773       }
774       if (reporter != null){
775         reporter.stateStored(this);
776       }
777     } catch (Throwable t) {
778       throw new JPFListenerException("exception during stateStored() notification", t);
779     }
780   }
781
782   /**
783    * Notifies the {@code SearchListener} objects in the {@code listeners} list that the search loop has restored a currently 
784    * stored state.
785    */
786   protected void notifyStateRestored() {
787     try {
788       for (int i = 0; i < listeners.length; i++) {
789         listeners[i].stateRestored(this);
790       }
791       if (reporter != null){
792         reporter.stateRestored(this);
793       }
794     } catch (Throwable t) {
795       throw new JPFListenerException("exception during stateRestored() notification", t);
796     }
797   }
798
799   /**
800    * Notifies the {@code SearchListener} objects in the {@code listeners} list that the search loop has backtracked to a 
801    * previous state.
802    */
803   protected void notifyStateBacktracked() {
804     try {
805       for (int i = 0; i < listeners.length; i++) {
806         listeners[i].stateBacktracked(this);
807       }
808       if (reporter != null){
809         reporter.stateBacktracked(this);
810       }
811     } catch (Throwable t) {
812       throw new JPFListenerException("exception during stateBacktracked() notification", t);
813     }
814   }
815
816   /**
817    * Notifies the {@code SearchListener} objects in the {@code listeners} list that the search loop has purged the current state.
818    */
819   protected void notifyStatePurged() {
820     try {
821       for (int i = 0; i < listeners.length; i++) {
822         listeners[i].statePurged(this);
823       }
824       if (reporter != null){
825         reporter.statePurged(this);
826       }
827     } catch (Throwable t) {
828       throw new JPFListenerException("exception during statePurged() notification", t);
829     }
830   }
831
832   /**
833    * Notifies the {@code SearchListener} objects in the {@code listeners} list that a probe request has been triggered during 
834    * verification.
835    */
836   public void notifySearchProbed() {
837     try {
838       for (int i = 0; i < listeners.length; i++) {
839         listeners[i].searchProbed(this);
840       }
841       if (reporter != null){
842         reporter.searchProbed(this);
843       }
844     } catch (Throwable t) {
845       throw new JPFListenerException("exception during searchProbed() notification", t);
846     }
847   }
848
849   
850   /**
851    * Notifies the {@code SearchListener} objects in the {@code listeners} list that the search loop has encountered a property 
852    * violation
853    */
854   protected void notifyPropertyViolated() {
855     try {
856       for (int i = 0; i < listeners.length; i++) {
857         listeners[i].propertyViolated(this);
858       }
859       if (reporter != null){
860         reporter.propertyViolated(this);
861       }
862     } catch (Throwable t) {
863       throw new JPFListenerException("exception during propertyViolated() notification", t);
864     }
865
866     // reset properties if getAllErrors is set
867     if (getAllErrors){
868       resetProperties();
869     }
870   }
871
872   /**
873    * Notifies the {@code SearchListener} objects in the {@code listeners} list that the search loop has begun verification.
874    */
875   protected void notifySearchStarted() {
876     try {
877       for (int i = 0; i < listeners.length; i++) {
878         listeners[i].searchStarted(this);
879       }
880       if (reporter != null){
881         reporter.searchStarted(this);
882       }
883     } catch (Throwable t) {
884       throw new JPFListenerException("exception during searchStarted() notification", t);
885     }
886   }
887
888   /**
889    * Notifies the {@code SearchListener} objects in the {@code listeners} list that the search loop has encountered a
890    * search constraint. The {@code details} String outlines the search constraint that was hit as well as any other
891    * relevant information.
892    * 
893    * @param details Information regarding the recent search constraint that was encountered.
894    */
895   public void notifySearchConstraintHit(String details) {
896     try {
897       lastSearchConstraint = details;
898       for (int i = 0; i < listeners.length; i++) {
899         listeners[i].searchConstraintHit(this);
900       }
901       if (reporter != null){
902         reporter.searchConstraintHit(this);
903       }
904     } catch (Throwable t) {
905       throw new JPFListenerException("exception during searchConstraintHit() notification", t);
906     }
907   }
908
909   /**
910    * Notifies the {@code SearchListener} objects in the {@code listeners} list that the search loop has finished verification.
911    */
912   protected void notifySearchFinished() {
913     try {
914       for (int i = 0; i < listeners.length; i++) {
915         listeners[i].searchFinished(this);
916       }
917       if (reporter != null){
918         reporter.searchFinished(this);
919       }
920     } catch (Throwable t) {
921       throw new JPFListenerException("exception during searchFinished() notification", t);
922     }
923   }
924
925   /**
926    * Requests that the virtual machine move to the next unvisited state below the current one in the search tree.
927    * {@code forward} along with {@code backtrack} constitute the two methods that are generally used to advance
928    * the search algorithm during verification.
929    * 
930    * @return true if a state exists and the virtual machine can move to it, false if the state does not exist
931    * or if it was previously explored.
932    * @see #backtrack()
933    */
934   protected boolean forward () {
935     currentError = null;
936
937     boolean ret = vm.forward();
938
939     checkPropertyViolation();
940     return ret;
941   }
942   
943   /**
944    * Requests that the virtual machine move to the previous state in the search tree. {@code backtrack} along
945    * with {@code forward} constitute the two methods that are generally used to advance the search algorithm 
946    * during verification.
947    * 
948    * @return true if the backtrack to the previous state was successful, false otherwise
949    */
950   protected boolean backtrack () {
951     return vm.backtrack();
952   }
953
954   /**
955    * Requests that the virtual machine sets whether the current state should be ignored in all future iterations
956    * of the search loop. This should not be used without cause as it causes the search tree to be pruned whenever
957    * it is called, which is expensive, especially in larger trees.
958    * 
959    * @param cond Whether or not the current state should be ignored
960    */
961   public void setIgnoredState (boolean cond) {
962     vm.ignoreState(cond);
963   }
964
965   /**
966    * Restores a previously stored virtual machine state.
967    * 
968    * <p>By default this method is not supported, and therefore requires implementation logic in child classes.
969    *
970    * @param state The stored state to be restored
971    */
972   protected void restoreState (State state) {
973     // not supported by default
974   }
975
976   /** 
977    * Sets {@code done} to true in order to terminate the search loop.
978    * 
979    * <p>Can be used by listeners to terminate the search.
980    * 
981    */
982   public void terminate () {
983     done = true;
984   }
985
986   /**
987    * Sets the depth of the specified state given its state id.
988    * 
989    * <p>When the depth of the state is set, it is set as depth + 1. This is to differentiate between
990    * states that have had their depths set, and states that have not (in which case their default depth
991    * will be 0).
992    * 
993    * @param stateId The state in question
994    * @param depth The new depth to set for the state
995    */
996   protected void setStateDepth (int stateId, int depth) {
997     stateDepth.set(stateId, depth + 1);
998   }
999
1000   
1001   /**
1002    * Returns the saved depth of the specified state given its state id.
1003    * 
1004    * <p>If the state in question has not had its state depth set previously, then it will by default have
1005    * a depth that is less than or equal to 0. Otherwise if the state has been visited, the depth will be 
1006    * returned.
1007    * 
1008    * @param stateId The state to return the depth of
1009    * @return The depth of the specified state
1010    * @throws JPFException If the state has not been visited in the past
1011    */
1012   public int getStateDepth (int stateId) {
1013     int depthPlusOne = stateDepth.get(stateId);
1014     if (depthPlusOne <= 0) {
1015       throw new JPFException("Asked for depth of unvisited state");
1016     } else {
1017       return depthPlusOne - 1;
1018     }
1019   }
1020
1021   /**
1022    * Check if there is the minimum amount of free memory left or more. If not, we would rather stop in time
1023    * (with a threshold amount left) in order to report something useful, and not just end verification silently
1024    * with a OutOfMemoryError (which is not handled too gracefully by most VMs)
1025    * 
1026    * <p>If the minimum amount of memory has been reached, the method will first try to activate garbage collection
1027    * and then check again if that made a difference. If the amount of memory available is still less than the 
1028    * minimum amount of memory, then we return false.
1029    * 
1030    * @return true if we have more memory than the minimum free memory, false otherwise.
1031    */
1032   public boolean checkStateSpaceLimit () {
1033     Runtime rt = Runtime.getRuntime();
1034
1035     long avail = rt.freeMemory();
1036
1037     // we could also just check for a max number of states, but what really
1038     // limits us is the memory required to store states
1039
1040     if (avail < minFreeMemory) {
1041       // try to collect first
1042       rt.gc();
1043       avail = rt.freeMemory();
1044
1045       if (avail < minFreeMemory) {
1046         // Ok, we give up, threshold reached
1047         return false;
1048       }
1049     }
1050
1051     return true;
1052   }
1053 }
1054