package search;

import gov.nasa.jpf.Config;
import gov.nasa.jpf.search.Search;
import gov.nasa.jpf.search.SearchListener;

import java.io.FileNotFoundException;
import java.io.FileOutputStream;
import java.io.IOException;
import java.io.ObjectOutputStream;
import java.util.ArrayList;
import java.util.List;

/**
 * Records the notifications of a search as a serialized list of strings.
 * If any notification follows the searchFinished notification, then 
 * an error is reported.
 * 
 * @author Franck van Breugel
 */
public class SearchNotificationRecorder implements SearchListener {
	private List<String> recording; // notifications
	private boolean finished; // has finish been notified
	private String fileName; // name of file containing serialization

	/**
	 * Initializes this notification recorder.
	 * 
	 * @exception FileNotFoundException if file for serialization could
	 * not be set up
	 */
	public SearchNotificationRecorder(Config config) {
		this.recording = new ArrayList<String>();
		this.finished = false;
		this.fileName = config.getString("recorder.file", "tmp.ser");
	}

	/**
	 * When the search starts, report its notification.
	 * 
	 * @param search JPF's search
	 */
	public void searchStarted(Search search) {
		this.recording.add("started in state " + search.getStateId());
		this.checkFinished();
	}

	/**
	 * Whenever the search is probed, report its notification.
	 * 
	 * @param search JPF's search
	 */
	public void searchProbed(Search search) {
		this.recording.add("probed in state " + search.getStateId());
		this.checkFinished();
	}

	/**
	 * When the search finishes, report its notification.
	 * 
	 * @param search JPF's search
	 */
	public void searchFinished(Search search) {
		this.recording.add("finished in state " + search.getStateId());
		this.finished = true;
		this.serialize();
	}

	/**
	 * Whenever the search advanced to a new state, report its notification.
	 * 
	 * @param search JPF's search
	 */
	public void stateAdvanced(Search search) {
		this.recording.add("advanced to state " + search.getStateId());
		this.checkFinished();
	}

	/**
	 * Whenever the search backtracks, report its notification.
	 * 
	 * @param search JPF's search
	 */
	public void stateBacktracked(Search search) {
		this.recording.add("backtracked to state " + search.getStateId());
		this.checkFinished();
	}

	/**
	 * Whenever the search has fully processed a state, report its notification.
	 * 
	 * @param search JPF's search
	 */
	public void stateProcessed(Search search) {
		this.recording.add("processed state " + search.getStateId());
		this.checkFinished();
	}

	/**
	 * Whenever the search stores a state, report its notification.
	 * 
	 * @param search JPF's search
	 */
	public void stateStored(Search search) {
		this.recording.add("stored state " + search.getStateId());
		this.checkFinished();
	}

	/**
	 * Whenever the search stores a state, report its notification.
	 * 
	 * @param search JPF's search
	 */
	public void stateRestored(Search search) {
		this.recording.add("restored state " + search.getStateId());
		this.checkFinished();
	}

	/**
	 * Whenever the search restores a state, report its notification.
	 * 
	 * @param search JPF's search
	 */
	public void statePurged(Search search) {
		this.recording.add("purged state " + search.getStateId());
		this.checkFinished();
	}

	/**
	 * Whenever the search observes the violation of a property, report 
	 * its notification.
	 * 
	 * @param search JPF's search
	 */
	public void propertyViolated(Search search) {
		String error = search.getCurrentError().getProperty().toString();
		// remove trailing @...
		int index = error.indexOf("@");
		if (index >= 0) {
			error = error.substring(0, index);
		}
		this.recording.add("violated property " + error);
		this.checkFinished();
	}

	/**
	 * Whenever the search observes that a constraint is violated, report 
	 * its notification.
	 * 
	 * @param search JPF's search
	 */
	public void searchConstraintHit(Search search) {
		this.recording.add("hit constraint " + search.getLastSearchConstraint());
		this.checkFinished();
	}

	/**
	 * Prints an error message whenever searchFinished is not the last 
	 * notification of the search.
	 */
	private void checkFinished() {
		if (this.finished) {
			System.out.println("searchFinished is not the last notification of the search");
			this.serialize();
		}
	}

	/**
	 * Serializes the recording.
	 */
	private void serialize() {
		try {
			FileOutputStream output = new FileOutputStream(this.fileName);
			ObjectOutputStream stream = new ObjectOutputStream(output);
			stream.writeObject(this.recording);
			stream.close();
			output.close();
		} catch (IOException e) {
			System.out.println("SearchNotificationRecorder failed");
		}
	}
}