---

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;
import java.io.*;
import java.net.*;
import java.util.*;
// ifdef DISTRIBUTED

//#endif DISTRIBUTED
// ifdef RACE
import gov.nasa.arc.ase.jpf.jvm.JVMOptions;
import gov.nasa.arc.ase.jpf.jvm.runtime.RaceWindow;
import gov.nasa.arc.ase.jpf.jvm.runtime.LockOrder;
import gov.nasa.arc.ase.jpf.jvm.runtime.Depend;
//#endif RACE

public class Engine {
  static String VERSION = "JPF 0.1 beta 12 - (C) 2000 RIACS/NASA Ames Research Center";
  static public iStore          store;
  static public rStatus         status;
  static public iVirtualMachine vm;
  static public iSearch         search;
  static public JPFOptions      options;
  static public String          className;
  static public Statistics  statistics;
  static public boolean         finished = false;
  static public boolean         cleanup = false;
// ifdef DISTRIBUTED





//#endif DISTRIBUTED
// ifdef BUCHI

//#endif BUCHI

  static private String[] classes;

// ifdef DISTRIBUTED





















































































//#endif DISTRIBUTED
  public static void init(String[] args) {
    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);

    classes = options.parse(args);
    if(options.version) {
      System.exit(0);
    }

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

    if(classes == null || classes.length != 1) {
      Debug.println(Debug.ERROR, "missing class name");
      System.exit(1);
    }
    className = classes[0];

    options.print();

    statistics = new Statistics();
    status = new rStatus();
// ifdef DISTRIBUTED





//#endif DISTRIBUTED
      store = new Store();
// ifdef DISTRIBUTED







//#endif DISTRIBUTED

      if (options.verify)
    search = new MC();
      else
    search = new Simulation();
// ifdef DISTRIBUTED

//#endif DISTRIBUTED
  }  
  public static void start() {
// ifdef DISTRIBUTED

//#endif DISTRIBUTED
      status.start();

// ifdef DISTRIBUTED

//#endif DISTRIBUTED
      search.Deadlock();

// ifdef RACE
      if (Depend.debug_on())Depend.print();
      if (LockOrder.on()) LockOrder.analyze((VirtualMachine)vm);
      if (((JVMOptions)options).post_verify) {
    RaceWindow.makeActive();
    RaceWindow.print();
    ((JVMOptions)Engine.options).race = false;
    ((JVMOptions)Engine.options).lock_order = false;
    ((JVMOptions)Engine.options).depend = false;
    ((JPFOptions)Engine.options).verify = true; 
    ((VirtualMachine)vm).reinit(className);
    Engine.status = new rStatus();
    search = new MC();
    search.Deadlock();
      }
//#endif RACE
// ifdef DISTRIBUTED

//#endif DISTRIBUTED

// ifdef DISTRIBUTED


//#endif DISTRIBUTED
  }  
  static public void stop() {
// ifdef DISTRIBUTED

//#endif DISTRIBUTED
      if(search.getResult()) {
    if (Engine.options.bandera) {
      Engine.vm.ShowErrorTrail(search.getErrorPath());
    } else {
      /******************************************************************/
      // dump error to file - to be used in path simulation
      /******************************************************************/
      Engine.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) {
      }
      if(Engine.options.assertions)
        Engine.status.print("Assertion broken!");
      else
        Engine.status.print("The program has a deadlock!");
// ifdef DISTRIBUTED


//#endif DISTRIBUTED
    }
      } else {
    if (Engine.options.assertions)
      Engine.status.print("The program has no assertion violations!");
    else 
      Engine.status.print("The program is deadlock free!");
      }
// ifdef DISTRIBUTED

//#endif DISTRIBUTED

    statistics.print();

// ifdef DISTRIBUTED

//#endif DISTRIBUTED
      if(!Engine.options.bandera)
    try {
      PrintStream out = new PrintStream(new FileOutputStream(className + ".log"));
      options.print(out);
      statistics.save(out);
      status.results.print(out, "The program is deadlock free");
      out.close();
    } catch(IOException e) {
    }
// ifdef DISTRIBUTED

//#endif DISTRIBUTED
    
// ifdef DISTRIBUTED

//#endif DISTRIBUTED
      status.stop();
  }  
  public static void threads() {
    ThreadGroup g = Thread.currentThread().getThreadGroup();

    while(g.getParent() != null)
      g = g.getParent();

    int count = 100;
    Thread[] t = new Thread[count];

    int l = g.enumerate(t, true);
    
    for(int i = 0; i < l; i++)
      Debug.println(Debug.WARNING, "#" + i + ": " + t[i]);
  }  
}

---