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 source;
	private int target;
	private PrintWriter writer;

	public StateSpace() 
	{
		this.source = -1;
		this.target = -1;
		try 
		{
			this.writer = new PrintWriter("state-space.dot");
		} 
		catch (FileNotFoundException e) 
		{
			e.printStackTrace();
		}
	}
	
	public void stateAdvanced(Search search) 
	{
		this.source = this.target;
		this.target = search.getStateId();
		if (this.source != -1) 
		{
			this.writer.printf("%d -> %d%n", this.source, this.target);
		}
	}
	
	public void stateBacktracked(Search search) 
	{
		this.target = search.getStateId();
	}
	
	public void stateRestored(Search search) 
	{
		this.target = search.getStateId();
	}

	public void searchStarted(Search search) 
	{
		this.writer.println("digraph statespace {");
	}
	
	public void searchFinished(Search search) 
	{
		this.writer.println("}");
		this.writer.close();
	}
}