First version of the StateReducer class.

diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java
new file mode 100644 (file)
index 0000000..5dbe79d
--- /dev/null
+++ b/src/main/gov/nasa/jpf/listener/StateReducer.java
@@ -0,0 +1,177 @@
+/*
+ * 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