Improved ProgressDisplay class.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4945 bbc10eb1-c90d-0410-af57-cb519fbb1720

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) {
@@ -138,7 +138,9 @@ public class ConstructModel
 		// Starting reachability...
 		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"));

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();
 	}
 

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
 {
@@ -37,44 +37,109 @@ public class ProgressDisplay
 	/** Minimum delay between updates (milliseconds); */
 	private int delay = 3000;
 	/** Display progress as multiples of this number */
-	private int multiple = 2;
+	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;
 	}
 
-	public void update(double percentageDone)
+	/**
+	 * Display an update, if it is ready and anything changed.
+	 */
+	public void updateIfReady(long count)
+	{
+		if (ready())
+			update(count);
+	}
+	
+	/**
+	 * 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;
+		// 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()
 	{
+		end("");
+	}
+
+	/**
+	 * Finish up, displaying {@code text} first.
+	 */
+	public void end(String text)
+	{
+		mainLog.print(text);
+		if (totalCount != -1)
 			mainLog.println(" ]");
 	}
 }