Adding a prevChoiceValue class property to store the previous choice to update the...

diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java
index 2194ff1..4740583 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/StateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/StateReducer.java
@@ -87,6 +87,8 @@ public class StateReducer extends ListenerAdapter {
   private HashSet<Integer> visitedStateSet;
   // Current state
   private int stateId;
   private HashSet<Integer> visitedStateSet;
   // Current state
   private int stateId;

+  // Previous choice number
+  private int prevChoiceValue;

 
   public StateReducer(Config config, JPF jpf) {
     debugMode = config.getBoolean("debug_state_transition", false);
 
   public StateReducer(Config config, JPF jpf) {
     debugMode = config.getBoolean("debug_state_transition", false);


@@ -104,6 +106,7 @@ public class StateReducer extends ListenerAdapter {
     vodGraphMap = new HashMap<>();
     visitedStateSet = new HashSet<>();
     stateId = -1;
     vodGraphMap = new HashMap<>();
     visitedStateSet = new HashSet<>();
     stateId = -1;

+    prevChoiceValue = -1;

     initializeStateReduction();
   }
 
     initializeStateReduction();
   }
 


@@ -297,17 +300,14 @@ public class StateReducer extends ListenerAdapter {
     if (stateReductionMode) {
       // Update vodGraph
       int currChoice = choiceCounter - 1;
     if (stateReductionMode) {
       // Update vodGraph
       int currChoice = choiceCounter - 1;

-      int prevChoice = currChoice - 1;
-      if (currChoice < 0) {
+      if (currChoice < 0 || choices[currChoice] == -1 || prevChoiceValue == choices[currChoice]) {

         // Current choice has to be at least 0 (initial case can be -1)
         // Current choice has to be at least 0 (initial case can be -1)

-        visitedStateSet.add(stateId);

         return;
       }
         return;
       }

-      // Current choice and previous choice values could be -1 (since we use -1 as the end-of-array condition)
-      int currChoiceValue = (choices[currChoice] == -1) ? 0 : choices[currChoice];

       // When current choice is 0, previous choice could be -1
       // When current choice is 0, previous choice could be -1

-      int prevChoiceValue = (prevChoice == -1) ? -1 : choices[prevChoice];
-      updateVODGraph(prevChoiceValue, currChoiceValue);
+      updateVODGraph(prevChoiceValue, choices[currChoice]);
+      // Current choice becomes previous choice in the next iteration
+      prevChoiceValue = choices[currChoice];

       // Line 19 in the paper page 11 (see the heading note above)
       stateId = search.getStateId();
       // Add state ID into the visited state set
       // Line 19 in the paper page 11 (see the heading note above)
       stateId = search.getStateId();
       // Add state ID into the visited state set