Fixing a typo in option name.

diff --git a/main.jpf b/main.jpf
index ce6708fe2e64f2943a4be0c861e8eef747fa4d1d..0e2f8e111034ff44ac084c94df95cc8316f7c497 100644 (file)
--- a/main.jpf
+++ b/main.jpf
@@ -35,11 +35,13 @@ apps=App1,App2
 
 # Debug mode for StateReducer
 debug_state_transition=true
+activate_state_reduction=false
 
 # Timeout in minutes (default is 0 which means no timeout)
 timeout=30
 
 #search.class = gov.nasa.jpf.search.heuristic.RandomHeuristic
+#choice.seed = 3
 #search.class = gov.nasa.jpf.search.heuristic.UserHeuristic
 #search.class = gov.nasa.jpf.search.heuristic.BFSHeuristic
 #search.class = gov.nasa.jpf.search.heuristic.DFSHeuristic

diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java
index 60782a98e9b73615789c937a80326eaee3fbbfdd..7d57f1d9044abaaad47bf309e2f4baeec1a60175 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/StateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/StateReducer.java
@@ -43,6 +43,7 @@ import java.util.*;
 public class StateReducer extends ListenerAdapter {
 
   private boolean debugMode;
+  private boolean stateReductionMode;
   private final PrintWriter out;
   private String detail;
   private int depth;
@@ -56,6 +57,7 @@ public class StateReducer extends ListenerAdapter {
 
   public StateReducer (Config config, JPF jpf) {
     debugMode = config.getBoolean("debug_state_transition", false);
+    stateReductionMode = config.getBoolean("activate_state_reduction", true);
     if (debugMode) {
       out = new PrintWriter(System.out, true);
     } else {
@@ -92,36 +94,40 @@ public class StateReducer extends ListenerAdapter {
 
   @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();
+    if (stateReductionMode) {
+      // 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();
+    if (stateReductionMode) {
+      // 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();
+        }
       }
     }
   }