package listener;

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.  The name 
 * of the dot file is <name of system under test>.dot.
 * 
 * @author Franck van Breugel
 */
public class StateSpaceDot extends ListenerAdapter implements SearchListener {
	private int current; // ID of current state (before state advances)
	private PrintWriter writer;
	
	/**
	 * Initializes this listener.
	 */
	public StateSpaceDot() {
		this.current = -1; // -1 is the ID of the initial state
	}
	
	/**
	 * Whenever JPF traverses a transition, writes the transition to the dot file 
	 * and colors the target of the transition red if it is a final state.
	 * 
	 * @param search JPF's search.
	 */
	@Override
	public void stateAdvanced(Search search) {
		this.writer.printf("%d -> %d%n", this.current, search.getStateId());
		this.current = search.getStateId();
		if (search.isEndState()) {
			this.writer.printf("%d [fillcolor=red]%n", this.current);
		}
	}
	
	/**
	 * Whenever JPF backtracks, updates information needed for this listener.
	 * 
	 * @param search JPF's search.
	 */
	@Override
	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.
	 */
	@Override
	public void stateRestored(Search search) {
		this.current = search.getStateId();
	}
	
	/**
	 * When JPF starts, opens the dot file and colors the initial state green.
	 * 
	 * @param search JPF's search.
	 */
	public void searchStarted(Search search) {
		String name = search.getVM().getSUTName();
		
		try {
			this.writer = new PrintWriter(name + ".dot");
			this.writer.println("digraph statespace {");
			this.writer.println("node [style=filled]");
			this.writer.println("-1 [fillcolor=green]");
		} catch (FileNotFoundException e) {
			e.printStackTrace();
			search.terminate();
		}
	}
	
	/**
	 * When JPF finishes, closes the dot file.
	 * 
	 * @param search JPF's search.
	 */
	@Override
	public void searchFinished(Search search) {
		this.writer.println("}");
		this.writer.close();
	}
}