---

JVMPathEntry.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 JVMPathEntry implements Serializable {
  public int line;
  public String classname;
  public String file;
  public int thread;
  public int random;

  public JVMPathEntry(int l, String cname, int t, int r) {
    line = l;
    classname = cname;
    if(cname == null) {
      file = "<unknown>";
      classname = "<unknown>";
    } else {
      file = Source.locateSourceFile(ClassInfo.getClassInfo(cname).getSourceFileName());
      if(file == null) file = cname;
    }
    thread = t;
    random = r;
  }  
  public boolean equals(Object o) {
    if(o == null) return false;
    if(!(o instanceof JVMPathEntry)) return false;

    JVMPathEntry e = (JVMPathEntry)o;
    
    return thread == e.thread && random == e.random && line == e.line &&
      classname.equals(e.classname) && file.equals(e.file);
  }  
}

---