---

JVMPath.java

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

import gov.nasa.arc.ase.jpf.Engine;
import gov.nasa.arc.ase.jpf.Path;
import gov.nasa.arc.ase.util.Debug;
import java.io.Serializable;

public class JVMPath implements Path {
  private JVMPathEntry[] error_moves;
  private int[] moves;
  private int   ups;
// ifdef DISTRIBUTED
// ifdef CHILDREN_LOOKAHEAD



//#endif CHILDREN_LOOKAHEAD
//#endif DISTRIBUTED
// ifdef DISTRIBUTED
// ifdef CHILDREN_LOOKAHEAD

//#endif CHILDREN_LOOKAHEAD
//#endif DISTRIBUTED

  // used for executing error-trails
  JVMPath(int s) {
    moves = new int[s];
    error_moves = new JVMPathEntry[s];
  }  
// ifdef DISTRIBUTED
// ifdef CHILDREN_LOOKAHEAD








//#else CHILDREN_LOOKAHEAD




//#endif CHILDREN_LOOKAHEAD
//#else DISTRIBUTED
  JVMPath(int s, int u) {
    moves = new int[s];
    ups = u;
  }  
  public Path append(Path p) {
    JVMPath pp = (JVMPath)p;
    int[] m1 = moves;
    int[] m2 = pp.moves;
    int l1 = m1.length;
    int l2 = m2.length;
    int u1 = ups;
    int u2 = pp.ups;
    int l, u, d;
    
    if(l1 > u2) {
      d = l1 - u2;
      u = u1;
    } else {
      d = 0;
      u = u1 + u2 - l1;
    }
    l = d + l2;

// ifdef DISTRIBUTED
// ifdef CHILDREN_LOOKAHEAD

//#else CHILDREN_LOOKAHEAD

//#endif CHILDREN_LOOKAHEAD
//#else DISTRIBUTED
    JVMPath ppp = new JVMPath(l, u);
//#endif DISTRIBUTED

    if(d != 0)
      System.arraycopy(m1, 0, ppp.moves, 0, d);
    System.arraycopy(m2, 0, ppp.moves, d, l2);

    return ppp;
  }  
  public boolean equals(Object o) {
    JVMPath p = (JVMPath)o;

    if(p.ups != ups) return false;
    if(p.moves.length != moves.length) return false;

    for(int i = 0; i < moves.length; i++)
      if(p.moves[i] != moves[i]) return false;

    return true;
  }  
  public static Path fromStoringData(Object o) {
    int[] data = (int[])o;
// ifdef DISTRIBUTED

//#endif DISTRIBUTED
    int length = data.length-1;
// ifdef DISTRIBUTED
// ifdef CHILDREN_LOOKAHEAD






//#endif CHILDREN_LOOKAHEAD
//#endif DISTRIBUTED
    
// ifdef DISTRIBUTED
// ifdef CHILDREN_LOOKAHEAD



//#else CHILDREN_LOOKAHEAD

//#endif CHILDREN_LOOKAHEAD
//#else DISTRIBUTED
    JVMPath p = new JVMPath(length, data[0]);
//#endif DISTRIBUTED
    System.arraycopy(data, 1, p.moves, 0, length);

    return p;
  }  
//#endif DISTRIBUTED

  int get(int index) {
    return moves[index];
  }  
  JVMPathEntry getErrorMove(int index) {
    return error_moves[index];
  }  
  public Object getStoringData() {
    int length = moves.length;
// ifdef DISTRIBUTED
// ifdef CHILDREN_LOOKAHEAD



//#endif CHILDREN_LOOKAHEAD
//#endif DISTRIBUTED
    int l = length + 1;
// ifdef DISTRIBUTED
// ifdef CHILDREN_LOOKAHEAD

//#endif CHILDREN_LOOKAHEAD
//#endif DISTRIBUTED
    int[] data = new int[l];

    data[0] = ups;
    System.arraycopy(moves, 0, data, 1, length);
// ifdef DISTRIBUTED
// ifdef CHILDREN_LOOKAHEAD


//#endif CHILDREN_LOOKAHEAD
//#endif DISTRIBUTED

    return data;
  }  
  public Path relativeTo(Path p) {
    int[] m1 = moves;
    int[] m2 = ((JVMPath)p).moves;
    int l1 = m1.length;
    int l2 = m2.length;
    int l = Math.min(l1, l2);
    
    int common = 0;
    for(int idx = 0; idx < l; idx++)
      if(m1[idx] == m2[idx])
    common++;
      else
    break;

// ifdef DISTRIBUTED
// ifdef CHILDREN_LOOKAHEAD

//#else CHILDREN_LOOKAHEAD

//#endif CHILDREN_LOOKAHEAD
//#else DISTRIBUTED
    JVMPath ppp = new JVMPath(l1 - common, l2 - common);
//#endif DISTRIBUTED

    for(int idx = common; idx < l1; idx++)
      ppp.moves[idx - common] = moves[idx];

    return ppp;
  }  
  void set(int index, int value) {
    moves[index] = value;
  }  
  void setErrorMove(int index, 
                    int line, 
                    String cname, 
                    int thread, 
                    int random) {
    error_moves[index] = new JVMPathEntry(line,
                                          cname,
                                          thread,
                                          random);
  }  
  public void setUps(int value) {
    ups = value;
  }  
  public int size() {
    return moves.length;
  }  
  public String toString() {
    StringBuffer sb = new StringBuffer("( ");

    sb.append(ups);
    sb.append(", [");

    int l = moves.length;
    for(int i = 0; i < l; i++) {
      if(i != 0) sb.append(", ");
      sb.append(moves[i]);
    }

    sb.append("] )");

    return sb.toString();
  }  
  public int upCount() {
    return ups;
  }  
}

---