package listeners;

import java.io.FileNotFoundException;
import java.io.PrintWriter;
import gov.nasa.jpf.ListenerAdapter;
import gov.nasa.jpf.search.Search;
import gov.nasa.jpf.search.SearchListener;

/**
 * This listener produces a dot file representing the state space.
 * 
 * @author Franck van Breugel
 */
public class StateSpace extends ListenerAdapter implements SearchListener {
	private int previous; // ID of previous state
	private int current; // ID of current state
	private PrintWriter writer;
	
	/**
	 * Initializes this listener.
	 */
	public StateSpace () {
		this.previous = -1; // -1 is the ID of the initial state
		this.current = -1;
	}
	
	/**
	 * Whenever JPF traverses a transition, writes the transition to the dot file.
	 * 
	 * @param search JPF's search.
	 */
	public void stateAdvanced(Search search) {
		this.previous = this.current;
		this.current = search.getStateId();
		
		if (this.previous != -1) { // the very first transition is not written to file
			this.writer.printf("%d -> %d%n", this.previous, this.current);
		}
	}
	
	/**
	 * Whenever JPF backtracks, updates information needed for this listener.
	 * 
	 * @param search JPF's search.
	 */
	public void stateBacktracked(Search search) {
		this.current = search.getStateId();
	}
	
	/**
	 * Whenever JPF restores an earlier visited state, updates information 
	 * needed for this listener.
	 * 
	 * @param search JPF's search.
	 */
	public void stateRestored(Search search) {
		this.current = search.getStateId();
	}
	
	/**
	 * When JPF starts, opens the dot file.
	 * 
	 * @param search JPF's search.
	 */
	public void searchStarted(Search search) {
		try {
			this.writer = new PrintWriter("statespace.dot");
			this.writer.println("digraph statespace {");
		} catch (FileNotFoundException e) {
			e.printStackTrace();
			search.terminate();
		}
	}
	
	/**
	 * When JPF finishes, closes the dot file.
	 * 
	 * @param search JPF's search.
	 */
	public void searchFinished(Search search) {
		this.writer.println("}");
		this.writer.close();
	}
}