---

SystemState.java

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

import gov.nasa.arc.ase.jpf.*;
import gov.nasa.arc.ase.util.Debug;
import java.util.Stack;

public class SystemState implements iSystemState,Cloneable{
  private Scheduler   scheduler;    // The scheduler for the transitions
  private TrailInfo   trail_info;   // The information for the trail
// ifdef NO_FASTBACKTRACK

//#else NO_FASTBACKTRACK
  private int[]       backtrack_data;   // The compact version of the state
  public static int counter = 0;

  private int threadref = -1;
  private int depth = -1;
  private MethodInfo currentMethod = null;
  private int line = -1;

  private boolean intermediate = false;
  public int atomicLevel;

// ifdef REFERENCE_COUNT















//#endif REFERENCE_COUNT
//#endif NO_FASTBACKTRACK
  
// ifdef REFERENCE_COUNT

//#endif REFERENCE_COUNT

// ifdef DISTRIBUTED

//#endif DISTRIBUTED

  public SystemState() {
    scheduler = new Scheduler();
    trail_info = null;
// ifdef NO_FASTBACKTRACK

//#else NO_FASTBACKTRACK
    backtrack_data = null;
//#endif NO_FASTBACKTRACK

// ifdef DISTRIBUTED



//#endif DISTRIBUTED

  }  
// ifdef DEBUG




//#endif DEBUG

  public Object clone(){
    try{
      // First basic cloning, copies all the fields values
      // including references
      SystemState ss = (SystemState)super.clone();

      // The scheduler has its own clone method
      ss.scheduler    = (Scheduler)scheduler.clone();

// ifdef NO_COMPRESSION

//#endif NO_COMPRESSION

      // The thead info are set again or never changed
      // so they can be scared
      // implicit: ss.thread_info = thread_info;

      // The backtrack data need to be shared for saving memory
      // Actually they should be coming from the hash table
      // implicit: ss.backtrack_data = backtrack_data

// ifdef DISTRIBUTED






//#endif DISTRIBUTED

      // Returns the newly created object
      return ss;
    } catch(CloneNotSupportedException e){
      throw new InternalError(e.toString());
    }
  }  
  public int[] getBacktrackData() { // gets the backtrack information
    return backtrack_data;
  }  
  public Scheduler getScheduler() { // returns the value of the scheduler
    return scheduler;
  }  
  public iTrailInfo getTrailInfo() { // return the trail information
    return trail_info;
  }  
  public boolean handleIntermediate(KernelState ks) {
    if(intermediate && threadref != getScheduler().getCurrentThread()) {
      Engine.vm.Backtrack();
      return true;
    }

    return false;
  }  
  //** May be moved to KernelState with SystemState a parameter **//
  public boolean nextSuccessor(iKernelState ks) { // generate the next successor
    ThreadInfo th; // Thread that is going to be executed

    if (VirtualMachine.options.verify) // verification vs simulation
      if (!VirtualMachine.options.po_reduction) 
    // With the partial order reduction the next thread
    // to be executed must also be a safe thread.
    th = (ThreadInfo)scheduler.locateRunningThread(this, ks);
      else 
    // Just picks the next thread that needs to be executed
    th = (ThreadInfo)scheduler.locateSafeThread(this, ks);
    else 
      // Random simulation just picks a thread at random
      th = (ThreadInfo)scheduler.locateRandomRunningThread(ks);

// ifdef DEBUG

//#endif DEBUG

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

    // executes the next instruction for that thread
    intermediate = true;
    while(!th.executeStep(this, (KernelState)ks))
      ((VirtualMachine)Engine.vm).pushSystemState();
    intermediate = false;

    return true;
  }  
  public void restoreAtomicData(KernelState ks) {
    ((ThreadInfo)ks.getThreadInfo(threadref)).setAtomicData(depth, currentMethod, line);
  }  
  public void saveAtomicData(int t, int d, MethodInfo m, int l) {
    threadref = t;
    depth = d;
    currentMethod = m;
    line = l;
  }  
// ifdef NO_FASTBACKTRACK
  public void setBacktrackData(int[] o) { // sets the backtrack information
    backtrack_data = o;
  }  
//#endif NO_FASTBACKTRACK

// ifdef DISTRIBUTED















//#endif DISTRIBUTED

  public void setScheduler(Scheduler sch) {
    scheduler = sch;
  }  
  public void setTrailInfo(int thread, int line, String classname) {
    // sets the value of the current instruction for the trail
    trail_info = new TrailInfo(thread, scheduler.getCurrentRandom(), line,
                   classname);
  }  
  public void setTrailInfo(TrailInfo ti) {
    trail_info = ti;
  }  
  public void updateExtra(iSystemState ss) {
    SystemState s = (SystemState)ss;

    threadref = s.threadref; s.threadref = -1;
    depth = s.depth; s.depth = -1;
    currentMethod = s.currentMethod; s.currentMethod = null;
    line = s.line; s.line = -1;
  }  
}

---