Updating main.jpf; Cleaning up the StateReducer.

diff --git a/main.jpf b/main.jpf
index c1e04caa3a112f3021d70fc9d9b2e4dc8a1dbb0b..ce6708fe2e64f2943a4be0c861e8eef747fa4d1d 100644 (file)
--- a/main.jpf
+++ b/main.jpf
@@ -1,13 +1,15 @@
 target = main
 
 # This is the listener that can detect variable write-after-write conflicts
-listener=gov.nasa.jpf.listener.VariableConflictTracker
+#listener=gov.nasa.jpf.listener.VariableConflictTracker
+#listener=gov.nasa.jpf.listener.StateReducer
+listener=gov.nasa.jpf.listener.VariableConflictTracker,gov.nasa.jpf.listener.StateReducer
 
 # Potentially conflicting variables
 # Alarms
 #variables=currentAlarm
 # Locks
-#variables=currentLock
+variables=currentLock
 # Thermostats
 #variables=currentHeatingSetpoint,thermostatSetpoint,currentCoolingSetpoint,thermostatOperatingState,thermostatFanMode,currentThermostatMode
 # Switches
@@ -23,13 +25,16 @@ listener=gov.nasa.jpf.listener.VariableConflictTracker
 # Valves
 #variables=valve,valveLatestValue
 # Cameras
-variables=image,alarmState
+#variables=image,alarmState
                        
 # Potentially conflicting apps (we default to App1 and App2 for now)
 apps=App1,App2
 
 # Tracking the location.mode variable conflict
-track_location_var_conflict=true
+#track_location_var_conflict=true
+
+# Debug mode for StateReducer
+debug_state_transition=true
 
 # Timeout in minutes (default is 0 which means no timeout)
 timeout=30

diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java
index 5dbe79dc4ab8f7c59b2f90b8ec423c8b7f217580..60782a98e9b73615789c937a80326eaee3fbbfdd 100644 (file)
--- 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