Fixing more potential bugs for the reachability analysis.

diff --git a/main.jpf b/main.jpf
index 81a40dc..4c3f7d9 100644 (file)
--- a/main.jpf
+++ b/main.jpf
@@ -9,8 +9,8 @@ target = main
 ##listener=gov.nasa.jpf.listener.ConflictTrackerOld,gov.nasa.jpf.listener.StateReducer
 ##listener=gov.nasa.jpf.listener.ConflictTrackerOld,gov.nasa.jpf.listener.DPORStateReducer
 #listener=gov.nasa.jpf.listener.ConflictTrackerOld
 ##listener=gov.nasa.jpf.listener.ConflictTrackerOld,gov.nasa.jpf.listener.StateReducer
 ##listener=gov.nasa.jpf.listener.ConflictTrackerOld,gov.nasa.jpf.listener.DPORStateReducer
 #listener=gov.nasa.jpf.listener.ConflictTrackerOld

-listener=gov.nasa.jpf.listener.DPORStateReducer
-#listener=gov.nasa.jpf.listener.DPORStateReducer,gov.nasa.jpf.listener.ConflictTrackerOld
+#listener=gov.nasa.jpf.listener.DPORStateReducer
+listener=gov.nasa.jpf.listener.DPORStateReducer,gov.nasa.jpf.listener.ConflictTrackerOld

 
 # Potentially conflicting variables
 # Alarms
 
 # Potentially conflicting variables
 # Alarms


@@ -44,7 +44,7 @@ apps=App1,App2
 
 # Debug mode for ConflictTracker
 # We do not report any conflicts if the value is true
 
 # Debug mode for ConflictTracker
 # We do not report any conflicts if the value is true

-debug_mode=true
+#debug_mode=true

 
 # Debug mode for StateReducer
 printout_state_transition=true
 
 # Debug mode for StateReducer
 printout_state_transition=true

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index 0c513f2..104af2b 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -490,14 +490,14 @@ public class DPORStateReducer extends ListenerAdapter {
     // Update the state variables
     // Line 19 in the paper page 11 (see the heading note above)
     int stateId = search.getStateId();
     // Update the state variables
     // Line 19 in the paper page 11 (see the heading note above)
     int stateId = search.getStateId();

-    currVisitedStates.add(stateId);

     // Insert state ID into the map if it is new
     if (!stateToEventMap.containsKey(stateId)) {
       HashSet<Integer> eventSet = new HashSet<>();
       stateToEventMap.put(stateId, eventSet);
     }
     // Insert state ID into the map if it is new
     if (!stateToEventMap.containsKey(stateId)) {
       HashSet<Integer> eventSet = new HashSet<>();
       stateToEventMap.put(stateId, eventSet);
     }

-    justVisitedStates.add(stateId);

     analyzeReachabilityAndCreateBacktrackPoints(search.getVM(), stateId);
     analyzeReachabilityAndCreateBacktrackPoints(search.getVM(), stateId);

+    justVisitedStates.add(stateId);
+    currVisitedStates.add(stateId);

   }
 
   // --- Functions related to Read/Write access analysis on shared fields
   }
 
   // --- Functions related to Read/Write access analysis on shared fields


@@ -835,8 +835,14 @@ public class DPORStateReducer extends ListenerAdapter {
   // 2) We need to analyze and find conflicts for the reachable choices/events in the cycle
   // 3) Then we create a new backtrack point for every new conflict
   private void analyzeReachabilityAndCreateBacktrackPoints(VM vm, int stateId) {
   // 2) We need to analyze and find conflicts for the reachable choices/events in the cycle
   // 3) Then we create a new backtrack point for every new conflict
   private void analyzeReachabilityAndCreateBacktrackPoints(VM vm, int stateId) {

-    // Perform this analysis only when there is a state match and state > 0 (state 0 is for boolean CG)
-    if (!vm.isNewState() && (stateId > 0)) {
+    // Perform this analysis only when:
+    // 1) there is a state match,
+    // 2) this is not during a switch to a new execution,
+    // 3) at least 2 choices/events have been explored (choiceCounter > 1),
+    // 4) the matched state has been encountered in the current execution, and
+    // 5) state > 0 (state 0 is for boolean CG)
+    if (!vm.isNewState() && !isEndOfExecution && choiceCounter > 1 &&
+            currVisitedStates.contains(stateId) && (stateId > 0)) {

       // Find the choice/event that marks the start of this cycle: first choice we explore for conflicts
       int conflictChoice = stateToChoiceCounterMap.get(stateId);
       int currentChoice = choiceCounter - 1;
       // Find the choice/event that marks the start of this cycle: first choice we explore for conflicts
       int conflictChoice = stateToChoiceCounterMap.get(stateId);
       int currentChoice = choiceCounter - 1;