LogEntry.java

package edu.udel.cis.vsl.tass.log.impl;

import java.io.PrintWriter;
import java.util.Arrays;
import java.util.Collection;
import java.util.HashSet;
import java.util.Set;

import edu.udel.cis.vsl.tass.config.VerifyConfiguration;
import edu.udel.cis.vsl.tass.semantics.IF.ExecutionException;
import edu.udel.cis.vsl.tass.semantics.IF.ExecutionProblem;
import edu.udel.cis.vsl.tass.semantics.IF.ExecutionStateException;

/**
 * A log entry represents the report of a single error discovered the
 * verification of a model or the comparison of two models.
 */
public class LogEntry {

	/** The id number of this log entry, unique within the log. */
	private int id;

	/**
	 * A measure of the size of the counterexample. For a single model, the
	 * length of the trace. For a model pair, the sum of the lenghts of the
	 * traces.
	 */
	private int size;

	/**
	 * The problem being logged. An instance of either ExecutionStateException
	 * or ExecutionException.
	 */
	private ExecutionProblem problem;

	/** The log to which this entry belongs */
	private ErrorLog log;

	private int hashCode;

	private Set<String> filenameSet = new HashSet<String>();

	public LogEntry(ErrorLog log, ExecutionProblem problem, int size) {
		this.log = log;
		this.id = -1;
		this.problem = problem;
		this.size = size;
		this.hashCode = computeHashCode();

	}

	public boolean isVerification() {
		return log.configuration() instanceof VerifyConfiguration;
	}

	public void setId(int id) {
		this.id = id;
	}

	public int id() {
		return id;
	}

	public int size() {
		return size;
	}

	public ErrorLog log() {
		return log;
	}

	public ExecutionProblem problem() {
		return problem;
	}

	/** Adds a filename to the list of associated files for this log entry */
	public void addFilename(String filename) {
		filenameSet.add(filename);
	}

	/** Returns the set of filenames associated to this log entry. */
	public Collection<String> filenames() {
		return filenameSet;
	}

	public boolean equals(Object object) {
		if (object instanceof LogEntry) {
			LogEntry that = (LogEntry) object;

			if (problem.kind() != that.problem.kind())
				return false;
			if (problem instanceof ExecutionException) {
				if (!(that.problem instanceof ExecutionException))
					return false;
				return ((ExecutionException) problem).element().equals(
						((ExecutionException) that.problem).element());
			} else if (problem instanceof ExecutionStateException) {
				if (!(that.problem instanceof ExecutionStateException))
					return false;
				return Arrays.equals(((ExecutionStateException) problem)
						.locations(), ((ExecutionStateException) that.problem)
						.locations());
			} else {
				throw new RuntimeException(
						"TASS internal error: unknown kind of execution problem: "
								+ problem);
			}
		}
		return false;
	}

	public int hashCode() {
		return hashCode;
	}

	private int computeHashCode() {
		int result = problem.kind().hashCode();

		if (problem instanceof ExecutionException) {
			result = ((ExecutionException) problem).element().hashCode();
		} else if (problem instanceof ExecutionStateException) {
			result = Arrays.hashCode(((ExecutionStateException) problem)
					.locations());
		} else {
			throw new RuntimeException(
					"TASS internal error: unknown kind of execution problem: "
							+ problem);
		}
		return result;
	}

	public void print(PrintWriter out) {
		boolean first = true;

		out.print("Error " + id + ": ");
		out.print(problem);
		out.println();
		if (filenameSet.isEmpty()) {
			out.print("Encountered in initial state.");
		} else {
			out.print("Trace logged in ");
			for (String filename : filenameSet) {
				if (!first) {
					out.print(", ");
				}
				out.print(filename);
				first = false;
			}
		}
		out.println();
		out.flush();
	}
}