---

TrailInfo.java

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

import gov.nasa.arc.ase.jpf.Engine;
import gov.nasa.arc.ase.jpf.iTrailInfo;
import gov.nasa.arc.ase.jpf.jvm.bytecode.Instruction;
import gov.nasa.arc.ase.util.Debug;

public class TrailInfo implements iTrailInfo {
  private int thread;
  private int random;
  private Step[] steps;
//#ifdef BUCHI
  private int buchi_state = -1;
//#endif BUCHI

  public TrailInfo(int t, int r) {
    thread = t;
    random = r;
    steps = new Step[0];
  }  
  public void addBytecode(Instruction i) {
    steps[steps.length-1].addBytecode(i);
  }  
  public void addComment(String c) {
    steps[steps.length-1].addComment(c);
  }  
  public void addStep(String classname, int line) {
    int l = steps.length;

    if(l > 0)
      if(steps[l-1].classname.equals(classname))
    if(steps[l-1].line == line)
      return;

    Step[] n = new Step[l+1];
    
    System.arraycopy(steps, 0, n, 0, l);
    steps = n;
    steps[l] = new Step(classname, line);
  }  
  public int countSteps() {
    return steps.length;
  }  
  public int getBuchiState() {
    return buchi_state;
  }  
  public JVMPathEntry getEntry() {
    return new JVMPathEntry(steps[0].line, steps[0].classname, thread, random);
  }  
  public int getRandom() {
    return this.random;
  }  
  public Step getStep(int index) {
    if(index < 0 || index >= steps.length)
      return null;

    return steps[index];
  }  
  public int getThread() {
    return this.thread;
  }  
//#ifdef BUCHI
  public void setBuchiState(int bs) {
    buchi_state = bs;
  }  
//#endif BUCHI

  public String toString() {
    StringBuffer sb = new StringBuffer();

    sb.append("Thread #");
    sb.append(thread);
    sb.append(" Random #");
    sb.append(random);
//#ifdef BUCHI
    if(Engine.options.buchi != null) {
      sb.append(" Buchi State ");
      sb.append(buchi_state);
    }
//#endif BUCHI
    sb.append('\n');

    for(int i = 0, l = steps.length; i < l; i++)
      sb.append(steps[i].toString());

    return sb.toString();
  }  
}

---