---

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.jpf.ByteArray;
import gov.nasa.arc.ase.util.Debug;
import java.io.Serializable;

public class JVMPath implements Path, Serializable {
  private JVMPathEntry[] moves;
  private int ups;

  public JVMPath(byte[] data) {
    ByteArray a = new ByteArray(data);

    int u = a.unpackInt();
    int m = a.unpackInt();

    init(m, u);

    for(int i = 0; i < m; i++) {
      int thread = a.unpackInt();
      int random = a.unpackInt();

      set(i, new JVMPathEntry(0, null, thread, random));
    }
  }  
  JVMPath(int m) {
    init(m, 0);
  }  
  JVMPath(int m, int u) {
    init(m, u);
  }  
  public Path append(Path o) {
    if(o == null) return (Path)clone();
    if(!(o instanceof JVMPath))
      throw new IllegalArgumentException("o must be a JVMPath");

    JVMPath p = (JVMPath)o;
    JVMPathEntry[] m1 = moves;
    JVMPathEntry[] m2 = p.moves;
    int l1 = m1.length;
    int l2 = m2.length;
    int u1 = ups;
    int u2 = p.ups;

    int l, u, d;
    
    if(l1 > u2) {
      d = l1 - u2;
      u = u1;
    } else {
      d = 0;
      u = u1 + u2 - l1;
    }
    l = d + l2;

    JVMPath n = new JVMPath(l, u);

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

    return n;
  }  
  public Object clone() {
    int l = moves.length;
    
    JVMPath p = new JVMPath(l, ups);

    for(int i = 0; i < l; i++)
      p.moves[i] = moves[i];

    return p;
  }  
  public boolean equals(Object o) {
    if(o == null) return false;
    if(!(o instanceof JVMPath)) return false;

    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].equals(moves[i]))
    return false;

    return true;
  }  
  public JVMPathEntry get(int index) {
    return moves[index];
  }  
  public byte[] getData() {
    ByteArray a = new ByteArray();

    a.pack(ups);
    a.pack(moves.length);

    for(int i = 0; i < moves.length; i++) {
      a.pack(moves[i].thread);
      a.pack(moves[i].random);
    }

    return a.getData();
  }  
  private void init(int m, int u) {
    moves = new JVMPathEntry[m];
    ups = u;
  }  
  public Path relativeTo(Path o) {
    if(o == null) return (Path)clone();
    if(!(o instanceof JVMPath))
      throw new IllegalArgumentException("o must be a JVMPath");

    JVMPath p = (JVMPath)o;
    JVMPathEntry[] m1 = moves;
    JVMPathEntry[] m2 = 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].equals(m2[idx]))
    common++;
      else
    break;

    JVMPath n = new JVMPath(l1 - common, l2 - common);

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

    return n;
  }  
  void set(int index, JVMPathEntry e) {
    moves[index] = e;
  }  
  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(", ");
      if(moves[i] == null)
    sb.append("<null>");
      else {
    sb.append("t");
    sb.append(moves[i].thread);
    sb.append("/r");
    sb.append(moves[i].random);
      }
    }

    sb.append("] )");

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

---