package listeners;

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

/**
 * This listener prints the state space.
 * 
 * @author Franck van Breugel
 */
public class StateSpace extends ListenerAdapter {
	private int previous; // id of current state
	private int current; // id of previous state
	
	/**
	 * Initializes this listener.
	 */
	public StateSpace () {
		this.previous = -1; // -1 represents undefined
		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) {
			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();
	}
}