From 90c9e53f8caef91c4c2a4ca44acd96f1c5527acb Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sun, 20 Nov 2011 21:27:26 +0000 Subject: [PATCH] Tweak some warning messages (wrt new log.printWarning method) + add warning message functionality in GUI threads. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4178 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/Modules2MTBDD.java | 6 +- prism/src/prism/NondetModelChecker.java | 10 +-- prism/src/prism/Prism.java | 4 +- prism/src/prism/PrismCL.java | 2 +- prism/src/prism/PrismLog.java | 64 +++++++++++-------- prism/src/prism/ProbModelChecker.java | 19 +++--- prism/src/simulator/SimulatorEngine.java | 6 +- .../userinterface/GUIComputationThread.java | 1 + prism/src/userinterface/GUIPlugin.java | 8 +++ prism/src/userinterface/log/GUILog.java | 4 ++ .../model/computation/BuildModelThread.java | 2 +- .../properties/GUIExperiment.java | 2 +- prism/src/userinterface/util/GUILogEvent.java | 1 + 13 files changed, 76 insertions(+), 53 deletions(-) diff --git a/prism/src/prism/Modules2MTBDD.java b/prism/src/prism/Modules2MTBDD.java index 8cafe41e..bdcd7014 100644 --- a/prism/src/prism/Modules2MTBDD.java +++ b/prism/src/prism/Modules2MTBDD.java @@ -533,7 +533,7 @@ public class Modules2MTBDD break; default: - mainLog.printWarning("Invalid MTBDD ordering selected - it's all going to go wrong.\n"); + mainLog.printWarning("Invalid MTBDD ordering selected - it's all going to go wrong."); break; } @@ -1449,7 +1449,7 @@ public class Modules2MTBDD if (guardDDs[l].equals(JDD.ZERO)) { // display a warning (unless guard is "false", in which case was probably intentional if (!Expression.isFalse(command.getGuard())) { - String s = "Guard for command " + (l+1) + " of module \"" + module.getName() + "\" is never satisfied.\n"; + String s = "Guard for command " + (l+1) + " of module \"" + module.getName() + "\" is never satisfied."; mainLog.printWarning(s); } // no point bothering to compute the mtbdds for the update @@ -1606,7 +1606,7 @@ public class Modules2MTBDD if (!(tmp.equals(JDD.ZERO))) { // if so, output a warning (but carry on regardless) mainLog.printWarning("Guard for command " + (i+1) + " of module \"" - + moduleNames[m] + "\" overlaps with previous commands.\n"); + + moduleNames[m] + "\" overlaps with previous commands."); } JDD.Deref(tmp); // add this command's guard to 'covered' diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 7dbadce7..c95714e2 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -177,11 +177,11 @@ public class NondetModelChecker extends NonProbModelChecker // Check for trivial (i.e. stupid) cases if (pb != null) { if ((p == 0 && relOp.equals(">=")) || (p == 1 && relOp.equals("<="))) { - mainLog.printWarning("Checking for probability " + relOp + " " + p + " - formula trivially satisfies all states\n"); + mainLog.printWarning("Checking for probability " + relOp + " " + p + " - formula trivially satisfies all states"); JDD.Ref(reach); return new StateValuesMTBDD(reach, model); } else if ((p == 0 && relOp.equals("<")) || (p == 1 && relOp.equals(">"))) { - mainLog.printWarning("Checking for probability " + relOp + " " + p + " - formula trivially satisfies no states\n"); + mainLog.printWarning("Checking for probability " + relOp + " " + p + " - formula trivially satisfies no states"); return new StateValuesMTBDD(JDD.Constant(0), model); } } @@ -269,11 +269,11 @@ public class NondetModelChecker extends NonProbModelChecker // check for trivial (i.e. stupid) cases if (rb != null) { if (r == 0 && relOp.equals(">=")) { - mainLog.printWarning("Checking for reward " + relOp + " " + r + " - formula trivially satisfies all states\n"); + mainLog.printWarning("Checking for reward " + relOp + " " + r + " - formula trivially satisfies all states"); JDD.Ref(reach); return new StateValuesMTBDD(reach, model); } else if (r == 0 && relOp.equals("<")) { - mainLog.printWarning("Checking for reward " + relOp + " " + r + " - formula trivially satisfies no states\n"); + mainLog.printWarning("Checking for reward " + relOp + " " + r + " - formula trivially satisfies no states"); return new StateValuesMTBDD(JDD.Constant(0), model); } } @@ -670,7 +670,7 @@ public class NondetModelChecker extends NonProbModelChecker // if requested (i.e. when prob bound is 0 or 1 and precomputation algorithms are enabled), // compute probabilities qualitatively if (qual) { - mainLog.printWarning("Probability bound in formula is" + " 0/1 so exact probabilities may not be computed\n"); + mainLog.print("\nProbability bound in formula is 0/1 so not computing exact probabilities...\n"); // for fairness, we compute max here probs = computeUntilProbsQual(trans01, newb1, newb2, min && !fairness); } diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 051f68e5..bfa1634a 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -1357,12 +1357,12 @@ public class Prism implements PrismSettingsListener // can only do ordered version of export for MDPs if (model.getModelType() == ModelType.MDP) { - if (!ordered) mainLog.printWarning("Cannot export unordered transition reward matrix for MDPs; using ordered"); + if (!ordered) mainLog.printWarning("Cannot export unordered transition reward matrix for MDPs; using ordered."); ordered = true; } // can only do ordered version of export for MRMC if (exportType == EXPORT_MRMC) { - if (!ordered) mainLog.printWarning("Cannot export unordered transition reward matrix in MRMC format; using ordered"); + if (!ordered) mainLog.printWarning("Cannot export unordered transition reward matrix in MRMC format; using ordered."); ordered = true; } // can only do ordered version of export for rows format diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index ea50b499..b4315626 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -755,7 +755,7 @@ public class PrismCL } // if requested, remove them else if (fixdl) { - mainLog.printWarning(states.size() + " deadlock states detected; adding self-loops in these states...\n"); + mainLog.printWarning(states.size() + " deadlock states detected; adding self-loops in these states..."); model.fixDeadlocks(); } // otherwise print error and bail out diff --git a/prism/src/prism/PrismLog.java b/prism/src/prism/PrismLog.java index d7ccd7ba..9396bff1 100644 --- a/prism/src/prism/PrismLog.java +++ b/prism/src/prism/PrismLog.java @@ -27,7 +27,7 @@ package prism; public abstract class PrismLog -{ +{ /** * Specifies that only more important messages should be printed */ @@ -40,14 +40,14 @@ public abstract class PrismLog * Specifies that all messages should be printed */ public static final int VL_ALL = 2; - + protected int verbosityLevel = VL_DEFAULT; /** * Keeps the count of warnings printed printed so far. */ protected int numberOfWarnings = 0; - + /** * Sets the counter of warnings that was printed to 0. */ @@ -55,7 +55,7 @@ public abstract class PrismLog { this.numberOfWarnings = 0; } - + /** * Returns the number of warnings that have been printed since the beginning * or since the last reset of number of warnings. @@ -65,7 +65,7 @@ public abstract class PrismLog { return this.numberOfWarnings; } - + /** * Returns the verbosity level of this log. The verbosity level * determines what messages will be printed. @@ -75,7 +75,7 @@ public abstract class PrismLog { return verbosityLevel; } - + /** * Changes the verbosity level of this log. The verbosity level * determines what messages will be printed. @@ -85,22 +85,33 @@ public abstract class PrismLog { this.verbosityLevel = verbosityLevel; } - + public abstract boolean ready(); + public abstract long getFilePointer(); + public abstract void flush(); + public abstract void close(); - + public abstract void print(boolean b); + public abstract void print(char c); + public abstract void print(double d); + public abstract void print(float f); + public abstract void print(int i); + public abstract void print(long l); + public abstract void print(Object obj); + public abstract void print(String s); + public abstract void println(); - + /** * Prints out the value of {@code b} if the log's verbosity level is at least {@code level} */ @@ -109,7 +120,7 @@ public abstract class PrismLog if (level >= this.verbosityLevel) print(b); } - + /** * Prints out the value of {@code c} if the log's verbosity level is at least {@code level} */ @@ -118,7 +129,7 @@ public abstract class PrismLog if (level >= this.verbosityLevel) print(c); } - + /** * Prints out the value of {@code d} if the log's verbosity level is at least {@code level} */ @@ -127,7 +138,7 @@ public abstract class PrismLog if (level >= this.verbosityLevel) print(d); } - + /** * Prints out the value of {@code f} if the log's verbosity level is at least {@code level} */ @@ -136,16 +147,16 @@ public abstract class PrismLog if (level >= this.verbosityLevel) print(f); } - + /** * Prints out the value of {@code i} if the log's verbosity level is at least {@code level} */ public void print(int i, int level) { if (level >= this.verbosityLevel) - print(i); + print(i); } - + /** * Prints out the value of {@code l} if the log's verbosity level is at least {@code level} */ @@ -154,7 +165,7 @@ public abstract class PrismLog if (level >= this.verbosityLevel) print(l); } - + /** * Prints out the value of {@code obj} if the log's verbosity level is at least {@code level} */ @@ -163,7 +174,7 @@ public abstract class PrismLog if (level >= this.verbosityLevel) print(obj); } - + /** * Prints out {@code s} if the log's verbosity level is at least {@code level} */ @@ -172,7 +183,7 @@ public abstract class PrismLog if (level >= this.verbosityLevel) print(s); } - + /** * Prints out the content of {@code arr} if the log's verbosity level is at least {@code level} */ @@ -181,7 +192,7 @@ public abstract class PrismLog if (level >= this.verbosityLevel) print(arr); } - + public void print(double arr[]) { int i, n = arr.length; @@ -263,7 +274,7 @@ public abstract class PrismLog print(arr); println(); } - + /** * Prints out the value of {@code b} followed by a newline character, provided that the log's verbosity level is at least {@code level} */ @@ -353,18 +364,17 @@ public abstract class PrismLog if (level >= this.verbosityLevel) println(arr); } - + /** - * Prints a warning message {@code s}, preceded by "\\nWarning: " string - * and followed by a newline characted. + * Prints a warning message {@code s}, preceded by "\nWarning: " and followed by a newline character. *

- * Also increases {@link #numberOfWarnings} by one. This variable can be then + * Also increases {@link #numberOfWarnings} by one. This variable can then be * queried using {@link #getNumberOfWarnings()} at the end of computation - * and the user can be appropriately informed that there were warnings - * generated. + * and the user can be appropriately informed that there were warnings generated. * @param s The warning message. */ - public void printWarning(String s) { + public void printWarning(String s) + { println("\nWarning: " + s); this.numberOfWarnings++; } diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index 0e242de2..3f1ae658 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -176,19 +176,19 @@ public class ProbModelChecker extends NonProbModelChecker if (pb != null) { if ((p == 0 && relOp.equals(">=")) || (p == 1 && relOp.equals("<="))) { mainLog.printWarning("Checking for probability " + relOp + " " + p - + " - formula trivially satisfies all states\n"); + + " - formula trivially satisfies all states"); JDD.Ref(reach); return new StateValuesMTBDD(reach, model); } else if ((p == 0 && relOp.equals("<")) || (p == 1 && relOp.equals(">"))) { mainLog.printWarning("Checking for probability " + relOp + " " + p - + " - formula trivially satisfies no states\n"); + + " - formula trivially satisfies no states"); return new StateValuesMTBDD(JDD.Constant(0), model); } } // Print a warning if Pmin/Pmax used if (relOp.equals("min=") || relOp.equals("max=")) { - mainLog.printWarning("\"Pmin=?\" and \"Pmax=?\" operators are identical to \"P=?\" for DTMCs/CTMCs\n"); + mainLog.printWarning("\"Pmin=?\" and \"Pmax=?\" operators are identical to \"P=?\" for DTMCs/CTMCs"); } // Compute probabilities @@ -263,19 +263,19 @@ public class ProbModelChecker extends NonProbModelChecker if (rb != null) { if (r == 0 && relOp.equals(">=")) { mainLog.printWarning("Checking for reward " + relOp + " " + r - + " - formula trivially satisfies all states\n"); + + " - formula trivially satisfies all states"); JDD.Ref(reach); return new StateValuesMTBDD(reach, model); } else if (r == 0 && relOp.equals("<")) { mainLog.printWarning("Checking for reward " + relOp + " " + r - + " - formula trivially satisfies no states\n"); + + " - formula trivially satisfies no states"); return new StateValuesMTBDD(JDD.Constant(0), model); } } // print a warning if Rmin/Rmax used if (relOp.equals("min=") || relOp.equals("max=")) { - mainLog.printWarning("\"Rmin=?\" and \"Rmax=?\" operators are identical to \"R=?\" for DTMCs/CTMCs\n"); + mainLog.printWarning("\"Rmin=?\" and \"Rmax=?\" operators are identical to \"R=?\" for DTMCs/CTMCs"); } // compute rewards @@ -352,12 +352,12 @@ public class ProbModelChecker extends NonProbModelChecker if (pb != null) { if ((p == 0 && relOp.equals(">=")) || (p == 1 && relOp.equals("<="))) { mainLog.printWarning("Checking for probability " + relOp + " " + p - + " - formula trivially satisfies all states\n"); + + " - formula trivially satisfies all states"); JDD.Ref(reach); return new StateValuesMTBDD(reach, model); } else if ((p == 0 && relOp.equals("<")) || (p == 1 && relOp.equals(">"))) { mainLog.printWarning("Checking for probability " + relOp + " " + p - + " - formula trivially satisfies no states\n"); + + " - formula trivially satisfies no states"); return new StateValuesMTBDD(JDD.Constant(0), model); } } @@ -802,8 +802,7 @@ public class ProbModelChecker extends NonProbModelChecker // if requested (i.e. when prob bound is 0 or 1 and precomputation algorithms are enabled), // compute probabilities qualitatively if (qual) { - mainLog.printWarning("Probability bound in formula is" - + " 0/1 so exact probabilities may not be computed\n"); + mainLog.print("\nProbability bound in formula is 0/1 so not computing exact probabilities...\n"); probs = computeUntilProbsQual(trans01, b1, b2); } // otherwise actually compute probabilities diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index cfcd6fca..7a52e242 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -610,7 +610,7 @@ public class SimulatorEngine public Object queryProperty(int index) { if (index < 0 || index >= propertySamplers.size()) { - mainLog.printWarning("Can't query property " + index); + mainLog.printWarning("Can't query property " + index + "."); return null; } Sampler sampler = propertySamplers.get(index); @@ -1589,11 +1589,11 @@ public class SimulatorEngine // Print a warning if deadlocks occurred at any point if (deadlocksFound) - mainLog.printWarning("Deadlocks were found during simulation: self-loops were added\n"); + mainLog.printWarning("Deadlocks were found during simulation: self-loops were added."); // Print a warning if simulation was stopped by the user if (shouldStopSampling) - mainLog.printWarning("Simulation was terminated before completion.\n"); + mainLog.printWarning("Simulation was terminated before completion."); // write to feedback file with true to indicate that we have finished sampling // Write_Feedback(iteration_counter, numIters, true); diff --git a/prism/src/userinterface/GUIComputationThread.java b/prism/src/userinterface/GUIComputationThread.java index 3ddbfb3c..5a8b09cc 100644 --- a/prism/src/userinterface/GUIComputationThread.java +++ b/prism/src/userinterface/GUIComputationThread.java @@ -71,6 +71,7 @@ public class GUIComputationThread extends Thread public void logln(short s) { plug.logln(s); } public void logln(byte b) { plug.logln(b); } public void logln(boolean b) { plug.logln(b); } + public void logWarning(String s) { plug.logWarning(s); } // pop up an error dialog public void errorDialog(String s) diff --git a/prism/src/userinterface/GUIPlugin.java b/prism/src/userinterface/GUIPlugin.java index 3e777f01..c88cc51b 100644 --- a/prism/src/userinterface/GUIPlugin.java +++ b/prism/src/userinterface/GUIPlugin.java @@ -541,6 +541,14 @@ public abstract class GUIPlugin extends JPanel implements GUIEventListener, Pris gui.enableTab(this, enabled); } + /** Method to add a warning message to the log contained within the parent GUIPrism. + * @param message The message to be added to the log + */ + public void logWarning(String message) + { + notifyEventListeners(new GUILogEvent(GUILogEvent.PRINTWARNING, message)); + } + /** Utility method to automatically jump this plugin to the front of the tabs * contained within the parent GUIPrism. */ diff --git a/prism/src/userinterface/log/GUILog.java b/prism/src/userinterface/log/GUILog.java index 1ea8674c..d582bc47 100644 --- a/prism/src/userinterface/log/GUILog.java +++ b/prism/src/userinterface/log/GUILog.java @@ -122,6 +122,10 @@ public class GUILog extends GUIPlugin implements MouseListener, PrismSettingsLis { theLog.print(le.getData()); } + else if(le.getID() == le.PRINTWARNING) + { + theLog.printWarning((String) le.getData()); + } } else if (e instanceof GUIClipboardEvent && super.getGUI().getFocussedPlugin() == this) { diff --git a/prism/src/userinterface/model/computation/BuildModelThread.java b/prism/src/userinterface/model/computation/BuildModelThread.java index 8970fc71..e1a5e42a 100644 --- a/prism/src/userinterface/model/computation/BuildModelThread.java +++ b/prism/src/userinterface/model/computation/BuildModelThread.java @@ -212,7 +212,7 @@ public class BuildModelThread extends GUIComputationThread String[] options = {"Continue", "Display deadlocks"}; int choice = plug.question("Error", "Error: Model contains deadlock states.\nAdd self-loops to these states and continue?\nOr stop and display deadlock states in log?", options); if (choice == 0) { - log("\nWarning: " + deadlocks.size() + " deadlock states detected; adding self-loops in these states...\n"); + logWarning(deadlocks.size() + " deadlock states detected; adding self-loops in these states..."); model.fixDeadlocks(); } else { diff --git a/prism/src/userinterface/properties/GUIExperiment.java b/prism/src/userinterface/properties/GUIExperiment.java index 91380bbb..b3c47a63 100644 --- a/prism/src/userinterface/properties/GUIExperiment.java +++ b/prism/src/userinterface/properties/GUIExperiment.java @@ -285,7 +285,7 @@ public class GUIExperiment StateList states = model.getDeadlockStates(); if (states != null) { if (states.size() > 0) { - guiProp.log("\nWarning: " + states.size() + " deadlock states detected; adding self-loops in these states...\n"); + guiProp.logWarning(states.size() + " deadlock states detected; adding self-loops in these states..."); model.fixDeadlocks(); } } diff --git a/prism/src/userinterface/util/GUILogEvent.java b/prism/src/userinterface/util/GUILogEvent.java index 14e05527..2b33578e 100644 --- a/prism/src/userinterface/util/GUILogEvent.java +++ b/prism/src/userinterface/util/GUILogEvent.java @@ -31,6 +31,7 @@ public class GUILogEvent extends GUIEvent { public static final int PRINTLN = 0; public static final int PRINT = 1; + public static final int PRINTWARNING = 2; /** * Constructs an instance of GUILogEvent with the specified detail message.