From c1a4d7c56d0b0f380240319b056398f74c5ab0d1 Mon Sep 17 00:00:00 2001 From: rtrimana Date: Mon, 18 Jan 2021 16:09:59 -0800 Subject: [PATCH] Adding a handler in the listener to check if the benchmark has no event (in this case we don't do DPOR). --- .../jpf/listener/DPORStateReducerWithSummary.java | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java index bdf17a7..6422b7d 100755 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java @@ -80,6 +80,7 @@ public class DPORStateReducerWithSummary extends ListenerAdapter { // Boolean states private boolean isBooleanCGFlipped; private boolean isEndOfExecution; + private boolean isNotCheckedForEventsYet; // Statistics private int numOfTransitions; @@ -100,6 +101,7 @@ public class DPORStateReducerWithSummary extends ListenerAdapter { } } isBooleanCGFlipped = false; + isNotCheckedForEventsYet = true; mainSummary = new MainSummary(); numOfTransitions = 0; nonRelevantClasses = new HashSet<>(); @@ -188,6 +190,17 @@ public class DPORStateReducerWithSummary extends ListenerAdapter { @Override public void choiceGeneratorRegistered(VM vm, ChoiceGenerator nextCG, ThreadInfo currentThread, Instruction executedInstruction) { + if (isNotCheckedForEventsYet) { + // Check if this benchmark has no events + if (nextCG instanceof IntChoiceFromSet) { + IntChoiceFromSet icsCG = (IntChoiceFromSet) nextCG; + Integer[] cgChoices = icsCG.getAllChoices(); + if (cgChoices.length == 2 && cgChoices[0] == 0 && cgChoices[1] == -1) { + stateReductionMode = false; + } + isNotCheckedForEventsYet = false; + } + } if (stateReductionMode) { // Initialize with necessary information from the CG if (nextCG instanceof IntChoiceFromSet) { -- 2.34.1