import gov.nasa.jpf.Config;
import gov.nasa.jpf.JPF;
import gov.nasa.jpf.JPFListener;
import gov.nasa.jpf.ListenerAdapter;
import gov.nasa.jpf.report.Publisher;
import gov.nasa.jpf.report.PublisherExtension;
import gov.nasa.jpf.search.Search;

//This code only works with BFS
//To get the XML file in the lecture
//set search.class=gov.nasa.jpf.search.heuristic.BFSHeuristic

public class StateSpaceXML extends ListenerAdapter implements PublisherExtension, JPFListener {
	int source;
	int target;

	PrintWriter pw;
	Set<Integer> setOfStates;

	public StateSpaceXML(Config config, JPF jpf) {
		source = -1;
		target = -1;
		setOfStates = new HashSet<Integer>();
		jpf.addPublisherExtension(Publisher.class, this);
	}

	@Override
	public void publishStart(Publisher publisher) {
		publisher.publishTopicStart("state_space");
	}

	@Override
	public void publishFinished(Publisher publisher) {
		publisher.publishTopicEnd("state");
		publisher.publishTopicEnd("state_space");
	}

	@Override
	public void publishTransition(Publisher publisher) {
		if (this.source != -1) {
			if (!this.setOfStates.contains(this.source)) {
				if (this.source != 0) {
					publisher.publishTopicEnd("state");
				}
				this.setOfStates.add(this.source);
				publisher.publishTopicStart("state id =" + this.source);

			}
			publisher.publishTopicStart("transition target = " + this.target);
			publisher.publishTopicEnd("transition");
		}
	}

	@Override
	public void stateAdvanced(Search search) {
		this.source = this.target;
		this.target = search.getStateId();

	}

	@Override
	public void stateBacktracked(Search search) {
		this.target = search.getStateId();
	}

	@Override
	public void stateRestored(Search search) {
		this.target = search.getStateId();
	}

}