import java.io.FileNotFoundException;
import java.io.PrintWriter;

import gov.nasa.jpf.JPFListener;
import gov.nasa.jpf.ListenerAdapter;
import gov.nasa.jpf.search.Search;

public class StateSpace extends ListenerAdapter implements JPFListener 
{
	private int previous;
	private PrintWriter writer;
	
	public StateSpace() 
	{
		this.previous = -1;
		try 
		{
			this.writer = new PrintWriter("state-space.dot");
		} 
		catch (FileNotFoundException e) 
		{
			e.printStackTrace();
		}
	}
	
	public void stateAdvanced(Search search) 
	{
		int current = search.getStateId();
		if (this.previous != -1) 
		{
			this.writer.printf("%d -> %d%n", this.previous, current);
		}
		if (search.isEndState())
		{
			this.writer.printf("%d [fillcolor=red]%n", current);
		}
		this.previous = current;
	}
	
	public void stateBacktracked(Search search) 
	{
		this.previous = search.getStateId();
	}
	
	public void stateRestored(Search search) 
	{
		this.previous = search.getStateId();
	}
	
	public void searchStarted(Search search) 
	{
		this.writer.println("digraph statespace {");
		this.writer.println("node [style=filled]");
		this.writer.println("0 [fillcolor=green]");
	}
	
	public void searchFinished(Search search) 
	{
		this.writer.println("}");
		this.writer.close();
	}
}