Browse Source

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
master
Dave Parker 14 years ago
parent
commit
90c9e53f8c
  1. 6
      prism/src/prism/Modules2MTBDD.java
  2. 10
      prism/src/prism/NondetModelChecker.java
  3. 4
      prism/src/prism/Prism.java
  4. 2
      prism/src/prism/PrismCL.java
  5. 64
      prism/src/prism/PrismLog.java
  6. 19
      prism/src/prism/ProbModelChecker.java
  7. 6
      prism/src/simulator/SimulatorEngine.java
  8. 1
      prism/src/userinterface/GUIComputationThread.java
  9. 8
      prism/src/userinterface/GUIPlugin.java
  10. 4
      prism/src/userinterface/log/GUILog.java
  11. 2
      prism/src/userinterface/model/computation/BuildModelThread.java
  12. 2
      prism/src/userinterface/properties/GUIExperiment.java
  13. 1
      prism/src/userinterface/util/GUILogEvent.java

6
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'

10
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);
}

4
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

2
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

64
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.
* <p/>
* 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++;
}

19
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

6
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);

1
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)

8
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.
*/

4
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)
{

2
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 {

2
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();
}
}

1
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 <code>GUILogEvent</code> with the specified detail message.

Loading…
Cancel
Save