---

SystemState.java

package gov.nasa.arc.ase.jpf.jvm;

import gov.nasa.arc.ase.jpf.Engine;
import gov.nasa.arc.ase.jpf.InternalErrorException;
import gov.nasa.arc.ase.jpf.iScheduler;
import gov.nasa.arc.ase.jpf.iSystemState;
import gov.nasa.arc.ase.jpf.iThreadInfo;
import gov.nasa.arc.ase.jpf.iTrailInfo;
import gov.nasa.arc.ase.jpf.JPFErrorException;
import gov.nasa.arc.ase.util.Debug;
import gov.nasa.arc.ase.util.HashData;
import java.util.Stack;

public class SystemState implements iSystemState, Storable, State {
  /**
   * The scheduler.
   */
  public Scheduler sch;

  /**
   * The kernel state.
   */
  public KernelState ks;

  /**
   * The trace information.
   */
  public TrailInfo  ti;
  
  /**
   * Reference to the virtual machine.
   */
  public VirtualMachine vm;

  /**
   * True if an assertion has been violated since last move.
   */
  public boolean violatedAssertion;

  /**
   * True if an exception was uncaught since last move.
   */
  public boolean uncaughtException;

  /**
   * Name of the uncaught exception since last move.
   */
  public String exceptionName;

//#ifdef MARK_N_SWEEP

  /**
   * Set to true if garbage collection is necessary
   */
  public boolean GCNeeded = false;

  private SystemState(SystemState ss) {
    sch = (Scheduler)ss.sch.clone();
    sch.ss = this;
    ks = (KernelState)ss.ks.clone();
    ks.ss = this;
    ti = null;
    vm = null;
    violatedAssertion = ss.violatedAssertion;
    uncaughtException = ss.uncaughtException;
    exceptionName = ss.exceptionName;
//#ifdef MARK_N_SWEEP
    GCNeeded = ss.GCNeeded;
//#endif MARK_N_SWEEP
  }  
//#endif MARK_N_SWEEP

  /**
   * Creates a new system state.
   */
  public SystemState(VirtualMachine vm) {
    this.vm = vm;

    ks = new KernelState(this);

    newScheduler();

    ti = null;

//#ifdef DISTRIBUTED && CHILDREN_LOOKAHEAD



//#endif DISTRIBUTED && CHILDREN_LOOKAHEAD
  }  
//#ifdef DISTRIBUTED && CHILDREN_LOOKAHEAD





























//#endif DISTRIBUTED && CHILDREN_LOOKAHEAD

//#ifdef MARK_N_SWEEP
  public void activateGC() {
    GCNeeded = true;
  }  
  public void backtrackTo(ArrayOffset storing, Object backtrack) {
    sch = (Scheduler)backtrack;
  }  
  public Object clone() {
    return new SystemState(this);
  }  
  public Object getBacktrackData() {
    return sch.clone();
  }  
  public Reference getClass(String name) {
    if(ks.sa.containsClass(name))
      return ks.sa.get(name);

    return null;
  }  
  public Object getData() {
    return new ArrayWrapper(ks.getStoringData());
  }  
  public int getDataSize(Object o) {
    return ((ArrayWrapper)o).size();
  }  
  public Reference getObject(int reference) {
    return ks.da.get(reference);
  }  
  public ThreadInfo getRunningThread() {
    if(sch.getThread() >= ks.tl.length()) return null;

    return ks.tl.get(sch.getThread());
  }  
  public iScheduler getScheduler() {
    return sch;
  }  
//#endif MARK_N_SWEEP

  public int[] getStoringData() {
    return null;
  }  
  public Thread getThread(int index) {
    return ks.tl.get(index);
  }  
  public Thread getThread(Reference reference) {
    return getThread(((ElementInfo)reference).index);
  }  
  public int getThreadCount() {
    return ks.tl.length();
  }  
  public iThreadInfo getThreadInfo(int idx) {
    return ks.tl.get(idx);
  }  
  public iTrailInfo getTrailInfo() {
    return ti;
  }  
  public void hash(HashData hd) {
    ks.hash(hd);
  }  
  public int hashCode() {
    HashData hd = new HashData();

    hash(hd);

    return hd.getValue();
  }  
  /**
   * Initializes a class. A class is initialized atomically without being
   * interleaved with any other thread.
   */
  public void initializeClass(ClassInfo ci) {
    ThreadInfo th = getRunningThread();
    if(th == null) return;

    MethodInfo mi = ci.getStaticMethod("<clinit>()V");
    if(mi == null) return;
    
    th.executeStaticMethod(mi);
  }  
  public void newScheduler() {
    if(Engine.options.interactive)
      sch = new InteractiveScheduler(this);
    else if(VirtualMachine.options.path_simulation)
      sch = new PathScheduler(this, (JVMPath)vm.getErrorTrail_from_file());
    else if (VirtualMachine.options.verify)
      if (VirtualMachine.options.po_reduction) 
    sch = new POScheduler(this);
      else if (VirtualMachine.options.random_order)
    sch = new RandomOrderScheduler(this);
      else
    sch = new DefaultScheduler(this);
    else
      sch = new RandomScheduler(this);
  }  
  /**
   * Computes next state.
   */
  public boolean nextSuccessor() {
    try {
//#ifdef HEURISTIC

//#endif HEURISTIC
      ThreadInfo th; // Thread that is going to be executed

      violatedAssertion = false;
      uncaughtException = false;
      exceptionName = null;
      th = (ThreadInfo)sch.locateThread(this);
    
      if(ks.isIntermediate()) {
    int t  = ks.getIntermediateThread();

    if (th != null)
          while(th != null && th.index != t) {
        sch.next();
        th = (ThreadInfo)sch.locateThread(this);
      }
      } 

      // there are no executable threads
      if (th == null) return false;
//#ifdef HEURISTIC

//#endif HEURISTIC
      try {
    if(th.executeStep()) {
      ks.clearIntermediate();
    } else {
      ks.setIntermediate();
    }
      } catch(UncaughtException e) {
    uncaughtException = true;
    exceptionName = e.getMessage();
      }

      return true;
    } catch(JPFErrorException e) {
      // JPF Errors fall throught and are caught by on outer try/catch.
      throw e;
    } catch(Exception e) {
      ks.jvmError(e, getRunningThread());
    }

    return false;
  }  
  public int random(int max) {
    return sch.random(max);
  }  
}

---