---

JPF.java

package gov.nasa.arc.ase.jpf;

import java.io.PrintStream;
import java.io.FileOutputStream;
import java.io.IOException;

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

import gov.nasa.arc.ase.jpf.jvm.VirtualMachine;

//#ifdef LOCK_ORDER

//#endif LOCK_ORDER

/**
 * This class contains references to the different object that
 * make a verification run.
 *
 * @author Flavio Lerda
 * @version 1.0
 * @since 1.0
 */
public class JPF implements Runnable {
  /**
   * Used to store the states.
   */
  public iStore          store;

  /**
   * Maintains the current status of the model checker.
   */
  public Status     status;

  /**
   * Generates period reports.
   */
  public iReporter  reporter;

  /**
   * Reference to the virtual machine used by the model checker.
   */
  public iVirtualMachine vm;

  /**
   * The search engine used to visit the state space.
   */
  public iSearch         search;

//#ifdef BUCHI

  /**
   * Buchi automaton that represent the property to be checked.
   */ 
  public SM     buchi;

//#endif BUCHI

  /**
   * Time of the last report.
   */
  protected long lastReportTime = System.currentTimeMillis();

  /**
   * Number of transition in last report.
   */
  protected int lastReportTransitions = 0;

  /**
   * Initialize the model checking environment.
   */
  public JPF() {
  }  
  /**
   * Called after the virtual machine has been initialized.
   */
  public void initialized() {
  }  
  /**
   * Prints the results of the verification.
   */
  private void printResults() {
    if(search.hasFailed()) {
//#ifdef BANDERA
      if(Engine.options.bandera)
    vm.ShowErrorTrail(search.getErrorPath());
      else {
//#endif BANDERA
    vm.getErrorTrail_to_file();
    search.getError().print();
    try {
      PrintStream out = new PrintStream(new FileOutputStream("error.trail"));
      search.getError().print(out);
      out.close();
    } catch(IOException e) {
    }
    printResults(search.getErrorMessage());
//#ifdef BANDERA
      }
//#endif BANDERA
    } else
      printResults(search.getErrorMessage());
  }  
  /**
   * Prints the results contained in the status field. 
   *
   * @param msg a string that has to be printed as the result of the verification
   */
  private void printResults(String msg) {
    Debug.println(Debug.ERROR);
    Debug.println(Debug.ERROR);
    Debug.println(Debug.ERROR, "===================================");
    Debug.println(Debug.ERROR, msg);
    Debug.println(Debug.ERROR, "===================================");
    Debug.println(Debug.ERROR);
    status.print();
  }  
  /**
   * Prints a periodic one line report.
   */
  public void report() {
//#ifdef COVERAGE






//#endif COVERAGE

    long currentTime = System.currentTimeMillis();
    lastReportTransitions = 
      status.report(currentTime - lastReportTime, lastReportTransitions);
    lastReportTime = currentTime;
  }  
  /**
   * Executes the verification.
   */ 
  public void run() {
    if(!Engine.options.interactive)
      reporter.start();
    search.search();
    if(!Engine.options.interactive)
      reporter.stop();

//#ifdef LOCK_ORDER


//#endif LOCK_ORDER
    printResults();
  }  
}

---