From d5abca72b4e24ce48e43a54521032006ea3a2a41 Mon Sep 17 00:00:00 2001 From: rtrimana Date: Fri, 20 Mar 2020 14:11:09 -0700 Subject: [PATCH] Fixing bugs: moving VOD-graph building into the CGAdvanced method to have the most up-to-date values. --- .../gov/nasa/jpf/listener/StateReducer.java | 58 ++++++++++--------- 1 file changed, 31 insertions(+), 27 deletions(-) diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java index ec2fe98..532076b 100644 --- a/src/main/gov/nasa/jpf/listener/StateReducer.java +++ b/src/main/gov/nasa/jpf/listener/StateReducer.java @@ -203,6 +203,7 @@ public class StateReducer extends ListenerAdapter { icsCG.advance(choices[choiceIndex]); unusedCG.add(icsCG); } + //choiceCounter = choiceCounter < choiceUpperBound ? choiceCounter + 1 : 0; choiceCounter++; } else { // Set new CGs to done so that the search algorithm explores the existing CGs @@ -241,6 +242,7 @@ public class StateReducer extends ListenerAdapter { cg.setDone(); } unusedCG.clear(); + saveVisitedStates(); } // Detect cycles in the current execution/trace @@ -249,12 +251,11 @@ public class StateReducer extends ListenerAdapter { // (2) the state has one or more cycles that involve all the events private boolean containsCyclesWithAllEvents(int stId) { + HashSet visitingStates = new HashSet<>(); HashSet visitedEvents = new HashSet<>(); boolean containsCyclesWithAllEvts = false; ConflictTracker.Node currNode = stateGraph.get(stId); - for(ConflictTracker.Edge edge : currNode.getOutEdges()) { - dfsFindCycles(edge.getDst(), visitedEvents, new HashSet<>()); - } + dfsFindCycles(currNode, visitingStates, visitedEvents, new HashSet<>()); if (checkIfAllEventsInvolved(visitedEvents)) { containsCyclesWithAllEvts = true; } @@ -262,18 +263,20 @@ public class StateReducer extends ListenerAdapter { return containsCyclesWithAllEvts; } - private void dfsFindCycles(ConflictTracker.Node currNode, HashSet visitedEvents, - HashSet visitingEvents) { + private void dfsFindCycles(ConflictTracker.Node currNode, HashSet visitingStates, + HashSet visitedEvents, HashSet visitingEvents) { // Stop when there is a cycle and record all the events - if (visitingEvents.contains(currNode.getId())) { + if (visitingStates.contains(currNode)) { visitedEvents.addAll(visitingEvents); } else { + visitingStates.add(currNode); for(ConflictTracker.Edge edge : currNode.getOutEdges()) { visitingEvents.add(edge.getEventNumber()); - dfsFindCycles(edge.getDst(), visitedEvents, visitingEvents); + dfsFindCycles(edge.getDst(), visitingStates, visitedEvents, visitingEvents); visitingEvents.remove(edge.getEventNumber()); } + visitingStates.remove(currNode); } } @@ -289,6 +292,13 @@ public class StateReducer extends ListenerAdapter { return true; } + private void saveVisitedStates() { + // CG is being reset + // Save all the visited states + prevVisitedStates.addAll(currVisitedStates); + currVisitedStates.clear(); + } + @Override public void choiceGeneratorAdvanced(VM vm, ChoiceGenerator currentCG) { @@ -315,7 +325,6 @@ public class StateReducer extends ListenerAdapter { choiceCounter = 0; } // Check if we have seen this state or this state contains cycles that involve all events -// if (prevStateId != -1 && stateId != prevStateId && isVisitedMultipleTimes(stateId)) { if (prevVisitedStates.contains(stateId) || containsCyclesWithAllEvents(stateId)) { // Traverse the sub-graphs if (isResetAfterAnalysis) { @@ -335,6 +344,7 @@ public class StateReducer extends ListenerAdapter { // Set done if this was the last backtrack list icsCG.setDone(); } + saveVisitedStates(); } } else { // Update and reset the CG if needed (do this for the first time after the analysis) @@ -342,13 +352,19 @@ public class StateReducer extends ListenerAdapter { resetAllCGs(); isResetAfterAnalysis = true; } - // Save all the visited states - prevVisitedStates.addAll(currVisitedStates); } + // Update the VOD graph always with the latest + updateVODGraph(icsCG.getNextChoice()); } } } + private void updateVODGraph(int currChoiceValue) { + // Update the graph when we have the current choice value + updateVODGraph(prevChoiceValue, currChoiceValue); + prevChoiceValue = currChoiceValue; + } + private void updateVODGraph(int prevChoice, int currChoice) { HashSet choiceSet; @@ -383,23 +399,6 @@ public class StateReducer extends ListenerAdapter { " which is " + detail + " Transition: " + transition + "\n"); } if (stateReductionMode) { - // Update vodGraph - int currChoice = choiceCounter - 1; - // Adjust currChoice with modulo - currChoice = currChoice >= 0 ? currChoice % (choices.length -1) : currChoice; - if (currChoice < 0 || choices[currChoice] == -1 || - prevChoiceValue == choices[currChoice]) { - // When current choice is 0, previous choice could be -1 -// updateVODGraph(prevChoiceValue, choices[currChoice]); - // Update the state ID variables - stateId = search.getStateId(); - currVisitedStates.add(stateId); - return; - } - // When current choice is 0, previous choice could be -1 - updateVODGraph(prevChoiceValue, choices[currChoice]); - // Current choice becomes previous choice in the next iteration - prevChoiceValue = choices[currChoice]; // Update the state ID variables stateId = search.getStateId(); currVisitedStates.add(stateId); @@ -417,6 +416,7 @@ public class StateReducer extends ListenerAdapter { // Update the state variables // Line 19 in the paper page 11 (see the heading note above) stateId = search.getStateId(); + currVisitedStates.add(stateId); out.println("\n==> DEBUG: The state is backtracked to state with id: " + id + " -- Transition: " + transition + " and depth: " + depth + "\n"); @@ -664,6 +664,10 @@ public class StateReducer extends ListenerAdapter { if (currChoiceNextNodes != null) { // Add only if there is a mapping for next nodes for (Integer nextNode : currChoiceNextNodes) { + // Skip cycles + if (nextNode == currChoice) { + continue; + } nodesToVisit.addLast(nextNode); } } -- 2.34.1