---

Engine.java

package gov.nasa.arc.ase.jpf;

import gov.nasa.arc.ase.jpf.jvm.VirtualMachine;
import gov.nasa.arc.ase.util.Debug;
import gov.nasa.arc.ase.util.Options;
import gov.nasa.arc.ase.util.Statistics;
//#ifdef HEURISTIC

//#endif HEURISTIC
import java.io.*;
import java.net.*;
import java.util.*;
//#ifdef DISTRIBUTED

//#endif DISTRIBUTED
//#ifdef RACE || LOCK_ORDER


//#endif RACE || LOCK_ORDER
//#ifdef JDK11

//#endif JDK11
//#ifdef PARALLEL

//#endif PARALLEL

/**
 * Main engine of the model checker.
 *
 * @author Flavio Lerda
 * @author Willem Visser
 * @version 1.0
 * @since 1.0
 */
public class Engine {
  /**
   * A String containing the version of the model checker engine. This field is
   * used to output the version information.
   *
   * @see #start()
   */
  public static String VERSION = "JPF 0.1 - (C) 2000 RIACS/NASA Ames Research Center";

  /**
   * Parsed program arguments.
   */
  public static JPFOptions      options;

  /**
   * Arguments given to the model checker.
   */
  public static String[]    arguments;

  /**
   * Facility used to maintain statistics about the verification.
   */
  public static Statistics  statistics;

  /**
   * Local object which contains all the thread specific information.
   * Used by the parallel version in order to have this information accessible
   * without passing a reference thorught each method call, and avoiding to have
   * to share it between the threads.
   */
//#ifdef BANDERA
  private static JPF xjpf;
//#ifdef PARALLEL



































































































//#endif PARALLEL
//#ifdef PARALLEL










//#ifdef JDK11

//#endif JDK11




























































//#endif PARALLEL

//#ifdef RACE || LOCK_ORDER






//#ifdef DEBUG

//#endif DEBUG






//#ifdef RACE && LOCK_ORDER





//#else RACE && LOCK_ORDER

//#ifdef RACE




//#endif RACE

//#ifdef LOCK_ORDER




//#endif LOCK_ORDER

//#endif RACE && LOCK_ORDER



//#ifdef RACE

//#endif RACE
//#ifdef LOCK_ORDER

//#endif LOCK_ORDER











//#endif RACE

  /**
   * Accesses the thread local copy of a JPF object.
   *
   * @return the local JPF object
   */
  public static JPF getJPF() {
//#ifdef BANDERA
    return xjpf;
//#else BANDERA

//#endif BANDERA
  }  
//#else BANDERA
//#ifdef JDK11

//#else JDK11

//#endif JDK11
//#endif BANDERA

  /**
   * Initialize the model checker.
   * <UL>
   * <LI>Prints the version information.
   * <LI>Parses the program arguments in the options field.
   * <LI>Check for correctness of the arguments.
   * <LI>Handles the -help and -version switches.
   * <LI>Prints the current options if necessary.
   * </UL>
   *
   * @param args  arguments the program has been called with
   */
  public static void init(String[] args) {
    printVersion();

    arguments = options.parse(args);

    if(options.version) { System.exit(0); }

    if(options.help) {
      options.usage();
      System.exit(0);
    }

    if(Engine.options.print_options)
      options.print();
  }  
  /**
   * Creates a new iSearch object based on the current options
   *
   * @return an iSearch that is going to be used to do the search
   */
  public static iSearch newSearchAlgorithm() {
    if(options.path_simulation)
      return new Simulation();

//#ifdef BUCHI
    if(options.buchi != null)
      return new LTL();
    else
//#endif BUCHI
      if(options.verify)
//#ifdef HEURISTIC

//#endif HEURISTIC
      return new MC();
//#ifdef HEURISTIC


//#endif HEURISTIC
      else
    return new Simulation();
  }  
  /**
   * Prints the statistics accumulated during model checking.
   */
  private static void printStatistics() {
    statistics.print();

//#ifdef COVERAGE









//#endif COVERAGE

  }  
//#ifdef DISTRIBUTED











//#ifdef JDK11

//#endif JDK11






























//#endif DISTRIBUTED

  /**
   * Prints the version information about the model checker.
   */
  private static void printVersion() {
    Debug.println(Debug.ERROR, VERSION);
    try {
      Debug.println(Debug.ERROR, options.getMainClass().getField("VERSION").get(null));
    } catch(NoSuchFieldException e) {
    } catch(IllegalAccessException e) {
    }
    Debug.println(Debug.ERROR, "Build " + Build.getBuild() + " (" + Build.getBuildDate() + ")");
    Debug.println(Debug.ERROR);
  }  
  /**
   * Runs the model checking. First initializes the virtual machine with the
   * arguments received from the command line, initializes the internal
   * structures and then starts the search algorithm.
   *
   * @param vm  a iVirtualMachine implementation
   */
  public static void run(iVirtualMachine vm) {
    JPF jpf = new JPF();

    setJPF(jpf);

    jpf.store = new Store();
    jpf.status = new Status();
    jpf.reporter = new Reporter();
//#ifdef JDK11

//#endif JDK11

    jpf.vm = vm;
    jpf.search = newSearchAlgorithm();

    statistics = new Statistics();

    vm.init(arguments);

    jpf.run();

//#ifdef RACE || LOCK_ORDER

//#endif RACE || LOCK_ORDER

    printStatistics();
  }  
  /**
   * Sets the local JPF object into the thread local object.
   *
   * @param jpf a JPF object
   */
  static void setJPF(JPF jpf) {
//#ifdef BANDERA
    xjpf = jpf;
//#else BANDERA

//#endif BANDERA
  }  
}

---