From a14171b0b869d72380021f292a955064de942e4a Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Mon, 28 Aug 2017 12:45:46 +0200 Subject: [PATCH] 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 | 36 ++++++++++++++++-------- prism/src/explicit/MDPModelChecker.java | 18 ++++++++---- prism/src/explicit/ProbModelChecker.java | 14 +++++++++ 3 files changed, 50 insertions(+), 18 deletions(-) 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. */