explicit model checkers: flag to silence log output during precomputations (prob0/1...)

Sometimes, we want to use the prob0/1... methods to generate schedulers instead of doing
the standard precomputations and don't want to have the normal log output.

Not inherited using inheritSettings()

prism/src/explicit/DTMCModelChecker.java

@@ -744,7 +744,8 @@ public class DTMCModelChecker extends ProbModelChecker
 
 		// Start precomputation
 		timer = System.currentTimeMillis();
-		mainLog.println("Starting Prob0...");
+		if (!silentPrecomputations)
+			mainLog.println("Starting Prob0...");
 
 		// Special case: no target states
 		if (target.isEmpty()) {
@@ -765,8 +766,10 @@ public class DTMCModelChecker extends ProbModelChecker
 
 		// Finished precomputation
 		timer = System.currentTimeMillis() - timer;
-		mainLog.print("Prob0");
-		mainLog.println(" took " + timer / 1000.0 + " seconds.");
+		if (!silentPrecomputations) {
+			mainLog.print("Prob0");
+			mainLog.println(" took " + timer / 1000.0 + " seconds.");
+		}
 
 		return result;
 	}
@@ -788,7 +791,8 @@ public class DTMCModelChecker extends ProbModelChecker
 
 		// Start precomputation
 		timer = System.currentTimeMillis();
-		mainLog.println("Starting Prob0...");
+		if (!silentPrecomputations)
+			mainLog.println("Starting Prob0...");
 
 		// Special case: no target states
 		if (target.cardinality() == 0) {
@@ -832,8 +836,10 @@ public class DTMCModelChecker extends ProbModelChecker
 
 		// Finished precomputation
 		timer = System.currentTimeMillis() - timer;
-		mainLog.print("Prob0");
-		mainLog.println(" took " + iters + " iterations and " + timer / 1000.0 + " seconds.");
+		if (!silentPrecomputations) {
+			mainLog.print("Prob0");
+			mainLog.println(" took " + iters + " iterations and " + timer / 1000.0 + " seconds.");
+		}
 
 		return u;
 	}
@@ -854,7 +860,8 @@ public class DTMCModelChecker extends ProbModelChecker
 
 		// Start precomputation
 		timer = System.currentTimeMillis();
-		mainLog.println("Starting Prob1...");
+		if (!silentPrecomputations)
+			mainLog.println("Starting Prob1...");
 
 		// Special case: no 'target' states
 		if (target.isEmpty()) {
@@ -899,8 +906,10 @@ public class DTMCModelChecker extends ProbModelChecker
 
 		// Finished precomputation
 		timer = System.currentTimeMillis() - timer;
-		mainLog.print("Prob1");
-		mainLog.println(" took " + timer / 1000.0 + " seconds.");
+		if (!silentPrecomputations) {
+			mainLog.print("Prob1");
+			mainLog.println(" took " + timer / 1000.0 + " seconds.");
+		}
 
 		return result;
 	}
@@ -922,7 +931,8 @@ public class DTMCModelChecker extends ProbModelChecker
 
 		// Start precomputation
 		timer = System.currentTimeMillis();
-		mainLog.println("Starting Prob1...");
+		if (!silentPrecomputations)
+			mainLog.println("Starting Prob1...");
 
 		// Special case: no target states
 		if (target.cardinality() == 0) {
@@ -974,8 +984,10 @@ public class DTMCModelChecker extends ProbModelChecker
 
 		// Finished precomputation
 		timer = System.currentTimeMillis() - timer;
-		mainLog.print("Prob1");
-		mainLog.println(" took " + iters + " iterations and " + timer / 1000.0 + " seconds.");
+		if (!silentPrecomputations) {
+			mainLog.print("Prob1");
+			mainLog.println(" took " + iters + " iterations and " + timer / 1000.0 + " seconds.");
+		}
 
 		return u;
 	}

prism/src/explicit/MDPModelChecker.java

@@ -602,7 +602,8 @@ public class MDPModelChecker extends ProbModelChecker
 
 		// Start precomputation
 		timer = System.currentTimeMillis();
-		mainLog.println("Starting Prob0 (" + (min ? "min" : "max") + ")...");
+		if (!silentPrecomputations)
+			mainLog.println("Starting Prob0 (" + (min ? "min" : "max") + ")...");
 
 		// Special case: no target states
 		if (target.cardinality() == 0) {
@@ -646,8 +647,10 @@ public class MDPModelChecker extends ProbModelChecker
 
 		// Finished precomputation
 		timer = System.currentTimeMillis() - timer;
-		mainLog.print("Prob0 (" + (min ? "min" : "max") + ")");
-		mainLog.println(" took " + iters + " iterations and " + timer / 1000.0 + " seconds.");
+		if (!silentPrecomputations) {
+			mainLog.print("Prob0 (" + (min ? "min" : "max") + ")");
+			mainLog.println(" took " + iters + " iterations and " + timer / 1000.0 + " seconds.");
+		}
 
 		// If required, generate strategy. This is for min probs,
 		// so it can be done *after* the main prob0 algorithm (unlike for prob1).
@@ -688,7 +691,8 @@ public class MDPModelChecker extends ProbModelChecker
 
 		// Start precomputation
 		timer = System.currentTimeMillis();
-		mainLog.println("Starting Prob1 (" + (min ? "min" : "max") + ")...");
+		if (!silentPrecomputations)
+			mainLog.println("Starting Prob1 (" + (min ? "min" : "max") + ")...");
 
 		// Special case: no target states
 		if (target.cardinality() == 0) {
@@ -766,8 +770,10 @@ public class MDPModelChecker extends ProbModelChecker
 
 		// Finished precomputation
 		timer = System.currentTimeMillis() - timer;
-		mainLog.print("Prob1 (" + (min ? "min" : "max") + ")");
-		mainLog.println(" took " + iters + " iterations and " + timer / 1000.0 + " seconds.");
+		if (!silentPrecomputations) {
+			mainLog.print("Prob1 (" + (min ? "min" : "max") + ")");
+			mainLog.println(" took " + iters + " iterations and " + timer / 1000.0 + " seconds.");
+		}
 
 		return u;
 	}

prism/src/explicit/ProbModelChecker.java

@@ -79,6 +79,8 @@ public class ProbModelChecker extends NonProbModelChecker
 	protected boolean precomp = true;
 	protected boolean prob0 = true;
 	protected boolean prob1 = true;
+	// should we suppress log output during precomputations?
+	protected boolean silentPrecomputations = false;
 	// Use predecessor relation? (e.g. for precomputation)
 	protected boolean preRel = true;
 	// Direction of convergence for value iteration (lfp/gfp)
@@ -291,6 +293,18 @@ public class ProbModelChecker extends NonProbModelChecker
 		this.verbosity = verbosity;
 	}
 
+	/**
+	 * Set flag for suppressing log output during precomputations (prob0, prob1, ...)
+	 * @param value silent?
+	 * @return the previous value of this flag
+	 */
+	public boolean setSilentPrecomputations(boolean value)
+	{
+		boolean old = silentPrecomputations;
+		silentPrecomputations = value;
+		return old;
+	}
+
 	/**
 	 * Set method used to solve linear equation systems.
 	 */