diff --git a/prism/src/explicit/ConstructModel.java b/prism/src/explicit/ConstructModel.java index 20a6bd09..78cabc91 100644 --- a/prism/src/explicit/ConstructModel.java +++ b/prism/src/explicit/ConstructModel.java @@ -128,7 +128,7 @@ public class ConstructModel Distribution distr = null; // Misc int i, j, nc, nt, src, dest; - long timer, timerProgress; + long timer; // Don't support multiple initial states if (modulesFile.getInitialStates() != null) { @@ -136,9 +136,11 @@ public class ConstructModel } // Starting reachability... - mainLog.print("\nComputing reachable states..."); + mainLog.print("\nComputing reachable states... "); mainLog.flush(); - timer = timerProgress = System.currentTimeMillis(); + ProgressDisplay progress = new ProgressDisplay(mainLog); + progress.start(); + timer = System.currentTimeMillis(); // Initialise simulator for this model modelType = modulesFile.getModelType(); @@ -242,17 +244,13 @@ public class ConstructModel } } } - // Print some progress info occasionally - if (System.currentTimeMillis() - timerProgress > 3000) { - mainLog.print(" " + (src + 1)); - mainLog.flush(); - timerProgress = System.currentTimeMillis(); - } + progress.updateIfReady(src + 1); } // Finish progress display - mainLog.println(" " + (src + 1)); + progress.update(src + 1); + progress.end(); // Reachability complete mainLog.print("Reachable states exploration" + (justReach ? "" : " and model construction")); diff --git a/prism/src/prism/ExplicitModel2MTBDD.java b/prism/src/prism/ExplicitModel2MTBDD.java index 0d9e30e2..351b076c 100644 --- a/prism/src/prism/ExplicitModel2MTBDD.java +++ b/prism/src/prism/ExplicitModel2MTBDD.java @@ -391,6 +391,7 @@ public class ExplicitModel2MTBDD nnz = modelExpl.getNumTransitions(); count = 0; progress = new ProgressDisplay(mainLog); + progress.setTotalCount(nnz); progress.start(); // Case for DTMCs/CTMCs... if (modelType == ModelType.DTMC || modelType == ModelType.CTMC) { @@ -433,10 +434,7 @@ public class ExplicitModel2MTBDD // deref element dd JDD.Deref(elem); // Print some progress info occasionally - count++; - if (progress.ready()) { - progress.update((100.0 * count) / nnz); - } + progress.updateIfReady(++count); } } } @@ -477,10 +475,7 @@ public class ExplicitModel2MTBDD // deref element dd JDD.Deref(elem); // Print some progress info occasionally - count++; - if (progress.ready()) { - progress.update((100.0 * count) / nnz); - } + progress.updateIfReady(++count); } } } @@ -488,7 +483,7 @@ public class ExplicitModel2MTBDD throw new PrismException("Unknown model type"); } // Tidy up progress display - progress.update(100.0); + progress.update(nnz); progress.end(); } diff --git a/prism/src/prism/ProgressDisplay.java b/prism/src/prism/ProgressDisplay.java index 24e7578e..5f6e6e19 100644 --- a/prism/src/prism/ProgressDisplay.java +++ b/prism/src/prism/ProgressDisplay.java @@ -27,7 +27,7 @@ package prism; /** - * Class to display percentage progress meter to a log. + * Class to display progress meter to a log, either as percentages or just a counter. */ public class ProgressDisplay { @@ -36,45 +36,110 @@ public class ProgressDisplay // Config /** Minimum delay between updates (milliseconds); */ private int delay = 3000; - /** Display progress as multiples of this number */ - private int multiple = 2; + /** Display progress as multiples of this number */ + private int percentMultiple = 2; // Current state - private int lastPercentageDone; + private long totalCount; + private long lastCount; + private long lastPercentageDone; private long timerProgress; - + private boolean first; + public ProgressDisplay(PrismLog mainLog) { this.mainLog = mainLog; } - + + /** + * Initialise; start the timer. + */ public void start() { + lastCount = 0; lastPercentageDone = 0; timerProgress = System.currentTimeMillis(); - mainLog.print("["); + first = true; } - + + /** + * Set total count expected, thus triggering percentage mode. + */ + public void setTotalCount(long totalCount) + { + this.totalCount = totalCount; + } + + /** + * Is it time for the next update? + */ public boolean ready() { return System.currentTimeMillis() - timerProgress > delay; } + + /** + * Display an update, if it is ready and anything changed. + */ + public void updateIfReady(long count) + { + if (ready()) + update(count); + } - public void update(double percentageDone) + /** + * Display an update, if anything changed. + */ + public void update(long count) { - // Round percentage down to nearest multiple of 'multiple' - int percentageDoneRound = (int) Math.floor(percentageDone); - percentageDoneRound = (percentageDoneRound / multiple) * multiple; - // Print if new - if (percentageDoneRound > lastPercentageDone) { - lastPercentageDone = percentageDoneRound; - mainLog.print(" " + percentageDoneRound + "%"); - mainLog.flush(); - timerProgress = System.currentTimeMillis(); + // Percentage mode + if (totalCount != -1) { + // Compute percentage, round down to nearest multiple of 'multiple' + int percentageDoneRound; + if (count >= totalCount) { + percentageDoneRound = 100; + } else { + percentageDoneRound = (int) Math.floor((100.0 * count) / totalCount); + percentageDoneRound = (percentageDoneRound / percentMultiple) * percentMultiple; + } + // Print if new + if (percentageDoneRound > lastPercentageDone) { + if (first) { + mainLog.print("["); + first = false; + } + lastPercentageDone = percentageDoneRound; + mainLog.print(" " + percentageDoneRound + "%"); + mainLog.flush(); + timerProgress = System.currentTimeMillis(); + } + } + // Counter mode + else { + // Print if new + if (count > lastCount) { + lastCount = count; + mainLog.print(" " + count); + mainLog.flush(); + timerProgress = System.currentTimeMillis(); + } } } - + + /** + * Finish up. + */ public void end() { - mainLog.println(" ]"); + end(""); + } + + /** + * Finish up, displaying {@code text} first. + */ + public void end(String text) + { + mainLog.print(text); + if (totalCount != -1) + mainLog.println(" ]"); } }