--- /dev/null
+/*
+ * Copyright (C) 2014, United States Government, as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The Java Pathfinder core (jpf-core) platform is licensed under the
+ * Apache License, Version 2.0 (the "License"); you may not use this file except
+ * in compliance with the License. You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0.
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package gov.nasa.jpf.listener;
+
+import gov.nasa.jpf.Config;
+import gov.nasa.jpf.JPF;
+import gov.nasa.jpf.ListenerAdapter;
+import gov.nasa.jpf.search.Search;
+import gov.nasa.jpf.jvm.bytecode.*;
+import gov.nasa.jpf.vm.*;
+import gov.nasa.jpf.vm.bytecode.LocalVariableInstruction;
+import gov.nasa.jpf.vm.bytecode.ReadInstruction;
+import gov.nasa.jpf.vm.bytecode.StoreInstruction;
+import gov.nasa.jpf.vm.bytecode.WriteInstruction;
+import gov.nasa.jpf.vm.choice.IntIntervalGenerator;
+
+import java.io.PrintWriter;
+
+import java.util.*;
+
+/**
+ * simple tool to log state changes
+ */
+public class StateReducer extends ListenerAdapter {
+
+ private final PrintWriter out;
+ volatile private String valueVarLock = "";
+ volatile private String valueVarContact = "";
+ volatile private String operation;
+ volatile private String detail;
+ volatile private int depth;
+ volatile private int id;
+ Transition transition;
+ Object annotation;
+ String label;
+ String output;
+ int stateId;
+
+
+ public StateReducer (Config conf, JPF jpf) {
+ out = new PrintWriter(System.out, true);
+ }
+
+ @Override
+ public void stateRestored(Search search) {
+ id = search.getStateId();
+ depth = search.getDepth();
+ operation = "restored";
+ transition = search.getTransition();
+ if (transition != null) {
+ annotation = transition.getAnnotation();
+ label = transition.getLabel();
+ output = transition.getOutput();
+ stateId = transition.getStateId();
+ }
+ detail = null;
+
+ out.println("\nThe state is restored to state with id: "+id+" Transition: "+transition+", with depth: "+depth+"##LockValue: "+valueVarLock+", ##ContactValue: "+valueVarContact +"\n");
+ }
+
+ //--- the ones we are interested in
+ @Override
+ public void searchStarted(Search search) {
+ out.println("----------------------------------- search started");
+ }
+
+ // Holds values that have appeared during CG advances
+ private HashSet<Integer> cgChoiceSet = new HashSet<>();
+ private Integer choiceUpperBound = 0;
+ private boolean isInitialized = false;
+
+ @Override
+ public void choiceGeneratorSet (VM vm, ChoiceGenerator<?> newCG) {
+
+ // Initialize with necessary information from the CG
+ if (newCG instanceof IntIntervalGenerator) {
+ IntIntervalGenerator iigCG = (IntIntervalGenerator) newCG;
+ // Check if CG has been initialized, otherwise initialize it
+ if (!isInitialized) {
+ Integer[] choices = iigCG.getChoices();
+ // Get the upper bound from the last element of the choices
+ choiceUpperBound = choices[choices.length - 1];
+ isInitialized = true;
+ } else {
+ newCG.setDone();
+ }
+ }
+ }
+
+ @Override
+ public void choiceGeneratorAdvanced (VM vm, ChoiceGenerator<?> currentCG) {
+ // Check every choice generated and make sure that all the available choices
+ // are chosen first before repeating the same choice of value twice!
+ if (currentCG instanceof IntIntervalGenerator) {
+ IntIntervalGenerator iigCG = (IntIntervalGenerator) currentCG;
+ Integer nextChoice = iigCG.getNextChoice();
+ if (!cgChoiceSet.contains(nextChoice)) {
+ cgChoiceSet.add(nextChoice);
+ }
+ // Allow reinitialization after an upper bound is hit
+ // This means all available choices have been explored once during this iteration
+ if (cgChoiceSet.contains(choiceUpperBound)) {
+ isInitialized = false;
+ cgChoiceSet.clear();
+ }
+ }
+ }
+
+ @Override
+ public void stateAdvanced(Search search) {
+ String theEnd = null;
+ id = search.getStateId();
+ depth = search.getDepth();
+ operation = "forward";
+ transition = search.getTransition();
+ if (transition != null) {
+ annotation = transition.getAnnotation();
+ label = transition.getLabel();
+ output = transition.getOutput();
+ stateId = transition.getStateId();
+ }
+ if (search.isNewState()) {
+ detail = "new";
+ } else {
+ detail = "visited";
+ }
+
+ if (search.isEndState()) {
+ out.println("This is the last state!");
+ theEnd = "end";
+ }
+
+ //out.println("stateId: "+stateId+", output: "+output+", label: "+label);
+ out.println("\nThe state is forwarded to state with id: "+id+", with depth: "+depth+" which is "+detail+" Transition: "+transition+" state: "+"% "+theEnd+"##LockValue: "+valueVarLock+", ##ContactValue: "+valueVarContact +"\n");
+
+ if (search.isEndState()) {
+ detail += " end";
+ }
+ }
+
+ @Override
+ public void stateBacktracked(Search search) {
+ id = search.getStateId();
+ depth = search.getDepth();
+ operation = "backtrack";
+ transition = search.getTransition();
+ if (transition != null) {
+ annotation = transition.getAnnotation();
+ label = transition.getLabel();
+ output = transition.getOutput();
+ stateId = transition.getStateId();
+ }
+ detail = null;
+
+ out.println("\nThe state is backtracked to state with id: "+id+" Transition: "+ transition+", with depth: "+depth+"##LockValue: "+valueVarLock+", ##ContactValue: "+valueVarContact +"\n");
+ }
+
+ @Override
+ public void searchFinished(Search search) {
+ out.println("----------------------------------- search finished");
+ }
+}
\ No newline at end of file