From c3dddbf13bb97e250db9d092cef9787d321fe8f0 Mon Sep 17 00:00:00 2001 From: rtrimana Date: Thu, 21 Jan 2021 16:06:22 -0800 Subject: [PATCH] Bug fix: need to check for conflicts between events extracted from the state summary and the current transition in updateBacktrackSetsFromGraph. --- .../jpf/listener/DPORStateReducerWithSummary.java | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java index 2bc18a9..a750c4d 100755 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java @@ -1338,11 +1338,19 @@ public class DPORStateReducerWithSummary extends ListenerAdapter { Set eventChoicesAtStateId = mainSummary.getEventChoicesAtStateId(stateId); for (Integer eventChoice : eventChoicesAtStateId) { // Get the ReadWriteSet object for this event at state ID - ReadWriteSet rwSet = mainSummary.getRWSetForEventChoiceAtState(eventChoice, stateId); + ReadWriteSet rwSet = mainSummary.getRWSetForEventChoiceAtState(eventChoice, stateId).getCopy(); + // We have to first check for conflicts between the event and the current transition + // Push up one happens-before transition + int conflictEventChoice = eventChoice; + if (isConflictFound(eventChoice, currExecution, currChoice, rwSet)) { + createBacktrackingPoint(eventChoice, currExecution, currChoice); + // We need to extract the pushed happens-before event choice from the predecessor execution and choice + conflictEventChoice = currExecution.getExecutionTrace().get(currChoice).getChoice(); + } // Memorize visited TransitionEvent object while performing backward DFS to avoid getting caught up in a cycle HashSet visited = new HashSet<>(); // Update the backtrack sets recursively - updateBacktrackSetDFS(currExecution, currChoice, eventChoice, rwSet.getCopy(), visited); + updateBacktrackSetDFS(currExecution, currChoice, conflictEventChoice, rwSet, visited); } } } -- 2.34.1