package gov.nasa.jpf.listener; import java.io.PrintWriter; import gov.nasa.jpf.Config; import gov.nasa.jpf.JPF; import gov.nasa.jpf.ListenerAdapter; import gov.nasa.jpf.report.Publisher; import gov.nasa.jpf.report.PublisherExtension; import gov.nasa.jpf.search.Search; import gov.nasa.jpf.search.SearchListener; public class StateSpacePrinter2 extends ListenerAdapter implements SearchListener, PublisherExtension { private int source; private int target; public StateSpacePrinter2(Config config, JPF jpf) { source = -1; target = -1; jpf.addPublisherExtension(Publisher.class, this); } @Override public void publishStart(Publisher publisher){ PrintWriter out = publisher.getOut(); out.println(""); } @Override public void publishTransition(Publisher publisher) { PrintWriter out = publisher.getOut(); if (source != -1) { out.println(" "); out.println(" "); out.println(" "); } } @Override public void publishFinished(Publisher publisher){ PrintWriter out = publisher.getOut(); out.println(""); } @Override public void stateAdvanced(Search search) { source = target; target = search.getStateId(); } @Override public void stateBacktracked(Search search) { target = search.getStateId(); } @Override public void stateRestored(Search search) { target = search.getStateId(); } }