From 87594ff533502d7145f07c0974ea4fc5399d1cac Mon Sep 17 00:00:00 2001 From: rtrimana Date: Thu, 9 Apr 2020 16:18:40 -0700 Subject: [PATCH] Fixing a bug: VOD graph traversal should continue with the next neighbor when there is a loop (repeated node found). --- src/main/gov/nasa/jpf/listener/DPORStateReducer.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java index 7d5546c..f9d79c5 100644 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java @@ -796,8 +796,8 @@ public class DPORStateReducer extends ListenerAdapter { if (choice == currEvent) { return true; } - if (visitedChoice.contains(choice)) { // If there is a loop then we don't find it - return false; + if (visitedChoice.contains(choice)) { // If there is a loop then just continue the exploration + continue; } // Continue searching visitedChoice.add(choice); -- 2.34.1