Commenting out a line that causes a lot of loops; let the exclusion trace continue...

[jpf-core.git] / src / main / gov / nasa / jpf / listener / DPORStateReducer.java

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index ef0994cbdeba690d46c526b1016c54a488bc09dc..743d7bedd2536aac19bcf5f7256063276770fa7a 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -352,6 +352,10 @@ public class DPORStateReducer extends ListenerAdapter {
       return executionTrace.get(0);
     }
 
+    public TransitionEvent getLastTransition() {
+      return executionTrace.get(executionTrace.size() - 1);
+    }
+
     public HashMap<Integer, ReadWriteSet> getReadWriteFieldsMap() {
       return readWriteFieldsMap;
     }
@@ -421,6 +425,12 @@ public class DPORStateReducer extends ListenerAdapter {
     }
 
     public HashSet<TransitionEvent> getReachableTransitionsAtState(int stateId) {
+      if (!graph.containsKey(stateId)) {
+        // This is a loop from a transition to itself, so just return the current transition
+        HashSet<TransitionEvent> transitionSet = new HashSet<>();
+        transitionSet.add(currentExecution.getLastTransition());
+        return transitionSet;
+      }
       return graph.get(stateId);
     }
 
@@ -1155,7 +1165,8 @@ public class DPORStateReducer extends ListenerAdapter {
               pushedExecution, pushedChoice, currRWSet, visited);
     }
     // Remove the transition after being explored
-    visited.remove(confTrans);
+    // TODO: Seems to cause a lot of loops---commented out for now
+    //visited.remove(confTrans);
   }
 
   // --- Functions related to the reachability analysis when there is a state match