Re-checking and cleaning up the code: most likely still have a bug in re-ordering...

diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java
index e03135454330bf21df98cb80db167cfc819fd8de..91c0b11cb0060fd65b75500470db2522fd387549 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/StateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/StateReducer.java
@@ -26,7 +26,9 @@ import gov.nasa.jpf.vm.*;
 import gov.nasa.jpf.vm.bytecode.ReadInstruction;
 import gov.nasa.jpf.vm.bytecode.WriteInstruction;
 import gov.nasa.jpf.vm.choice.IntChoiceFromSet;
 import gov.nasa.jpf.vm.bytecode.ReadInstruction;
 import gov.nasa.jpf.vm.bytecode.WriteInstruction;
 import gov.nasa.jpf.vm.choice.IntChoiceFromSet;

+import gov.nasa.jpf.vm.choice.IntIntervalGenerator;

 
 

+import java.awt.*;

 import java.io.PrintWriter;
 
 import java.util.*;
 import java.io.PrintWriter;
 
 import java.util.*;


@@ -139,6 +141,9 @@ public class StateReducer extends ListenerAdapter {
       resetReadWriteAnalysis();
       backtrackMap.clear();
       backtrackSet.clear();
       resetReadWriteAnalysis();
       backtrackMap.clear();
       backtrackSet.clear();

+      stateToEventMap.clear();
+      prevVisitedStates.clear();
+      currVisitedStates.clear();

     }
   }
 
     }
   }
 


@@ -188,9 +193,9 @@ public class StateReducer extends ListenerAdapter {
   }
 
   private void continueExecutingThisTrace(IntChoiceFromSet icsCG) {
   }
 
   private void continueExecutingThisTrace(IntChoiceFromSet icsCG) {

-    // We repeat the same trace if a state match is not found yet
-    IntChoiceFromSet setCG = setNewCG(icsCG);
-    unusedCG.add(setCG);
+      // We repeat the same trace if a state match is not found yet
+      IntChoiceFromSet setCG = setNewCG(icsCG);
+      unusedCG.add(setCG);

   }
 
   private void initializeChoiceGenerators(IntChoiceFromSet icsCG, Integer[] cgChoices) {
   }
 
   private void initializeChoiceGenerators(IntChoiceFromSet icsCG, Integer[] cgChoices) {


@@ -245,7 +250,6 @@ public class StateReducer extends ListenerAdapter {
           //icsCG.setDone();
           manageChoiceGeneratorsInSubsequentTraces(icsCG);
         }
           //icsCG.setDone();
           manageChoiceGeneratorsInSubsequentTraces(icsCG);
         }

-        choiceCounter++;

       }
     }
   }
       }
     }
   }


@@ -259,6 +263,8 @@ public class StateReducer extends ListenerAdapter {
   }
 
   private void resetAllCGs() {
   }
 
   private void resetAllCGs() {

+
+    isResetAfterAnalysis = true;

     // Extract the event numbers that have backtrack lists
     Set<Integer> eventSet = backtrackMap.keySet();
     // Return if there is no conflict at all (highly unlikely)
     // Extract the event numbers that have backtrack lists
     Set<Integer> eventSet = backtrackMap.keySet();
     // Return if there is no conflict at all (highly unlikely)


@@ -294,6 +300,10 @@ public class StateReducer extends ListenerAdapter {
   // Basically, we have to check that we have executed all events between two occurrences of such state.
   private boolean containsCyclesWithAllEvents(int stId) {
 
   // Basically, we have to check that we have executed all events between two occurrences of such state.
   private boolean containsCyclesWithAllEvents(int stId) {
 

+    // False if the state ID hasn't been recorded
+    if (!stateToEventMap.containsKey(stId)) {
+      return false;
+    }

     HashSet<Integer> visitedEvents = stateToEventMap.get(stId);
     boolean containsCyclesWithAllEvts = false;
     if (checkIfAllEventsInvolved(visitedEvents)) {
     HashSet<Integer> visitedEvents = stateToEventMap.get(stId);
     boolean containsCyclesWithAllEvts = false;
     if (checkIfAllEventsInvolved(visitedEvents)) {


@@ -333,14 +343,61 @@ public class StateReducer extends ListenerAdapter {
     }
   }
 
     }
   }
 

+  private void checkAndEnforceFairScheduling(IntChoiceFromSet icsCG) {
+    // Check the next choice and if the value is not the same as the expected then force the expected value
+    int choiceIndex = choiceCounter % refChoices.length;
+    int nextChoice = icsCG.getNextChoice();
+    if (refChoices[choiceIndex] != nextChoice) {
+      int expectedChoice = refChoices[choiceIndex];
+      int currCGIndex = icsCG.getNextChoiceIndex();
+      if ((currCGIndex >= 0) && (currCGIndex < refChoices.length)) {
+        icsCG.setChoice(currCGIndex, expectedChoice);
+      }
+    }
+  }
+
+  private void mapStateToEvent(int nextChoiceValue) {
+    // Update all states with this event/choice
+    // This means that all past states now see this transition
+    Set<Integer> stateSet = stateToEventMap.keySet();
+    for(Integer stateId : stateSet) {
+      HashSet<Integer> eventSet = stateToEventMap.get(stateId);
+      eventSet.add(nextChoiceValue);
+    }
+  }
+
+  private void updateVODGraph(int currChoiceValue) {
+    // Update the graph when we have the current choice value
+    HashSet<Integer> choiceSet;
+    if (vodGraphMap.containsKey(prevChoiceValue)) {
+      // If the key already exists, just retrieve it
+      choiceSet = vodGraphMap.get(prevChoiceValue);
+    } else {
+      // Create a new entry
+      choiceSet = new HashSet<>();
+      vodGraphMap.put(prevChoiceValue, choiceSet);
+    }
+    choiceSet.add(currChoiceValue);
+    prevChoiceValue = currChoiceValue;
+  }
+
+  private boolean terminateCurrentExecution() {
+    // We need to check all the states that have just been visited
+    // Often a transition (choice/event) can result into forwarding/backtracking to a number of states
+    for(Integer stateId : justVisitedStates) {
+      if (prevVisitedStates.contains(stateId) || containsCyclesWithAllEvents(stateId)) {
+        return true;
+      }
+    }
+    return false;
+  }
+

   private void exploreNextBacktrackSets(IntChoiceFromSet icsCG) {
     // Traverse the sub-graphs
     if (isResetAfterAnalysis) {
       // 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
   private void exploreNextBacktrackSets(IntChoiceFromSet icsCG) {
     // Traverse the sub-graphs
     if (isResetAfterAnalysis) {
       // 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)) {
-      //if ((!icsCG.hasMoreChoices() || choiceCounter > 1) && cgMap.containsKey(icsCG)) {
-      if (choiceCounter > 1 && cgMap.containsKey(icsCG)) {
+      if (icsCG.getNextChoiceIndex() > 0 && 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) {


@@ -359,37 +416,16 @@ public class StateReducer extends ListenerAdapter {
       // 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();
       // 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;

     }
   }
 
     }
   }
 

-  private void checkAndEnforceFairScheduling(IntChoiceFromSet icsCG) {
-    // Check the next choice and if the value is not the same as the expected then force the expected value
-    int choiceIndex = (choiceCounter - 1) % refChoices.length;
-    if (choices[choiceIndex] != icsCG.getNextChoiceIndex()) {
-      int expectedChoice = refChoices[choiceIndex];
-      int currCGIndex = icsCG.getNextChoiceIndex();
-      if ((currCGIndex >= 0) && (currCGIndex < refChoices.length)) {
-        icsCG.setChoice(currCGIndex, expectedChoice);
-      }
-    }
-  }
-
-  private boolean terminateCurrentExecution() {
-    // We need to check all the states that have just been visited
-    // Often a transition (choice/event) can result into forwarding/backtracking to a number of states
-    for(Integer stateId : justVisitedStates) {
-      if (prevVisitedStates.contains(stateId) || containsCyclesWithAllEvents(stateId)) {
-        return true;
-      }
-    }
-    return false;
-  }
-

   @Override
   public void choiceGeneratorAdvanced(VM vm, ChoiceGenerator<?> currentCG) {
 
     if (stateReductionMode) {
   @Override
   public void choiceGeneratorAdvanced(VM vm, ChoiceGenerator<?> currentCG) {
 
     if (stateReductionMode) {

+      if (vm.getNextChoiceGenerator() instanceof BooleanChoiceGenerator) {
+        System.out.println("Next CG is a booleanCG");
+      }

       // Check the boolean CG and if it is flipped, we are resetting the analysis
       if (currentCG instanceof BooleanChoiceGenerator) {
         if (!isBooleanCGFlipped) {
       // Check the boolean CG and if it is flipped, we are resetting the analysis
       if (currentCG instanceof BooleanChoiceGenerator) {
         if (!isBooleanCGFlipped) {


@@ -404,44 +440,28 @@ public class StateReducer extends ListenerAdapter {
         IntChoiceFromSet icsCG = (IntChoiceFromSet) currentCG;
         // Update the current pointer to the current set of choices
         updateChoicesForNewExecution(icsCG);
         IntChoiceFromSet icsCG = (IntChoiceFromSet) currentCG;
         // Update the current pointer to the current set of choices
         updateChoicesForNewExecution(icsCG);

+        // If we don't see a fair scheduling of events/choices then we have to enforce it
+        checkAndEnforceFairScheduling(icsCG);
+        // Map state to event
+        mapStateToEvent(icsCG.getNextChoice());
+        // Update the VOD graph always with the latest
+        updateVODGraph(icsCG.getNextChoice());

         // Check if we have seen this state or this state contains cycles that involve all events
         if (terminateCurrentExecution()) {
           exploreNextBacktrackSets(icsCG);
         }
         justVisitedStates.clear();
         // Check if we have seen this state or this state contains cycles that involve all events
         if (terminateCurrentExecution()) {
           exploreNextBacktrackSets(icsCG);
         }
         justVisitedStates.clear();

-        // If we don't see a fair scheduling of events/choices then we have to enforce it
-        checkAndEnforceFairScheduling(icsCG);
-        // Update the VOD graph always with the latest
-        updateVODGraph(icsCG.getNextChoice());
+        choiceCounter++;

       }
     }
   }
 
       }
     }
   }
 

-  private void updateVODGraph(int currChoiceValue) {
-    // Update the graph when we have the current choice value
-    HashSet<Integer> choiceSet;
-    if (vodGraphMap.containsKey(prevChoiceValue)) {
-      // If the key already exists, just retrieve it
-      choiceSet = vodGraphMap.get(prevChoiceValue);
-    } else {
-      // Create a new entry
-      choiceSet = new HashSet<>();
-      vodGraphMap.put(prevChoiceValue, choiceSet);
-    }
-    choiceSet.add(currChoiceValue);
-    prevChoiceValue = currChoiceValue;
-  }
-
-  private void mapStateToEvent(Search search, int stateId) {
-    // Insert state ID and event choice into the map
-    HashSet<Integer> eventSet;
-    if (stateToEventMap.containsKey(stateId)) {
-      eventSet = stateToEventMap.get(stateId);
-    } else {
-      eventSet = new HashSet<>();
+  private void checkAndRecordNewState(int stateId) {
+    // Insert state ID into the map if it is new
+    if (!stateToEventMap.containsKey(stateId)) {
+      HashSet<Integer> eventSet = new HashSet<>();

       stateToEventMap.put(stateId, eventSet);
     }
       stateToEventMap.put(stateId, eventSet);
     }

-    eventSet.add(prevChoiceValue);

   }
 
   private void updateStateInfo(Search search) {
   }
 
   private void updateStateInfo(Search search) {


@@ -450,7 +470,7 @@ public class StateReducer extends ListenerAdapter {
       // Line 19 in the paper page 11 (see the heading note above)
       int stateId = search.getStateId();
       currVisitedStates.add(stateId);
       // Line 19 in the paper page 11 (see the heading note above)
       int stateId = search.getStateId();
       currVisitedStates.add(stateId);

-      mapStateToEvent(search, stateId);
+      checkAndRecordNewState(stateId);

       justVisitedStates.add(stateId);
     }
   }
       justVisitedStates.add(stateId);
     }
   }


@@ -740,13 +760,26 @@ public class StateReducer extends ListenerAdapter {
     return false;
   }
 
     return false;
   }
 

+  private int getCurrentChoice(VM vm) {
+    ChoiceGenerator<?> currentCG = vm.getChoiceGenerator();
+    // This is the main event CG
+    if (currentCG instanceof IntChoiceFromSet) {
+      return ((IntChoiceFromSet) currentCG).getNextChoiceIndex();
+    } else {
+      // This is the interval CG used in device handlers
+      ChoiceGenerator<?> parentCG = ((IntIntervalGenerator) currentCG).getPreviousChoiceGenerator();
+      return ((IntChoiceFromSet) parentCG).getNextChoiceIndex();
+    }
+  }
+

   @Override
   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
     if (stateReductionMode) {
   @Override
   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
     if (stateReductionMode) {

-      if (isInitialized) {
-        int currentChoice = (choiceCounter % refChoices.length) - 1;
-        if (currentChoice < 0) {
-          // We do not compute the conflicts for the choice '-1'
+      // Has to be initialized and a integer CG
+      ChoiceGenerator<?> cg = vm.getChoiceGenerator();
+      if (isInitialized && (cg instanceof IntChoiceFromSet || cg instanceof IntIntervalGenerator)) {
+        int currentChoice = getCurrentChoice(vm);
+        if (currentChoice < 0) { // If choice is -1 then skip

           return;
         }
         // Record accesses from executed instructions
           return;
         }
         // Record accesses from executed instructions

diff --git a/src/main/gov/nasa/jpf/vm/choice/IntChoiceFromSet.java b/src/main/gov/nasa/jpf/vm/choice/IntChoiceFromSet.java
index eb2f33b50c4b81ff766cc9ec17e5d6f0a19b08f6..be114369f08e41c69f2d6cdbebd5b5154f8891fb 100644 (file)
--- a/src/main/gov/nasa/jpf/vm/choice/IntChoiceFromSet.java
+++ b/src/main/gov/nasa/jpf/vm/choice/IntChoiceFromSet.java
@@ -68,13 +68,6 @@ public class IntChoiceFromSet extends IntChoiceFromList {
     count = -1;
   }
 
     count = -1;
   }
 

-  // TODO: Fix for Groovy's model-checking
-  // TODO: This is a setter to change the values of the ChoiceGenerator to implement POR
-  @Override
-  public void setNewValues(Integer[] vals) {
-    values = vals;
-  }
-

   @Override
   public Integer[] getAllChoices() {
     return values;
   @Override
   public Integer[] getAllChoices() {
     return values;