---

MC.java

package gov.nasa.arc.ase.jpf;

//import gov.nasa.arc.ase.jpf.communication.*;
import gov.nasa.arc.ase.util.Debug;

public class MC implements iSearch {
  private boolean done;
  private boolean failed = false;
  private boolean deadlock = false;
  private Path errorPath;
  private ErrorTrailInterface error;

  public MC() {
    Debug.println(Debug.MESSAGE, "MC Search");
  }  
  private void error() {
    failed = true;
    if (Engine.options.bandera) {
      errorPath = Engine.getJPF().vm.getErrorTrail1();
    } else {
      error = Engine.getJPF().vm.getErrorTrail();        
    }
    done = !Engine.options.multiple_errors;
  }  
  public ErrorTrailInterface getError() {
    return error;
  }  
  public String getErrorMessage() {
    if(!failed) return "No Errors Found";

    if(deadlock) return "Deadlock found";

    return Engine.getJPF().vm.getErrorMessage();
  }  
  public Path getErrorPath() {
    return errorPath;
  }  
  public boolean hasFailed() {
    return failed;
  }  
  public void search() {
    int depth = 0;
//#ifdef DISTRIBUTED

//#endif DISTRIBUTED

    done = false;
    Engine.getJPF().status.states++;
    depth++;

    if(Engine.options.deadlocks) {
      if(Engine.getJPF().vm.isDeadlocked()) {
    deadlock = true;
    error();
      }
    }

    while(depth > 0 && !done) {
      int tResult = Engine.getJPF().vm.Forward();

      if(Engine.options.assertions) {
    if(TransitionResult.isError(tResult)) {
      error();
      if(done) break;
    }
      }

      switch(TransitionResult.getResults(tResult)) {
    case TransitionResult.NEW:
      depth++;
      Engine.getJPF().status.states++;
      Engine.getJPF().status.transitions++;
      if(Engine.options.deadlocks) {
        if(Engine.getJPF().vm.isDeadlocked()) {
          deadlock = true;
          error();
        }
      }
      break;

    case TransitionResult.OLD:
      depth++;
      Engine.getJPF().status.transitions++;

    case TransitionResult.END:
      depth--;
      Engine.getJPF().vm.Backtrack();
      break;
      }
    }
  }  
}

---