---

Simulation.java

package gov.nasa.arc.ase.jpf;

public class Simulation implements iSearch {
  public Simulation() {
  }  
  public void Deadlock(){
    boolean deadlock = verifyDeadlock();

    if(!deadlock)
      Engine.status.print("The program is deadlock free!");
  }  
  public ErrorTrailInterface getError() {
    return null;
  }  
  public Path getErrorPath() {
    return null;
  }  
  public boolean getResult() {
    return false;
  }  
  public void Invariant(iProperty p){
    Engine.status.print("Invariant can't be checked in simulation");
  }  
  private boolean verifyDeadlock() {
    boolean notFinished = true;
    int result;
    int index = 0;

    Engine.status.incrStates(index);
    while (notFinished) {
      result = Engine.vm.simForward();
      switch (result) {
      case RESULT.END:
        Engine.status.print("Deadlock!");
        Engine.vm.ShowErrorTrail();
    return true;

      case RESULT.EXIT:
        notFinished = false;
        break;

      case RESULT.NEW:
    Engine.status.incrStates(index);
    index++;
      }
    }

    return false;
  }  
}

---