package listeners;

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

/**
 * This listener prints the state space.
 * 
 * @author Franck van Breugel
 */
public class StateSpace extends ListenerAdapter implements SearchListener {
	private int previous; // ID of prvious state
	private int current; // ID of current state
	
	/**
	 * Initializes this listener.
	 */
	public StateSpace () {
		this.previous = -1; // -1 is the ID of the initial state
		this.current = -1;
	}
	
	/**
	 * Whenever JPF traverses a transition, prints the transition.
	 * 
	 * @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 printed
			System.out.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();
	}
}