001: //
002: // Copyright (C) 2005 United States Government as represented by the
003: // Administrator of the National Aeronautics and Space Administration
004: // (NASA). All Rights Reserved.
005: //
006: // This software is distributed under the NASA Open Source Agreement
007: // (NOSA), version 1.3. The NOSA has been approved by the Open Source
008: // Initiative. See the file NOSA-1.3-JPF at the top of the distribution
009: // directory tree for the complete NOSA document.
010: //
011: // THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
012: // KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
013: // LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
014: // SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
015: // A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
016: // THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
017: // DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
018: //
019: package gov.nasa.jpf.search;
020:
021: import gov.nasa.jpf.*;
022: import gov.nasa.jpf.util.Debug;
023:
024: /**
025: * standard depth first model checking (but can be bounded by search depth
026: * and/or explicit Verify.ignoreIf)
027: */
028: public class DFSearch extends AbstractSearch {
029:
030: public DFSearch(Config config, VM vm) {
031: super (config, vm);
032:
033: Debug.println(Debug.MESSAGE, "MC Search");
034: }
035:
036: public boolean requestBacktrack() {
037: doBacktrack = true;
038:
039: return true;
040: }
041:
042: /**
043: * state model of the search
044: * next new -> action
045: * T T forward
046: * T F backtrack, forward
047: * F T backtrack, forward
048: * F F backtrack, forward
049: *
050: * end condition
051: * backtrack failed (no saved states)
052: * | property violation (currently only checked in new states)
053: * | search constraint (depth or memory or time)
054: *
055: * <2do> we could split the properties into forward and backtrack properties,
056: * the latter ones being usable for liveness properties that are basically
057: * condition accumulators for sub-paths of the state space, to be checked when
058: * we backtrack to the state where they were introduced. I think that could be
059: * actually much simpler (to implement) and more powerful than our currently
060: * broken LTL based scheme.
061: * But then again - at some point the properties and the searches will probably
062: * be unified into VM listeners, anyway
063: */
064:
065: public void search() {
066: int maxDepth = getMaxSearchDepth();
067:
068: depth = 0;
069:
070: notifySearchStarted();
071:
072: while (!done) {
073: if (!isNewState || isEndState) {
074: if (!backtrack()) { // backtrack not possible, done
075: break;
076: }
077:
078: depth--;
079: notifyStateBacktracked();
080: }
081:
082: if (forward()) {
083: notifyStateAdvanced();
084:
085: if (hasPropertyTermination()) {
086: break;
087: }
088:
089: if (isNewState) {
090: depth++;
091:
092: if (depth >= maxDepth) {
093: isEndState = true;
094: notifySearchConstraintHit(QUEUE_CONSTRAINT);
095: }
096:
097: if (!checkStateSpaceLimit()) {
098: notifySearchConstraintHit(SIZE_CONSTRAINT);
099: // can't go on, we exhausted our memory
100: break;
101: }
102: }
103: } else { // state was processed
104: notifyStateProcessed();
105: }
106: }
107:
108: notifySearchFinished();
109: }
110:
111: public boolean supportsBacktrack() {
112: return true;
113: }
114: }
|