[PEx] Several updates to logging, PEx config

Changes default max choices limit to 20 per call and 250 per schedule (to account for open-source protocols with monolithic transition relation modeled as single action)

Adds logging support to print choose(.) location info for easy debugging TooManyChoicesException via replayer log

Minor correction

Src/PRuntimes/PExRuntime/src/main/java/pex/RuntimeExecutor.java

@@ -165,21 +165,25 @@ private static void process() throws Exception {
             PExLogger.logBugFoundInfo(e.getScheduler());
 
             String schFile = PExGlobal.getConfig().getOutputFolder() + "/" + PExGlobal.getConfig().getProjectName() + "_0_0.schedule";
-            PExLogger.logInfo(String.format("Writing buggy trace in %s", schFile));
+            PExLogger.logInfo(String.format("... Writing buggy trace in %s", schFile));
             e.getScheduler().getSchedule().writeToFile(schFile);
 
-            ReplayScheduler replayer = new ReplayScheduler(e.getScheduler().getSchedule());
+            ReplayScheduler replayer = new ReplayScheduler(e.getScheduler().getSchedule(), e);
             PExGlobal.setReplayScheduler(replayer);
+            PExLogger.logReplayerInfo(replayer);
             try {
                 replayer.run();
             } catch (NullPointerException | StackOverflowError | ClassCastException replayException) {
-                PExLogger.logStackTrace((Exception) replayException);
+                replayer.getLogger().logStackTrace((Exception) replayException);
+                PExLogger.logTrace((Exception) replayException);
                 throw new BugFoundException(replayException.getMessage(), replayException);
             } catch (BugFoundException replayException) {
-                PExLogger.logStackTrace(replayException);
+                replayer.getLogger().logStackTrace(replayException);
+                PExLogger.logTrace(replayException);
                 throw replayException;
             } catch (Exception replayException) {
-                PExLogger.logStackTrace(replayException);
+                replayer.getLogger().logStackTrace(replayException);
+                PExLogger.logTrace(replayException);
                 throw new Exception("Error when replaying the bug", replayException);
             }
             throw new Exception("Failed to replay bug", e);
@@ -218,25 +222,29 @@ public static void runSearch() throws Exception {
     private static void replaySchedule(String fileName) throws Exception {
         PExLogger.logInfo(String.format("... Reading buggy trace from %s", fileName));
 
-        ReplayScheduler replayer = new ReplayScheduler(Schedule.readFromFile(fileName));
+        ReplayScheduler replayer = new ReplayScheduler(Schedule.readFromFile(fileName), null);
         PExGlobal.setReplayScheduler(replayer);
+        PExLogger.logReplayerInfo(replayer);
         try {
             replayer.run();
         } catch (NullPointerException | StackOverflowError | ClassCastException replayException) {
             PExGlobal.setStatus(STATUS.BUG_FOUND);
             PExGlobal.setResult(String.format("found cex of length %d", replayer.getStepNumber()));
-            PExLogger.logStackTrace((Exception) replayException);
+            replayer.getLogger().logStackTrace((Exception) replayException);
+            PExLogger.logTrace((Exception) replayException);
             throw new BugFoundException(replayException.getMessage(), replayException);
         } catch (BugFoundException replayException) {
             PExGlobal.setStatus(STATUS.BUG_FOUND);
             PExGlobal.setResult(String.format("found cex of length %d", replayer.getStepNumber()));
             if (replayException instanceof TooManyChoicesException) {
                 PExGlobal.setResult(PExGlobal.getResult() + " (too many choices)");
             }
-            PExLogger.logStackTrace(replayException);
+            replayer.getLogger().logStackTrace(replayException);
+            PExLogger.logTrace(replayException);
             throw replayException;
         } catch (Exception replayException) {
-            PExLogger.logStackTrace(replayException);
+            replayer.getLogger().logStackTrace(replayException);
+            PExLogger.logTrace(replayException);
             throw new Exception("Error when replaying the bug", replayException);
         } finally {
             printStats();

Src/PRuntimes/PExRuntime/src/main/java/pex/commandline/PExConfig.java

@@ -77,8 +77,8 @@ public class PExConfig {
     int maxChildrenPerTask = 2;
     //max number of choices per choose(.) operation per call
     @Setter
-    int maxChoicesPerStmtPerCall = 10;
+    int maxChoicesPerStmtPerCall = 20;
     //max number of choices per choose(.) operation in total
     @Setter
-    int maxChoicesPerStmtPerSchedule = 100;
+    int maxChoicesPerStmtPerSchedule = 250;
 }

Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/PExLogger.java

@@ -65,7 +65,7 @@ public static void logVerbose(String message) {
      * @param timeSpent Time spent in seconds
      */
     public static void logEndOfRun(long timeSpent) {
-        if (verbosity == 0) {
+        if (verbosity == 0 && PExGlobal.getStatus() != STATUS.BUG_FOUND) {
             log.info("");
         }
         log.info("--------------------");
@@ -97,12 +97,12 @@ public static void logEndOfRun(long timeSpent) {
      *
      * @param e Exception object
      */
-    public static void logStackTrace(Exception e) {
-        StringWriter sw = new StringWriter();
-        PrintWriter pw = new PrintWriter(sw);
-        e.printStackTrace(pw);
-        log.info("--------------------");
-        log.info(sw.toString());
+    public static void logTrace(Exception e) {
+//        StringWriter sw = new StringWriter();
+//        PrintWriter pw = new PrintWriter(sw);
+//        e.printStackTrace(pw);
+//        log.info("--------------------");
+        log.info(String.format(".... \033[31m %s \033[0m", e));
     }
 
     /**
@@ -112,6 +112,15 @@ public static void logStackTrace(Exception e) {
      */
     public static void logBugFoundInfo(Scheduler sch) {
         log.info("--------------------");
-        log.info(String.format("Thread %d found a bug. Details in %s", sch.getSchedulerId(), sch.getLogger().getFileName()));
+        log.info(String.format("... Thread %d found a bug. Details in %s", sch.getSchedulerId(), sch.getLogger().getFileName()));
+    }
+
+    /**
+     * Prints replayer info
+     *
+     * @param sch Replay scheduler
+     */
+    public static void logReplayerInfo(Scheduler sch) {
+        log.info(String.format("... Replaying bug. Details in %s", sch.getLogger().getFileName()));
     }
 }

Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/SchedulerLogger.java

@@ -44,6 +44,10 @@ public class SchedulerLogger {
      */
     public SchedulerLogger(int schId) {
         verbosity = PExGlobal.getConfig().getVerbosity();
+        if (schId == 0 && verbosity == 0) {
+            // set minimum verbosity to 1 for replay scheduler
+            verbosity = 1;
+        }
         log = Log4JConfig.getContext().getLogger(SchedulerLogger.class.getName() + schId);
         org.apache.logging.log4j.core.Logger coreLogger =
                 (org.apache.logging.log4j.core.Logger) LogManager.getLogger(SchedulerLogger.class.getName() + schId);
@@ -207,9 +211,9 @@ public void logNewScheduleChoice(List<PMachineId> choices, int step, int idx) {
         }
     }
 
-    public void logNewDataChoice(List<PValue<?>> choices, int step, int idx) {
+    public void logNewDataChoice(String loc, List<PValue<?>> choices, int step, int idx) {
         if (verbosity > 1) {
-            log.info(String.format("    @%d::%d new data choice: %s", step, idx, choices));
+            log.info(String.format("    @%d::%d %d new data choices from %s - %s", step, idx, choices.size(), loc, choices));
         }
     }
 
@@ -225,15 +229,15 @@ public void logCurrentScheduleChoice(PMachine choice, int step, int idx) {
         }
     }
 
-    public void logRepeatDataChoice(PValue<?> choice, int step, int idx) {
+    public void logRepeatDataChoice(String loc, PValue<?> choice, int step, int idx) {
         if (verbosity > 2) {
-            log.info(String.format("    @%d::%d %s (repeat)", step, idx, choice));
+            log.info(String.format("    @%d::%d %s (repeat) from %s", step, idx, choice, loc));
         }
     }
 
-    public void logCurrentDataChoice(PValue<?> choice, int step, int idx) {
+    public void logCurrentDataChoice(String loc, PValue<?> choice, int step, int idx) {
         if (verbosity > 2) {
-            log.info(String.format("    @%d::%d %s", step, idx, choice));
+            log.info(String.format("    @%d::%d %s from %s", step, idx, choice, loc));
         }
     }
 
@@ -411,4 +415,18 @@ public void logStackTrace(Exception e) {
         log.info("--------------------");
         log.info(sw.toString());
     }
+
+    /**
+     * Print choice loc
+     *
+     * @param step Step number
+     * @param idx Choice number
+     * @param loc choose(.) location
+     * @param choices Data choices
+     */
+    public void logDataChoiceLoc(int step, int idx, String loc, List<PValue<?>> choices) {
+        if (verbosity > 0) {
+            log.info(String.format("    @%d::%d %d new data choices from %s - %s", step, idx, choices.size(), loc, choices));
+        }
+    }
 }

Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/Scheduler.java

@@ -130,7 +130,7 @@ protected void reset() {
      *
      * @return PValue as data choice
      */
-    protected abstract PValue<?> getNextDataChoice(List<PValue<?>> input_choices);
+    protected abstract PValue<?> getNextDataChoice(String loc, List<PValue<?>> input_choices);
 
     public void updateLogNumber() {
         stepNumLogs += 1;
@@ -146,11 +146,11 @@ public void updateLogNumber() {
      */
     public PBool getRandomBool(String loc) {
         List<PValue<?>> choices = new ArrayList<>();
-        stepState.updateChoiceStats(loc, 2);
+        stepState.updateChoiceStats(this, loc, 2);
 
         choices.add(PBool.PTRUE);
         choices.add(PBool.PFALSE);
-        return (PBool) getNextDataChoice(choices);
+        return (PBool) getNextDataChoice(loc, choices);
     }
 
     /**
@@ -165,12 +165,12 @@ public PInt getRandomInt(String loc, PInt bound) {
         if (boundInt == 0) {
             boundInt = 1;
         }
-        stepState.updateChoiceStats(loc, boundInt);
+        stepState.updateChoiceStats(this, loc, boundInt);
 
         for (int i = 0; i < boundInt; i++) {
             choices.add(new PInt(i));
         }
-        return (PInt) getNextDataChoice(choices);
+        return (PInt) getNextDataChoice(loc, choices);
     }
 
     /**

Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/ExplicitSearchScheduler.java

@@ -387,14 +387,14 @@ public PMachine getNextScheduleChoice() {
      * @return PValue as data choice
      */
     @Override
-    public PValue<?> getNextDataChoice(List<PValue<?>> input_choices) {
+    public PValue<?> getNextDataChoice(String loc, List<PValue<?>> input_choices) {
         PValue<?> result;
 
         if (choiceNumber < backtrackChoiceNumber) {
             // pick the current data choice
             result = schedule.getCurrentDataChoice(choiceNumber);
             assert (input_choices.contains(result));
-            logger.logRepeatDataChoice(result, stepNumber, choiceNumber);
+            logger.logRepeatDataChoice(loc, result, stepNumber, choiceNumber);
 
             // increment choice number
             choiceNumber++;
@@ -410,7 +410,7 @@ public PValue<?> getNextDataChoice(List<PValue<?>> input_choices) {
             choices = input_choices;
             if (choices.size() > 1) {
                 // log new choice
-                logger.logNewDataChoice(choices, stepNumber, choiceNumber);
+                logger.logNewDataChoice(loc, choices, stepNumber, choiceNumber);
             }
 
             if (choices.isEmpty()) {
@@ -425,7 +425,7 @@ public PValue<?> getNextDataChoice(List<PValue<?>> input_choices) {
         // pick a choice
         int selected = PExGlobal.getChoiceSelector().selectChoice(this, choices);
         result = choices.get(selected);
-        logger.logCurrentDataChoice(result, stepNumber, choiceNumber);
+        logger.logCurrentDataChoice(loc, result, stepNumber, choiceNumber);
 
         // remove the selected choice from unexplored choices
         choices.remove(selected);

Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/SchedulerStatistics.java

@@ -9,12 +9,12 @@ public class SchedulerStatistics {
     /**
      * Min steps
      */
-    public int minSteps = 0;
+    public int minSteps = -1;
 
     /**
      * Max steps
      */
-    public int maxSteps = 0;
+    public int maxSteps = -1;
 
     /**
      * Total steps

Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/StepState.java

@@ -4,6 +4,8 @@
 import pex.runtime.PExGlobal;
 import pex.runtime.machine.MachineLocalState;
 import pex.runtime.machine.PMachine;
+import pex.runtime.scheduler.Scheduler;
+import pex.runtime.scheduler.replay.ReplayScheduler;
 import pex.utils.exceptions.TooManyChoicesException;
 
 import java.io.Serializable;
@@ -121,7 +123,7 @@ public String getTimelineString() {
         return s.toString();
     }
 
-    public void updateChoiceStats(String loc, int num) {
+    public void updateChoiceStats(Scheduler sch, String loc, int num) {
         if (!choicesNumCalls.containsKey(loc)) {
             choicesNumCalls.put(loc, 1);
             choicesNumChoices.put(loc, num);

Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/replay/ReplayScheduler.java

@@ -1,21 +1,27 @@
 package pex.runtime.scheduler.replay;
 
+import lombok.Getter;
 import pex.runtime.PExGlobal;
 import pex.runtime.logger.ScheduleWriter;
 import pex.runtime.logger.TextWriter;
 import pex.runtime.machine.PMachine;
 import pex.runtime.machine.PMachineId;
 import pex.runtime.scheduler.Schedule;
 import pex.runtime.scheduler.Scheduler;
+import pex.utils.exceptions.BugFoundException;
+import pex.utils.exceptions.TooManyChoicesException;
 import pex.utils.misc.Assert;
 import pex.values.PValue;
 
 import java.util.List;
 import java.util.concurrent.TimeoutException;
 
 public class ReplayScheduler extends Scheduler {
-    public ReplayScheduler(Schedule sch) {
+    @Getter
+    BugFoundException bugFoundException = null;
+    public ReplayScheduler(Schedule sch, BugFoundException e) {
         super(0, sch);
+        bugFoundException = e;
     }
 
     @Override
@@ -105,16 +111,24 @@ protected PMachine getNextScheduleChoice() {
     }
 
     @Override
-    protected PValue<?> getNextDataChoice(List<PValue<?>> input_choices) {
+    protected PValue<?> getNextDataChoice(String loc, List<PValue<?>> input_choices) {
         if (choiceNumber >= schedule.size()) {
             return null;
         }
 
         // pick the current data choice
         PValue<?> result = schedule.getCurrentDataChoice(choiceNumber);
         assert (input_choices.contains(result));
+
         ScheduleWriter.logDataChoice(result);
-        logger.logRepeatDataChoice(result, stepNumber, choiceNumber);
+        logger.logRepeatDataChoice(loc, result, stepNumber, choiceNumber);
+        if (bugFoundException != null) {
+            if (bugFoundException instanceof TooManyChoicesException e) {
+                if (e.getLoc().equals(loc)) {
+                    logger.logDataChoiceLoc(stepNumber, choiceNumber, loc, input_choices);
+                }
+            }
+        }
 
         choiceNumber++;
         return result;

Src/PRuntimes/PExRuntime/src/main/java/pex/utils/exceptions/TooManyChoicesException.java

@@ -1,8 +1,11 @@
 package pex.utils.exceptions;
 
+import lombok.Getter;
 import pex.runtime.PExGlobal;
 
 public class TooManyChoicesException extends BugFoundException {
+    @Getter
+    String loc = "";
     /**
      * Constructs a new TooManyChoicesException for choose(.) with too choices in a single call.
      *
@@ -12,6 +15,7 @@ public class TooManyChoicesException extends BugFoundException {
     public TooManyChoicesException(String loc, int numChoices) {
         super(String.format("%s: choose expects a parameter with at most %d choices, got %d choices instead.",
                 loc, PExGlobal.getConfig().getMaxChoicesPerStmtPerCall(), numChoices));
+        this.loc = loc;
     }
 
     /**
@@ -26,5 +30,6 @@ public TooManyChoicesException(String loc, int numChoices, int numCalls) {
                         %s: too many choices generated from this statement - total %d choices after %d choose calls.
                         Reduce the total number of choices generated here to at most %d, by reducing the number of times this choose statement is called.""",
                 loc, numChoices, numCalls, PExGlobal.getConfig().getMaxChoicesPerStmtPerSchedule()));
+        this.loc = loc;
     }
 }