ErrorLog.java

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

import java.io.File;
import java.io.FileNotFoundException;
import java.io.PrintWriter;
import java.util.LinkedHashMap;
import java.util.Map;
import java.util.Stack;

import edu.udel.cis.vsl.tass.config.CompareConfiguration;
import edu.udel.cis.vsl.tass.config.RunConfiguration;
import edu.udel.cis.vsl.tass.config.VerifyConfiguration;
import edu.udel.cis.vsl.tass.log.IF.ErrorLogIF;
import edu.udel.cis.vsl.tass.log.IF.ExcessiveErrorException;
import edu.udel.cis.vsl.tass.model.IF.ModelIF;
import edu.udel.cis.vsl.tass.search.DfsSearcher;
import edu.udel.cis.vsl.tass.semantics.IF.ExecutionException;
import edu.udel.cis.vsl.tass.semantics.IF.ExecutionStateException;
import edu.udel.cis.vsl.tass.state.IF.StateIF;
import edu.udel.cis.vsl.tass.transition.IF.TransitionIF;
import edu.udel.cis.vsl.tass.transition.IF.TransitionSequenceIF;

public class ErrorLog implements ErrorLogIF {
	/**
	 * The number of models involved. 1 if this is a log for a verification run
	 * (single model). 2 if this is a log for a comparison run (two models).
	 */
	private int numModels;

	/** An array of length numModels. */
	private ModelIF[] models;

	// private DynamicFactoryIF dynamicFactory;

	// private TASSStateManagerIF stateManager;

	private RunConfiguration configuration;

	private Map<LogEntry, LogEntry> entryMap = new LinkedHashMap<LogEntry, LogEntry>();

	private DfsSearcher<StateIF, TransitionIF, TransitionSequenceIF> searcher;

	private int numEntries = 0;

	private PrintWriter out;

	private String line = "--------------------------------------------------------------------------------";

	private int numReports = 0;

	private int errorBound = 1;

	// private boolean concretizeDebug = false;

	private ErrorLog(RunConfiguration configuration, ModelIF[] models) {
		this.configuration = configuration;
		this.models = models;
		this.searcher = null;
		this.out = configuration.out();
		this.numModels = models.length;
	}

	public ErrorLog(VerifyConfiguration configuration, ModelIF model) {
		this(configuration, new ModelIF[] { model });
	}

	public ErrorLog(CompareConfiguration configuration, ModelIF specModel,
			ModelIF implModel) {
		this(configuration, new ModelIF[] { specModel, implModel });
	}

	@Override
	public String name() {
		if (searcher == null)
			return null;
		else
			return searcher.name();
	}

	@Override
	public void setSearcher(
			DfsSearcher<StateIF, TransitionIF, TransitionSequenceIF> searcher) {
		this.searcher = searcher;
	}

	@Override
	public void setErrorBound(int bound) {
		this.errorBound = bound;
	}

	@Override
	public RunConfiguration configuration() {
		return configuration;
	}

	@Override
	public int numErrors() {
		return entryMap.size();
	}

	@Override
	public int numReports() {
		return numReports;
	}

	private void processLogEntry(LogEntry entry) {
		LogEntry oldEntry = entryMap.get(entry);

		numReports++;
		out.println("\n ************ ERROR DETECTED ************\n"
				+ entry.problem());
		out.flush();
		if (oldEntry != null) {
			if (entry.size() >= oldEntry.size()) {
				out
						.println("Previously found error is shorter: ignore thing one.\n");
				return;
			}
			entry.setId(oldEntry.id());
		}
		if (entry.id() < 0) {
			entry.setId(numEntries);
			numEntries++;
			entryMap.put(entry, entry);
		}
		if (searcher == null) {
			out.println("Encountered in initial state.\n");
			return;
		}
		if (!configuration.replay())
			try {
				String traceFilename = name() + "_" + entry.id() + ".trace";
				File traceFile;
				PrintWriter traceOut;

				entry.addFilename(traceFilename);
				traceFile = new File(configuration.workingDirectory(),
						traceFilename);
				traceOut = new PrintWriter(traceFile);
				out.print("Writing trace to " + traceFilename + "...");
				out.flush();
				// searcher.printStack(traceOut);
				writeTrace(traceOut);
				// findModel(models[0].inputVariables(),
				// searcher.currentState());
				out.println("done.\n");
				out.flush();
				traceOut.close();
			} catch (FileNotFoundException e) {
				out.println("Unable to open file for writing...exiting...");
				print(out);
				throw new RuntimeException(
						"TASS: Exiting due to inability to open log file.");
			}
	}

	private void writeTrace(PrintWriter traceOut) {
		RunConfiguration newConfiguration = configuration.clone();
		Stack<TransitionSequenceIF> stack = searcher.stack();
		int stackSize = stack.size();

		newConfiguration.setErrorBound(numErrors());
		newConfiguration.write(traceOut);
		traceOut.println();
		for (int i = 0; i < stackSize; i++) {
			TransitionSequenceIF sequence = stack.elementAt(i);

			if (sequence.isMultiple())
				traceOut.println(sequence.index());
		}
	}

	@Override
	public void report(ExecutionException error) {
		int size = (searcher == null ? 0 : searcher.stack().size());
		processLogEntry(new LogEntry(this, error, size));
		considerQuitting();
	}

	@Override
	public void report(ExecutionStateException error) {
		int size = (searcher == null ? 0 : searcher.stack().size());
		processLogEntry(new LogEntry(this, error, size));
		considerQuitting();
	}

	private void considerQuitting() {
		int numErrors = numErrors();

		if (numErrors >= errorBound) {
			throw new ExcessiveErrorException(numErrors);
		}
	}

	@Override
	public void writeModels() throws FileNotFoundException {
		for (int i = 0; i < numModels; i++) {
			ModelIF model = models[i];

			String modelFilename = model.name() + ".model";
			File modelFile = new File(configuration.workingDirectory(),
					modelFilename);
			PrintWriter modelOut = new PrintWriter(modelFile);

			out.print("Writing model " + modelFilename + "...");
			out.flush();
			model.print(modelOut, true);
			modelOut.close();
			out.println("done.");
			out.flush();
		}
	}

	@Override
	public void print(PrintWriter out) {
		out
				.println("================================ TASS Error Log ================================");
		configuration.print(out);
		out.println();
		out.println("Number of errors reported........... " + numReports());
		out.println("Number of distinct errors........... " + numErrors());
		out.println();
		out.println(line);
		for (LogEntry entry : entryMap.values()) {
			out.println();
			entry.print(out);
			out.println();
			out.println(line);
		}
		out.flush();
	}

	@Override
	public void print() throws FileNotFoundException {
		String filename = "TASS_LOG-";

		for (int i = 0; i < numModels; i++) {
			if (i > 0)
				filename += "-";
			filename += models[i].name();
		}
		filename += ".txt";
		PrintWriter writer = new PrintWriter(new File(configuration
				.workingDirectory(), filename));
		print(writer);
		writer.close();
	}

	// private Map<SharedVariableIF, ValueIF> findModel(
	// Collection<SharedVariableIF> inputVariables, StateIF state) {
	// if (state == null) {
	// System.err.println("State was null during concretization.");
	// return null;
	// }
	// if (concretizeDebug) {
	// System.out.println("Input Variables: " + inputVariables);
	// System.out.println("Input Variable Cells: "
	// + dynamicFactory.getSharedVariableCells(inputVariables));
	// }
	// if (!inputVariables.isEmpty()) {
	// Map<SharedVariableIF, ValueIF> valueMap = stateManager
	// .getSharedVariableValues(dynamicFactory
	// .getSharedVariableCells(inputVariables), state);
	// ValueIF pathCondition = stateManager.getPathCondition(state);
	// if (pathCondition != null && !valueMap.isEmpty())
	// try {
	// ValueIF model = dynamicFactory.findModel(pathCondition);
	// System.out.println("Concretized path condition: " + model);
	// if (model != null) {
	// DynamicSimplifierIF simplifier = dynamicFactory
	// .simplifier(model, dynamicFactory
	// .simplifyCache());
	// Set<Entry<SharedVariableIF, ValueIF>> entrySet = valueMap
	// .entrySet();
	// if (concretizeDebug)
	// for (Entry<SharedVariableIF, ValueIF> entry : entrySet) {
	// System.out
	// .println("Variable: "
	// + entry.getKey()
	// + " Value: "
	// + entry.getValue()
	// + " Simplified: "
	// + simplifier.simplify(entry
	// .getValue()));
	// }
	// }
	// } catch (DynamicException e) {
	// // TODO Auto-generated catch block
	// e.printStackTrace();
	// }
	// }
	// return null;
	// }
	//
	// public void setStateManager(TASSStateManagerIF stateManager) {
	// this.stateManager = stateManager;
	// }

	// public void setDynamicFactory(DynamicFactoryIF dynamicFactory) {
	// this.dynamicFactory = dynamicFactory;
	// }

}