01: //
02: // Copyright (C) 2005 United States Government as represented by the
03: // Administrator of the National Aeronautics and Space Administration
04: // (NASA). All Rights Reserved.
05: //
06: // This software is distributed under the NASA Open Source Agreement
07: // (NOSA), version 1.3. The NOSA has been approved by the Open Source
08: // Initiative. See the file NOSA-1.3-JPF at the top of the distribution
09: // 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:
24: import java.util.TreeSet;
25:
26: /**
27: * A BeamSearch is a HeuristicSearch with a state queue that is reset at each
28: * search level (i.e. it doesn't hop between search levels whe fetching the
29: * next state from the queue)
30: */
31: public class BeamSearch extends HeuristicSearch {
32: private TreeSet parents;
33:
34: public BeamSearch(Config config, VM vm) throws Config.Exception {
35: super (config, vm);
36: }
37:
38: public void search() {
39: int maxDepth = getMaxSearchDepth();
40:
41: int sid = getStateNumber();
42: h_state = new HeuristicState(sid, initHeuristicValue);
43: heuristic.processParent();
44:
45: if (pathCoverage) {
46: h_state.saveCoverage();
47: }
48:
49: done = false;
50:
51: if (hasPropertyTermination()) {
52: return;
53: }
54:
55: generateChildren(maxDepth);
56:
57: while ((queue.size() != 0) && !done) {
58: expandChildren(maxDepth);
59: }
60: }
61:
62: private void expandChildren(int maxDepth) {
63: // <2do> provide search listener hooks to monitor queue size and expanded states
64:
65: parents = (TreeSet) (queue.clone());
66: queue = new TreeSet(parents.comparator()); // 2do - Hmm, is this correct?
67:
68: while ((parents.size() != 0) && !done) {
69: expandState();
70: generateChildren(maxDepth);
71: }
72: }
73:
74: private void expandState() {
75: int s = parents.size();
76: h_state = (HeuristicState) (parents.first());
77: parents.remove(h_state);
78: vm.restoreState(h_state.getVirtualState());
79: heuristic.processParent();
80: }
81: }
|