From d3dd8a7ac19240bf350b968853d36aaa02b7cbaf Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Fri, 23 Mar 2012 15:30:26 +0000
Subject: [PATCH] Adapt some classes to use new ProgressDisplay.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4947 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/explicit/ConstructModel.java |  4 ++--
 prism/src/pta/ForwardsReach.java       | 26 ++++++++++----------------
 2 files changed, 12 insertions(+), 18 deletions(-)

diff --git a/prism/src/explicit/ConstructModel.java b/prism/src/explicit/ConstructModel.java
index 78cabc91..ce227a02 100644
--- a/prism/src/explicit/ConstructModel.java
+++ b/prism/src/explicit/ConstructModel.java
@@ -136,7 +136,7 @@ public class ConstructModel
 		}
 
 		// Starting reachability...
-		mainLog.print("\nComputing reachable states... ");
+		mainLog.print("\nComputing reachable states...");
 		mainLog.flush();
 		ProgressDisplay progress = new ProgressDisplay(mainLog);
 		progress.start();
@@ -250,7 +250,7 @@ public class ConstructModel
 
 		// Finish progress display
 		progress.update(src + 1);
-		progress.end();
+		progress.end(" states");
 
 		// Reachability complete
 		mainLog.print("Reachable states exploration" + (justReach ? "" : " and model construction"));
diff --git a/prism/src/pta/ForwardsReach.java b/prism/src/pta/ForwardsReach.java
index 3bd7243c..a1533cfb 100644
--- a/prism/src/pta/ForwardsReach.java
+++ b/prism/src/pta/ForwardsReach.java
@@ -94,17 +94,18 @@ public class ForwardsReach
 		ReachabilityGraph graph;
 		int src, dest, count, dests[];
 		boolean canDiverge;
-		long timer, timerProgress;
-		boolean progressDisplayed;
+		long timer;
 
 		// Store target info
 		this.targetLocs = targetLocs;
 		this.targetConstraint = targetConstraint;
 
 		// Starting reachability...
-		mainLog.println("\nBuilding forwards reachability graph...");
-		timer = timerProgress = System.currentTimeMillis();
-		progressDisplayed = false;
+		mainLog.print("\nBuilding forwards reachability graph...");
+		mainLog.flush();
+		ProgressDisplay progress = new ProgressDisplay(mainLog);
+		progress.start();
+		timer = System.currentTimeMillis();
 
 		// Re-compute max clock constraint value if required
 		if (targetConstraint != null)
@@ -231,20 +232,13 @@ public class ForwardsReach
 				throw new PrismException(s);
 			}
 			// Print some progress info occasionally
-			if (System.currentTimeMillis() - timerProgress > 3000) {
-				if (!progressDisplayed) {
-					mainLog.print("Number of states so far:");
-					progressDisplayed = true;
-				}
-				mainLog.print(" " + Yset.size());
-				mainLog.flush();
-				timerProgress = System.currentTimeMillis();
-			}
+			if (progress.ready())
+				progress.update(Yset.size());
 		}
 
 		// Tidy up progress display
-		if (progressDisplayed)
-			mainLog.println(" " + Yset.size());
+		progress.update(Yset.size());
+		progress.end(" states");
 
 		// Convert state set to ArrayList and store
 		graph.states = Yset.toArrayList();