---

Simulation.java

package gov.nasa.arc.ase.jpf;

import gov.nasa.arc.ase.util.Debug;

public class Simulation implements iSearch {
  private boolean failed = false;
  private boolean deadlock = false;
  private ErrorTrailInterface error;
  private Path errorPath;
  private boolean done;
  
  public Simulation() {
    Debug.println(Debug.WARNING, "Simulation 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;

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

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

    while (!done) {
      int tResult = Engine.getJPF().vm.Forward();

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

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

    case TransitionResult.END:
      done = true;
      break;
      }
    }
  }  
}

---