Some fixes for the DPOR state-reducer.
authorrtrimana <rtrimana@uci.edu>
Mon, 16 Mar 2020 20:44:02 +0000 (13:44 -0700)
committerrtrimana <rtrimana@uci.edu>
Mon, 16 Mar 2020 20:44:02 +0000 (13:44 -0700)
main.jpf
src/main/gov/nasa/jpf/listener/StateReducer.java

index 0842997..35b5ea4 100644 (file)
--- a/main.jpf
+++ b/main.jpf
@@ -6,13 +6,17 @@ target = main
 #listener=gov.nasa.jpf.listener.StateReducerOld
 #listener=gov.nasa.jpf.listener.VariableConflictTracker,gov.nasa.jpf.listener.StateReducer
 #listener=gov.nasa.jpf.listener.ConflictTracker,gov.nasa.jpf.listener.StateReducer
 #listener=gov.nasa.jpf.listener.StateReducerOld
 #listener=gov.nasa.jpf.listener.VariableConflictTracker,gov.nasa.jpf.listener.StateReducer
 #listener=gov.nasa.jpf.listener.ConflictTracker,gov.nasa.jpf.listener.StateReducer
-listener=gov.nasa.jpf.listener.ConflictTracker
+
+#listener=gov.nasa.jpf.listener.ConflictTracker,gov.nasa.jpf.listener.StateReducerClean
+#listener=gov.nasa.jpf.listener.ConflictTracker
+#listener=gov.nasa.jpf.listener.StateReducerClean
+listener=gov.nasa.jpf.listener.StateReducer
 
 # Potentially conflicting variables
 # Alarms
 #variables=currentAlarm
 # Locks
 
 # Potentially conflicting variables
 # Alarms
 #variables=currentAlarm
 # Locks
-#variables=currentLock
+variables=currentLock
 # Thermostats
 #variables=currentHeatingSetpoint,thermostatSetpoint,currentCoolingSetpoint,thermostatOperatingState,thermostatFanMode,currentThermostatMode
 # Switches
 # Thermostats
 #variables=currentHeatingSetpoint,thermostatSetpoint,currentCoolingSetpoint,thermostatOperatingState,thermostatFanMode,currentThermostatMode
 # Switches
@@ -20,7 +24,7 @@ listener=gov.nasa.jpf.listener.ConflictTracker
 # Lights
 #variables=colorChanged,currentHue,currentSaturation,currentLevel,currentSwitch,colorTemperature
 # Dimmers
 # Lights
 #variables=colorChanged,currentHue,currentSaturation,currentLevel,currentSwitch,colorTemperature
 # Dimmers
-variables=currentSwitch,currentLevel
+#variables=currentSwitch,currentLevel
 # Speeches
 #variables=level,oneUser
 # Music players
 # Speeches
 #variables=level,oneUser
 # Music players
@@ -41,7 +45,7 @@ apps=App1,App2
 #track_location_var_conflict=true
 
 # Debug mode for StateReducer
 #track_location_var_conflict=true
 
 # Debug mode for StateReducer
-#debug_state_transition=true
+debug_state_transition=true
 #activate_state_reduction=true
 
 # Timeout in minutes (default is 0 which means no timeout)
 #activate_state_reduction=true
 
 # Timeout in minutes (default is 0 which means no timeout)
index e67ee13..71eaf32 100644 (file)
@@ -84,11 +84,16 @@ public class StateReducer extends ListenerAdapter {
   // Set that represents hash table H
   // (i.e., hash table that records encountered states)
   // VOD graph is updated when the state has not yet been seen
   // Set that represents hash table H
   // (i.e., hash table that records encountered states)
   // VOD graph is updated when the state has not yet been seen
-  private HashSet<Integer> visitedStateSet;
   // Current state
   private int stateId;
   // Current state
   private int stateId;
+  // Previous state
+  private int prevStateId;
   // Previous choice number
   private int prevChoiceValue;
   // Previous choice number
   private int prevChoiceValue;
+  // Counter for a visited state
+  private HashMap<Integer, Integer> visitedStateCounter;
+  // HashSet that stores references to unused CGs
+  private HashSet<IntChoiceFromSet> unusedCG;
 
   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,14 +109,16 @@ public class StateReducer extends ListenerAdapter {
     transition = null;
     isBooleanCGFlipped = false;
     vodGraphMap = new HashMap<>();
     transition = null;
     isBooleanCGFlipped = false;
     vodGraphMap = new HashMap<>();
-    visitedStateSet = new HashSet<>();
     stateId = -1;
     stateId = -1;
+    prevStateId = -1;
     prevChoiceValue = -1;
     cgMap = new HashMap<>();
     readWriteFieldsMap = new HashMap<>();
     backtrackMap = new HashMap<>();
     backtrackSet = new HashSet<>();
     conflictPairMap = new HashMap<>();
     prevChoiceValue = -1;
     cgMap = new HashMap<>();
     readWriteFieldsMap = new HashMap<>();
     backtrackMap = new HashMap<>();
     backtrackSet = new HashSet<>();
     conflictPairMap = new HashMap<>();
+    unusedCG = new HashSet<>();
+    visitedStateCounter = new HashMap<>();
     initializeStateReduction();
   }
 
     initializeStateReduction();
   }
 
@@ -166,28 +173,37 @@ public class StateReducer extends ListenerAdapter {
           isInitialized = true;
         }
         // Record the subsequent Integer CGs only until we hit the upper bound
           isInitialized = true;
         }
         // Record the subsequent Integer CGs only until we hit the upper bound
-        if (!isResetAfterAnalysis && choiceCounter <= choiceUpperBound && !cgMap.containsValue(choiceCounter)) {
-          // Update the choices of the first CG and add '-1'
-          if (choices == null) {
-            // Initialize backtrack set that stores all the explored backtrack lists
-            maxUpperBound = cgChoices.length;
-            // All the choices are always the same so we only need to update it once
-            choices = new Integer[cgChoices.length + 1];
-            System.arraycopy(cgChoices, 0, choices, 0, cgChoices.length);
-            choices[choices.length - 1] = -1;
-            String firstChoiceListString = buildStringFromChoiceList(choices);
-            backtrackSet.add(firstChoiceListString);
+        if (!isResetAfterAnalysis) {
+          if (choiceCounter <= choiceUpperBound && !cgMap.containsValue(choiceCounter)) {
+            // Update the choices of the first CG and add '-1'
+            if (choices == null) {
+              // Initialize backtrack set that stores all the explored backtrack lists
+              maxUpperBound = cgChoices.length;
+              // All the choices are always the same so we only need to update it once
+              choices = new Integer[cgChoices.length + 1];
+              System.arraycopy(cgChoices, 0, choices, 0, cgChoices.length);
+              choices[choices.length - 1] = -1;
+              String firstChoiceListString = buildStringFromChoiceList(choices);
+              backtrackSet.add(firstChoiceListString);
+            }
+            icsCG.setNewValues(choices);
+            icsCG.reset();
+            // Advance the current Integer CG
+            // This way we explore all the event numbers in the first pass
+            icsCG.advance(choices[choiceCounter]);
+            cgMap.put(icsCG, choices[choiceCounter]);
+          } else {
+            // We repeat the same trace if a state match is not found yet
+            icsCG.setNewValues(choices);
+            icsCG.reset();
+            // Use a modulo since choiceCounter is going to keep increasing
+            int choiceIndex = choiceCounter % (choices.length - 1);
+            icsCG.advance(choices[choiceIndex]);
+            unusedCG.add(icsCG);
           }
           }
-          icsCG.setNewValues(choices);
-          icsCG.reset();
-          // Advance the current Integer CG
-          // This way we explore all the event numbers in the first pass
-          icsCG.advance(choices[choiceCounter]);
-          cgMap.put(icsCG, choices[choiceCounter]);
           choiceCounter++;
         } else {
           choiceCounter++;
         } else {
-          // Set done the subsequent CGs
-          // We only need n CGs (n is event numbers)
+          // Set new CGs to done so that the search algorithm explores the existing CGs
           icsCG.setDone();
         }
       }
           icsCG.setDone();
         }
       }
@@ -199,6 +215,10 @@ public class StateReducer extends ListenerAdapter {
     Set<Integer> eventSet = backtrackMap.keySet();
     // Return if there is no conflict at all (highly unlikely)
     if (eventSet.isEmpty()) {
     Set<Integer> eventSet = backtrackMap.keySet();
     // Return if there is no conflict at all (highly unlikely)
     if (eventSet.isEmpty()) {
+      // Set every CG to done!
+      for (IntChoiceFromSet cg : cgMap.keySet()) {
+        cg.setDone();
+      }
       return;
     }
     // Reset every CG with the first backtrack lists
       return;
     }
     // Reset every CG with the first backtrack lists
@@ -214,6 +234,31 @@ public class StateReducer extends ListenerAdapter {
         cg.setDone();
       }
     }
         cg.setDone();
       }
     }
+    // Set done every CG in the unused CG set
+    for (IntChoiceFromSet cg : unusedCG) {
+      cg.setDone();
+    }
+    unusedCG.clear();
+  }
+
+  private void incrementVisitedStateCounter(int stId) {
+    // Increment counter for this state ID
+    if (visitedStateCounter.containsKey(stId)) {
+      int stateCount = visitedStateCounter.get(stId);
+      visitedStateCounter.put(stId, stateCount + 1);
+    } else {
+      // If we have seen it then the frequency is 2
+      visitedStateCounter.put(stId, 2);
+    }
+  }
+
+  private boolean isVisitedMultipleTimes(int stId) {
+    // Return true if the state has been visited more than once
+    if (visitedStateCounter.containsKey(stId) &&
+            visitedStateCounter.get(stId) > 1) {
+      return true;
+    }
+    return false;
   }
 
   @Override
   }
 
   @Override
@@ -241,13 +286,18 @@ public class StateReducer extends ListenerAdapter {
           readWriteFieldsMap.clear();
           choiceCounter = 0;
         }
           readWriteFieldsMap.clear();
           choiceCounter = 0;
         }
-        // Traverse the sub-graphs
-        if (isResetAfterAnalysis) {
-          // Advance choice counter for sub-graphs
-          choiceCounter++;
-          // Do this for every CG after finishing each backtrack list
-          if (icsCG.getNextChoice() == -1 || visitedStateSet.contains(stateId)) {
-            if (cgMap.containsKey(icsCG)) {
+        if (!vm.isNewState()) {
+          incrementVisitedStateCounter(stateId);
+        }
+        // Check if we have seen this state and it's not looping back to itself
+        if (prevStateId != -1 && stateId != prevStateId && isVisitedMultipleTimes(stateId)) {
+          // Traverse the sub-graphs
+          if (isResetAfterAnalysis) {
+            // Advance choice counter for sub-graphs
+            choiceCounter++;
+            // Do this for every CG after finishing each backtrack list
+            // We try to update the CG with a backtrack list if the state has been visited multiple times
+            if ((icsCG.getNextChoice() == -1 || choiceCounter > 1) && cgMap.containsKey(icsCG)) {
               int event = cgMap.get(icsCG);
               LinkedList<Integer[]> choiceLists = backtrackMap.get(event);
               if (choiceLists != null && choiceLists.peekFirst() != null) {
               int event = cgMap.get(icsCG);
               LinkedList<Integer[]> choiceLists = backtrackMap.get(event);
               if (choiceLists != null && choiceLists.peekFirst() != null) {
@@ -260,13 +310,13 @@ public class StateReducer extends ListenerAdapter {
                 icsCG.setDone();
               }
             }
                 icsCG.setDone();
               }
             }
+          } else {
+            // Update and reset the CG if needed (do this for the first time after the analysis)
+            // Start backtracking if this is a visited state and it is not a repeating state
+            resetAllCGs();
+            isResetAfterAnalysis = true;
           }
         }
           }
         }
-        // Update and reset the CG if needed (do this for the first time after the analysis)
-        if (!isResetAfterAnalysis && icsCG.getNextChoice() == -1) {
-          resetAllCGs();
-          isResetAfterAnalysis = true;
-        }
       }
     }
   }
       }
     }
   }
@@ -285,6 +335,13 @@ public class StateReducer extends ListenerAdapter {
     choiceSet.add(currChoice);
   }
 
     choiceSet.add(currChoice);
   }
 
+  private void updateStateId(Search search) {
+    // Saving the previous state
+    prevStateId = stateId;
+    // Line 19 in the paper page 11 (see the heading note above)
+    stateId = search.getStateId();
+  }
+
   @Override
   public void stateAdvanced(Search search) {
     if (debugMode) {
   @Override
   public void stateAdvanced(Search search) {
     if (debugMode) {
@@ -307,7 +364,18 @@ public class StateReducer extends ListenerAdapter {
     if (stateReductionMode) {
       // Update vodGraph
       int currChoice = choiceCounter - 1;
     if (stateReductionMode) {
       // Update vodGraph
       int currChoice = choiceCounter - 1;
-      if (currChoice < 0 || currChoice > choices.length - 1 || choices[currChoice] == -1 || prevChoiceValue == choices[currChoice]) {
+      // Adjust currChoice with modulo
+      currChoice = currChoice >= 0 ? currChoice % (choices.length -1) : currChoice;
+      if (currChoice < 0 || choices[currChoice] == -1 ||
+              prevChoiceValue == choices[currChoice]) {
+//              || currChoice > choices.length - 1 || choices[currChoice] == -1 ||
+//              prevChoiceValue == choices[currChoice]) {
+//        // When current choice is 0, previous choice could be -1
+//        updateVODGraph(prevChoiceValue, choices[currChoice]);
+//        // Current choice becomes previous choice in the next iteration
+//        prevChoiceValue = choices[currChoice];
+        // Update the state ID variables
+        updateStateId(search);
         // Handle all corner cases (e.g., out of bound values)
         return;
       }
         // Handle all corner cases (e.g., out of bound values)
         return;
       }
@@ -315,10 +383,8 @@ public class StateReducer extends ListenerAdapter {
       updateVODGraph(prevChoiceValue, choices[currChoice]);
       // Current choice becomes previous choice in the next iteration
       prevChoiceValue = choices[currChoice];
       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
-      visitedStateSet.add(stateId);
+      // Update the state ID variables
+      updateStateId(search);
     }
   }
 
     }
   }
 
@@ -330,6 +396,12 @@ public class StateReducer extends ListenerAdapter {
       transition = search.getTransition();
       detail = null;
 
       transition = search.getTransition();
       detail = null;
 
+      // Update the state variables
+      // Saving the previous state
+      prevStateId = stateId;
+      // Line 19 in the paper page 11 (see the heading note above)
+      stateId = search.getStateId();
+
       out.println("\n==> DEBUG: The state is backtracked to state with id: " + id + " -- Transition: " + transition +
               " and depth: " + depth + "\n");
     }
       out.println("\n==> DEBUG: The state is backtracked to state with id: " + id + " -- Transition: " + transition +
               " and depth: " + depth + "\n");
     }
@@ -588,7 +660,7 @@ public class StateReducer extends ListenerAdapter {
   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
     if (stateReductionMode) {
       if (isInitialized) {
   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
     if (stateReductionMode) {
       if (isInitialized) {
-        if (choiceCounter > choices.length - 1) {
+        if (choiceCounter <= 0 || choiceCounter > choices.length - 1) {
           // We do not compute the conflicts for the choice '-1'
           return;
         }
           // We do not compute the conflicts for the choice '-1'
           return;
         }
@@ -630,8 +702,8 @@ public class StateReducer extends ListenerAdapter {
                   // If it has been serviced before, we just skip this
                   if (recordConflictPair(currentChoice, eventNumber)) {
                     // Lines 4-8 of the algorithm in the paper page 11 (see the heading note above)
                   // If it has been serviced before, we just skip this
                   if (recordConflictPair(currentChoice, eventNumber)) {
                     // Lines 4-8 of the algorithm in the paper page 11 (see the heading note above)
-                    if (!visitedStateSet.contains(stateId)||
-                            (visitedStateSet.contains(stateId) && isReachableInVODGraph(choices[currentChoice], choices[currentChoice-1]))) {
+                    if (vm.isNewState() ||
+                            (!vm.isNewState() && isReachableInVODGraph(choices[currentChoice], choices[currentChoice-1]))) {
                       createBacktrackChoiceList(currentChoice, eventNumber);
                       // Break if a conflict is found!
                       break;
                       createBacktrackChoiceList(currentChoice, eventNumber);
                       // Break if a conflict is found!
                       break;