From: rtrimana Date: Thu, 9 Apr 2020 23:44:57 +0000 (-0700) Subject: Testing DPORStateReducer and ConflictTracker: JPF seems to work fine and find the... X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=895d95e4012ea4f6db20abb68410c4ccfc8213f7 Testing DPORStateReducer and ConflictTracker: JPF seems to work fine and find the conflicts. --- diff --git a/main.jpf b/main.jpf index 0665ff2..d6a241e 100644 --- a/main.jpf +++ b/main.jpf @@ -9,7 +9,8 @@ target = main ##listener=gov.nasa.jpf.listener.ConflictTrackerOld,gov.nasa.jpf.listener.StateReducer ##listener=gov.nasa.jpf.listener.ConflictTrackerOld,gov.nasa.jpf.listener.DPORStateReducer ##listener=gov.nasa.jpf.listener.ConflictTrackerOld -listener=gov.nasa.jpf.listener.DPORStateReducer +#listener=gov.nasa.jpf.listener.DPORStateReducer +listener=gov.nasa.jpf.listener.DPORStateReducer,gov.nasa.jpf.listener.ConflictTrackerOld # Potentially conflicting variables # Alarms @@ -43,10 +44,10 @@ apps=App1,App2 # Debug mode for ConflictTracker # We do not report any conflicts if the value is true -#debug_mode=true +debug_mode=true # Debug mode for StateReducer -printout_state_transition=true +#printout_state_transition=true #activate_state_reduction=true # Timeout in minutes (default is 0 which means no timeout) diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java index d8133e3..632edea 100644 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java @@ -28,7 +28,6 @@ import gov.nasa.jpf.vm.bytecode.WriteInstruction; import gov.nasa.jpf.vm.choice.IntChoiceFromSet; import gov.nasa.jpf.vm.choice.IntIntervalGenerator; -import java.awt.*; import java.io.PrintWriter; import java.util.*;