HeuristicSearch


1   //
2   // Copyright (C) 2005 United States Government as represented by the
3   // Administrator of the National Aeronautics and Space Administration
4   // (NASA).  All Rights Reserved.
5   // 
6   // This software is distributed under the NASA Open Source Agreement
7   // (NOSA), version 1.3.  The NOSA has been approved by the Open Source
8   // Initiative.  See the file NOSA-1.3-JPF at the top of the distribution
9   // directory tree for the complete NOSA document.
10  // 
11  // THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
12  // KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
13  // LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
14  // SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
15  // A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
16  // THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
17  // DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
18  //
19  package gov.nasa.jpf.search.heuristic;
20  
21  import gov.nasa.jpf.Config;
22  import gov.nasa.jpf.VM;
23  import gov.nasa.jpf.search.AbstractSearch;
24  import gov.nasa.jpf.util.CoverageManager;
25  
26  import java.util.Comparator  ;
27  import java.util.TreeSet  ;
28  import gov.nasa.jpf.VMState;
29  
30  
31  /**
32   * a search strategy class that computes all immediate successors of a given
33   * state, puts them into a priority queue (the priority is provided by a
34   * Heuristic strategy object), and processes states in the sequence of
35   * highest priorities. Note that the queue is search-global, i.e. we might hop
36   * between search levels.
37   */
38  public class HeuristicSearch extends AbstractSearch {
39    
40    static final String   DEFAULT_HEURISTIC_PACKAGE = "gov.nasa.jpf.search.heuristic.";
41    
42    protected TreeSet       queue;
43    protected int         numberNewChildren = 0;
44    protected HeuristicState h_state;
45    protected HeuristicState new_h_state;
46    protected Heuristic     heuristic;
47    
48    protected boolean useAstar;
49    protected boolean pathCoverage = false; // set by some Heuristics instances
50    protected int initHeuristicValue;
51    protected int queueLimit;
52    
53    // statistics
54    int maxHeuristic = Integer.MIN_VALUE;
55    int minHeuristic = Integer.MAX_VALUE;
56    int heuristicTotal = 0;
57    int heuristicCount = 0;
58    
59    public HeuristicSearch (Config config, VM vm) throws Config.Exception {
60      super(config, vm);
61      
62      // note this covers three potential Heuristic implementation ctors:
63      // (a) (Config,HeuristicSearch), (b) (Config), (c) default
64      Class  [] argTypes = { Config.class, HeuristicSearch.class };
65      Object  [] args = { config, this };
66      heuristic = (Heuristic) config.getEssentialInstance("search.heuristic.class", 
67                                                          Heuristic.class, argTypes, args);
68      
69      useAstar = config.getBoolean("search.heuristic.astar");
70      pathCoverage = config.getBoolean("search.coverage.path");
71          
72      Comparator   comp = (Comparator  ) config.getEssentialInstance("search.heuristic.comparator.class",
73                                                                   Comparator  .class);
74      
75      queue = new TreeSet  (comp);
76      
77      queueLimit = config.getInt("search.heuristic.queue_limit", -1);
78      
79      initHeuristicValue = config.getInt("search.heuristic.initial_value", 0);
80    }
81    
82    public HeuristicState getNew () {
83      return new_h_state;
84    }
85    
86    public HeuristicState getOld () {
87      return h_state;
88    }
89  
90    protected void generateChildren (int maxDepth) {
91  
92      // <2do> add listener notifications to keep track of queue size
93      
94      boolean allChildren = false;
95      numberNewChildren = 0;
96      
97      while (!done && !allChildren) {
98        if (pathCoverage) {
99          h_state.restoreCoverage();
100       }
101       
102       CoverageManager.setLastIncrements(-1);
103       
104       if (!forward()) {
105         notifyStateProcessed();
106         return;
107       }
108 
109       depth = vm.getPathLength();
110       notifyStateAdvanced();
111 
112       if (hasPropertyTermination()) {
113         return;
114       }
115       
116       if (!isEndState) {
117 
118         if (!isNewState) {              // we have seen this
119           backtrack();
120           notifyStateBacktracked();
121           
122         } else if (depth >= maxDepth) { // don't want to see this
123           notifySearchConstraintHit(DEPTH_CONSTRAINT);
124           
125           backtrack();
126           notifyStateBacktracked();
127           
128         } else {                        // this is a new state, add to queue
129           new_h_state = new HeuristicState(getStateNumber(), initHeuristicValue);
130           
131           int h_value = heuristic.heuristicValue();
132           
133           if (vm.isInterestingState()) {
134             h_value = 0;
135           } else if (vm.isBoringState()) {
136             h_value = (maxHeuristic + 1);
137           }
138 
139           // update HeuristicSearch specific statistics
140           if (maxHeuristic < h_value) {
141             maxHeuristic = h_value;
142           }
143           if (minHeuristic > h_value) {
144             minHeuristic = h_value;
145           }
146           heuristicTotal += h_value;
147           heuristicCount++;
148           
149           if (useAstar) {
150             h_value += vm.getPathLength();
151           }
152           
153           if (h_value >= 0) {
154             new_h_state.setPriority(h_value);
155                         
156             // note that we only need to backtrack up to this point (from
157             // future forwards), hence we don't need full restorability
158             // (which is too expensive)
159             // <2do> might change in the future with a different state history rep
160             VMState vmState = vm.getState();
161             vmState.makeForwardRestorable();
162             new_h_state.setVirtualState(vmState);
163             
164             numberNewChildren++;
165             
166             if (pathCoverage) {
167               new_h_state.saveCoverage();
168             }
169             
170             queue.add(new_h_state);
171             
172             if ((queueLimit > 0) && (queue.size() > queueLimit)) {
173               queue.remove(queue.last());
174               notifySearchConstraintHit( QUEUE_CONSTRAINT);
175             }
176           }
177           
178           backtrack(); // back to our parent, to get the next child
179           notifyStateBacktracked();
180         }
181 
182       } else {  // no next state, nothing to queue
183         backtrack();
184         notifyStateBacktracked();
185       }
186     }
187   }
188   
189   public int getQueueSize () {
190     return queue.size();
191   }
192   
193   private void expandState () {
194     int s = queue.size();
195     h_state = (HeuristicState) (queue.first());
196     queue.remove(h_state);
197     
198     vm.restoreState(h_state.getVirtualState());
199     
200     heuristic.processParent();
201   }
202    
203   public void search () {
204     int maxDepth = getMaxSearchDepth();
205         
206     int sid = getStateNumber();
207     h_state = new HeuristicState(sid, initHeuristicValue);
208     heuristic.processParent();
209     
210     if (pathCoverage) {
211       h_state.saveCoverage();
212     }
213         
214     done = false;
215 
216     notifySearchStarted();
217     
218     if (hasPropertyTermination()) {
219       return;
220     }
221     
222     generateChildren(maxDepth);
223     while ((queue.size() != 0) && !done) {
224       expandState();
225       notifyStateRestored();
226       
227       // we could re-init the scheduler here
228       generateChildren(maxDepth);
229     }
230     
231     notifySearchFinished();
232   }
233   
234   public void setPathCoverage (boolean b) {
235     pathCoverage = b;
236     
237     CoverageManager.setPathCoverage(b); // <2do> bad redundancy
238   }
239   
240   public void setInstructionCoverage(boolean b) {
241     CoverageManager.setInstructionCoverage(b); // <2do> bad propagation, see 'setPathCoverage'
242   }
243   
244   public void setCalcBranchCoverage (boolean b) {
245     CoverageManager.setCalcBranchCoverage(b);
246   }
247 }
248 
249 
250
A to Z: JavaDoc & Examples Daily Java News & Articles Open Source Projects Open Source Codes Free Computer Books Remove Frame
Popular Tags