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;
20:
21: import gov.nasa.jpf.Config;
22: import gov.nasa.jpf.VM;
23:
24: /**
25: * PathSearch is not really a Search object, just a simple 'forward'
26: * driver for the VM that loops until there is no next instruction or
27: * a property doesn't hold
28: *
29: */
30: public class PathSearch extends AbstractSearch {
31:
32: public PathSearch(Config config, VM vm) {
33: super (config, vm);
34: }
35:
36: public boolean requestBacktrack() {
37: doBacktrack = true;
38:
39: return true;
40: }
41:
42: public void search() {
43: depth++;
44:
45: if (hasPropertyTermination()) {
46: return;
47: }
48:
49: notifySearchStarted();
50:
51: while (true) {
52: while (doBacktrack) { // might be set by StateListeners
53:
54: if (depth > 0) {
55: vm.backtrack();
56: depth--;
57:
58: notifyStateBacktracked();
59: }
60:
61: doBacktrack = false;
62: }
63:
64: forward();
65: // isVisitedState is never true, because we don't really search, just replay
66: notifyStateAdvanced();
67:
68: if (hasPropertyTermination()) {
69: break;
70: }
71:
72: if (isEndState) {
73: break;
74: }
75:
76: depth++;
77: }
78:
79: notifySearchFinished();
80: }
81:
82: public boolean supportsBacktrack() {
83: return true;
84: }
85: }
|