package listeners;

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

/**
 * For each event triggered by JPF's search, prints the sort of event
 * and the ID of the state of the search in which the event occurs.
 * 
 * @author Franck van Breugel
 */
public class SearchEvents implements SearchListener {
	/**
	 * Whenever JPF traverses a transition, prints a description of the event and 
	 * the ID of the state of the search in which the event occurs.
	 * 
	 * @param search JPF's search.
	 */
    public void stateAdvanced(Search search) {
        System.out.println("advanced to state " + search.getStateId());
    }

    /**
	 * Whenever JPF has fully explored a state, prints a description of the event and 
	 * the ID of the state of the search in which the event occurs.
	 * 
	 * @param search JPF's search.
	 */
    public void stateProcessed(Search search) {
        System.out.println("state " + search.getStateId() + " processed");
    }

    /**
	 * Whenever JPF backtracks, prints a description of the event and 
	 * the ID of the state of the search in which the event occurs.
	 * 
	 * @param search JPF's search.
	 */
    public void stateBacktracked(Search search) {
        System.out.println("backtracked to state " + search.getStateId());
    }

    /**
	 * Whenever JPF purges a state, prints a description of the event and 
	 * the ID of the state of the search in which the event occurs.
	 * 
	 * @param search JPF's search.
	 */
    public void statePurged(Search search) {
        System.out.println("state " + search.getStateId() + " purged");
    }

    /**
	 * Whenever JPF stores a state, prints a description of the event and 
	 * the ID of the state of the search in which the event occurs.
	 * 
	 * @param search JPF's search.
	 */
    public void stateStored(Search search) {
        System.out.println("state " + search.getStateId() + " stored");
    }

    /**
	 * Whenever JPF restores a state, prints a description of the event and 
	 * the ID of the state of the search in which the event occurs.
	 * 
	 * @param search JPF's search.
	 */
    public void stateRestored(Search search) {
        System.out.println("state " + search.getStateId() + " restored");
    }

    /**
	 * Whenever JPF's search is probed, prints a description of the event and 
	 * the ID of the state of the search in which the event occurs.
	 * 
	 * @param search JPF's search.
	 */
    public void searchProbed(Search search) {
        System.out.println("search probed in state " + search.getStateId());
    }

    /**
	 * Whenever JPF detects a property violation, prints a description of the event and 
	 * the ID of the state of the search in which the event occurs.
	 * 
	 * @param search JPF's search.
	 */
    public void propertyViolated(Search search) {
        System.out.println("property violated in state " + search.getStateId());
    }

    /**
	 * Whenever JPF detects that a constraint is hit, prints a description of the event and 
	 * the ID of the state of the search in which the event occurs.
	 * 
	 * @param search JPF's search.
	 */
    public void searchConstraintHit(Search search) {
        System.out.println("search constraint hit in state " + search.getStateId());
    }

    /**
	 * When the search starts, prints a description of the event and 
	 * the ID of the state of the search in which the event occurs.
	 * 
	 * @param search JPF's search.
	 */
    public void searchStarted(Search search) {
        System.out.println("search started in state " + search.getStateId());
    }

    /**
	 * When the search finishes, prints a description of the event and 
	 * the ID of the state of the search in which the event occurs.
	 * 
	 * @param search JPF's search.
	 */
    public void searchFinished(Search search) {
        System.out.println("search finished in state " + search.getStateId());
    }
}