diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index aef58b00..aa8f9b39 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/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; } diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index be909905..1f015899 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/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; } diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index 0b5d16fe..d4454b48 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/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. */