Fixing a bug in isConflict method.

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index f6903824fc2a9ec388f538b71a44498aefe54420..a483afcc7e6d6f0843b9a168b1c248b0c91ded17 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -961,21 +961,21 @@ public class DPORStateReducer extends ListenerAdapter {
   private boolean isConflictFound(Execution execution, int reachableChoice, Execution conflictExecution, int conflictChoice,
                                   ReadWriteSet currRWSet) {
     ArrayList<TransitionEvent> executionTrace = execution.getExecutionTrace();
   private boolean isConflictFound(Execution execution, int reachableChoice, Execution conflictExecution, int conflictChoice,
                                   ReadWriteSet currRWSet) {
     ArrayList<TransitionEvent> executionTrace = execution.getExecutionTrace();

-    HashMap<Integer, ReadWriteSet> execRWFieldsMap = execution.getReadWriteFieldsMap();

     ArrayList<TransitionEvent> conflictTrace = conflictExecution.getExecutionTrace();
     ArrayList<TransitionEvent> conflictTrace = conflictExecution.getExecutionTrace();

+    HashMap<Integer, ReadWriteSet> confRWFieldsMap = conflictExecution.getReadWriteFieldsMap();

     // Skip if this event does not have any Read/Write set or the two events are basically the same event (number)
     // Skip if this event does not have any Read/Write set or the two events are basically the same event (number)

-    if (!execRWFieldsMap.containsKey(conflictChoice) ||
+    if (!confRWFieldsMap.containsKey(conflictChoice) ||

             executionTrace.get(reachableChoice).getChoice() == conflictTrace.get(conflictChoice).getChoice()) {
       return false;
     }
     // R/W set of choice/event that may have a potential conflict
             executionTrace.get(reachableChoice).getChoice() == conflictTrace.get(conflictChoice).getChoice()) {
       return false;
     }
     // R/W set of choice/event that may have a potential conflict

-    ReadWriteSet evtRWSet = execRWFieldsMap.get(conflictChoice);
+    ReadWriteSet confRWSet = confRWFieldsMap.get(conflictChoice);

     // Check for conflicts with Read and Write fields for Write instructions
     Set<String> currWriteSet = currRWSet.getWriteSet();
     for(String writeField : currWriteSet) {
       int currObjId = currRWSet.writeFieldObjectId(writeField);
     // Check for conflicts with Read and Write fields for Write instructions
     Set<String> currWriteSet = currRWSet.getWriteSet();
     for(String writeField : currWriteSet) {
       int currObjId = currRWSet.writeFieldObjectId(writeField);

-      if ((evtRWSet.readFieldExists(writeField) && evtRWSet.readFieldObjectId(writeField) == currObjId) ||
-          (evtRWSet.writeFieldExists(writeField) && evtRWSet.writeFieldObjectId(writeField) == currObjId)) {
+      if ((confRWSet.readFieldExists(writeField) && confRWSet.readFieldObjectId(writeField) == currObjId) ||
+          (confRWSet.writeFieldExists(writeField) && confRWSet.writeFieldObjectId(writeField) == currObjId)) {

         // Remove this from the write set as we are tracking per memory location
         currRWSet.removeWriteField(writeField);
         return true;
         // Remove this from the write set as we are tracking per memory location
         currRWSet.removeWriteField(writeField);
         return true;


@@ -985,7 +985,7 @@ public class DPORStateReducer extends ListenerAdapter {
     Set<String> currReadSet = currRWSet.getReadSet();
     for(String readField : currReadSet) {
       int currObjId = currRWSet.readFieldObjectId(readField);
     Set<String> currReadSet = currRWSet.getReadSet();
     for(String readField : currReadSet) {
       int currObjId = currRWSet.readFieldObjectId(readField);

-      if (evtRWSet.writeFieldExists(readField) && evtRWSet.writeFieldObjectId(readField) == currObjId) {
+      if (confRWSet.writeFieldExists(readField) && confRWSet.writeFieldObjectId(readField) == currObjId) {

         // Remove this from the read set as we are tracking per memory location
         currRWSet.removeReadField(readField);
         return true;
         // Remove this from the read set as we are tracking per memory location
         currRWSet.removeReadField(readField);
         return true;