X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=blobdiff_plain;f=src%2Fmain%2Fgov%2Fnasa%2Fjpf%2Flistener%2FStateReducer.java;h=60782a98e9b73615789c937a80326eaee3fbbfdd;hp=5dbe79dc4ab8f7c59b2f90b8ec423c8b7f217580;hb=75c00d3f11e45587f0919d4c7de84a2249d1567e;hpb=564ad9103d56228149eaeea0b978de4f7bd73c59;ds=sidebyside

diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java
index 5dbe79d..60782a9 100644
--- a/src/main/gov/nasa/jpf/listener/StateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/StateReducer.java
@@ -33,60 +33,65 @@ import java.io.PrintWriter;
 
 import java.util.*;
 
+// TODO: Fix for Groovy's model-checking
+// TODO: This is a listener created to detect device conflicts and global variable conflicts
 /**
- * simple tool to log state changes
+ * Simple listener tool to track remove unwanted ChoiceGenerators that are registered
+ * while an existing ChoiceGenerator is being explored. Multiple ChoiceGenerators of the same
+ * type could be registered spuriously during a while(true) loop.
  */
 public class StateReducer extends ListenerAdapter {
 
+  private boolean debugMode;
   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);
+  private String detail;
+  private int depth;
+  private int id;
+  private Transition transition;
+
+  // Holds values that have appeared during CG advances
+  private HashSet<Integer> cgChoiceSet;
+  private Integer choiceUpperBound;
+  private boolean isInitialized;
+
+  public StateReducer (Config config, JPF jpf) {
+    debugMode = config.getBoolean("debug_state_transition", false);
+    if (debugMode) {
+      out = new PrintWriter(System.out, true);
+    } else {
+      out = null;
+    }
+    detail = null;
+    depth = 0;
+    id = 0;
+    transition = null;
+    cgChoiceSet = new HashSet<>();
+    choiceUpperBound = 0;
+    isInitialized = false;
   }
 
   @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();
+    if (debugMode) {
+      id = search.getStateId();
+      depth = search.getDepth();
+      transition = search.getTransition();
+      detail = null;
+      out.println("\n==> DEBUG: The state is restored to state with id: " + id + " -- Transition: " + transition +
+              " and depth: " + depth + "\n");
     }
-    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");
+    if (debugMode) {
+      out.println("\n==> DEBUG: ----------------------------------- search started" + "\n");
+    }
   }
 
-  // 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;
@@ -123,55 +128,42 @@ public class StateReducer extends ListenerAdapter {
 
   @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 (debugMode) {
+      id = search.getStateId();
+      depth = search.getDepth();
+      transition = search.getTransition();
+      if (search.isNewState()) {
+        detail = "new";
+      } else {
+        detail = "visited";
+      }
 
-    if (search.isEndState()) {
-      detail += " end";
+      if (search.isEndState()) {
+        out.println("\n==> DEBUG: This is the last state!\n");
+        detail += " end";
+      }
+      out.println("\n==> DEBUG: The state is forwarded to state with id: " + id + " with depth: " + depth +
+              " which is " + detail + " Transition: " + transition + "\n");
     }
   }
 
   @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();
+    if (debugMode) {
+      id = search.getStateId();
+      depth = search.getDepth();
+      transition = search.getTransition();
+      detail = null;
+
+      out.println("\n==> DEBUG: The state is backtracked to state with id: " + id + " -- Transition: " + transition +
+              " and depth: " + depth + "\n");
     }
-    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");
+    if (debugMode) {
+      out.println("\n==> DEBUG: ----------------------------------- search finished" + "\n");
+    }
   }
 }
\ No newline at end of file