diff --git a/prism/src/explicit/PrismExplicit.java b/prism/src/explicit/PrismExplicit.java index 5a64bf8f..e18fd349 100644 --- a/prism/src/explicit/PrismExplicit.java +++ b/prism/src/explicit/PrismExplicit.java @@ -103,7 +103,7 @@ public class PrismExplicit { // can only do ordered version of export for explicit engine if (!ordered) { - mainLog.println("\nWarning: Cannot export unordered transition matrix with the explicit engine; using ordered."); + mainLog.printWarning("Cannot export unordered transition matrix with the explicit engine; using ordered."); ordered = true; } // print message diff --git a/prism/src/explicit/QuantAbstractRefine.java b/prism/src/explicit/QuantAbstractRefine.java index cf37dcc5..26836f5f 100644 --- a/prism/src/explicit/QuantAbstractRefine.java +++ b/prism/src/explicit/QuantAbstractRefine.java @@ -1013,7 +1013,7 @@ public abstract class QuantAbstractRefine // Don't refine a state that we have already modified through refinement if (rebuiltStates.contains(refineState)) { if (verbosity >= 1) - mainLog.println("Warning: Skipping refinement of #" + refineState + mainLog.printWarning("Skipping refinement of #" + refineState + " which has already been modified by refinement."); return 1; } @@ -1070,7 +1070,7 @@ public abstract class QuantAbstractRefine // Check if lb/ub are identical (just use equals() since lists are sorted) if (lbStrat.equals(ubStrat) && lbStrat.size() == abstraction.getNumChoices(refineState)) { if (verbosity >= 1) - mainLog.println("Warning: Skipping refinement of #" + refineState + mainLog.printWarning("Skipping refinement of #" + refineState + " for which lb/ub strategy sets are equal and covering."); return 1; } diff --git a/prism/src/prism/Modules2MTBDD.java b/prism/src/prism/Modules2MTBDD.java index 8f94d4cb..8cafe41e 100644 --- a/prism/src/prism/Modules2MTBDD.java +++ b/prism/src/prism/Modules2MTBDD.java @@ -533,7 +533,7 @@ public class Modules2MTBDD break; default: - mainLog.print("\nWarning: 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.\n"); break; } @@ -1449,8 +1449,8 @@ 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 = "\nWarning: Guard for command " + (l+1) + " of module \"" + module.getName() + "\" is never satisfied.\n"; - mainLog.print(s); + String s = "Guard for command " + (l+1) + " of module \"" + module.getName() + "\" is never satisfied.\n"; + mainLog.printWarning(s); } // no point bothering to compute the mtbdds for the update // if the guard is never satisfied @@ -1605,8 +1605,8 @@ public class Modules2MTBDD tmp = JDD.And(guardDDs[i], covered); if (!(tmp.equals(JDD.ZERO))) { // if so, output a warning (but carry on regardless) - mainLog.print("\nWarning: Guard for command " + (i+1) + " of module \""); - mainLog.print(moduleNames[m] + "\" overlaps with previous commands.\n"); + mainLog.printWarning("Guard for command " + (i+1) + " of module \"" + + moduleNames[m] + "\" overlaps with previous commands.\n"); } JDD.Deref(tmp); // add this command's guard to 'covered' @@ -1878,7 +1878,7 @@ public class Modules2MTBDD // Use a PrismLangException to get line numbers displayed msg = "Update " + (i+1) + " of command " + (l+1); msg += " of module \"" + moduleNames[m] + "\" doesn't do anything"; - mainLog.println("\nWarning: " + new PrismLangException(msg, u.getUpdate(i)).getMessage()); + mainLog.printWarning(new PrismLangException(msg, u.getUpdate(i)).getMessage()); } // multiply by probability/rate p = u.getProbability(i); @@ -1890,7 +1890,7 @@ public class Modules2MTBDD // Use a PrismLangException to get line numbers displayed msg = "Update " + (i+1) + " of command " + (l+1); msg += " of module \"" + moduleNames[m] + "\" doesn't do anything"; - mainLog.println("\nWarning: " + new PrismLangException(msg, u.getUpdate(i)).getMessage()); + mainLog.printWarning(new PrismLangException(msg, u.getUpdate(i)).getMessage()); } dd = JDD.Apply(JDD.PLUS, dd, udd); } diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index c4024136..763ab43e 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -86,10 +86,10 @@ public class NondetModelChecker extends NonProbModelChecker // Display warning and/or make changes for some option combinations if (prism.getExportAdv() != Prism.EXPORT_ADV_NONE) { if (engine != Prism.SPARSE) { - mainLog.println("\nWarning: Adversary generation is only implemented for the sparse engine"); + mainLog.printWarning("Adversary generation is only implemented for the sparse engine"); } if (precomp && prob1) { - mainLog.println("\nWarning: Disabling Prob1 since this is needed for adversary generation"); + mainLog.printWarning("Disabling Prob1 since this is needed for adversary generation"); prob1 = false; } } @@ -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.print("\nWarning: checking for probability " + relOp + " " + p + " - formula trivially satisfies all states\n"); + mainLog.printWarning("Checking for probability " + relOp + " " + p + " - formula trivially satisfies all states\n"); JDD.Ref(reach); return new StateValuesMTBDD(reach, model); } else if ((p == 0 && relOp.equals("<")) || (p == 1 && relOp.equals(">"))) { - mainLog.print("\nWarning: checking for probability " + relOp + " " + p + " - formula trivially satisfies no states\n"); + mainLog.printWarning("Checking for probability " + relOp + " " + p + " - formula trivially satisfies no states\n"); 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.print("\nWarning: checking for reward " + relOp + " " + r + " - formula trivially satisfies all states\n"); + mainLog.printWarning("Checking for reward " + relOp + " " + r + " - formula trivially satisfies all states\n"); JDD.Ref(reach); return new StateValuesMTBDD(reach, model); } else if (r == 0 && relOp.equals("<")) { - mainLog.print("\nWarning: checking for reward " + relOp + " " + r + " - formula trivially satisfies no states\n"); + mainLog.printWarning("Checking for reward " + relOp + " " + r + " - formula trivially satisfies no states\n"); return new StateValuesMTBDD(JDD.Constant(0), model); } } @@ -456,7 +456,7 @@ public class NondetModelChecker extends NonProbModelChecker mainLog.println("\nExporting product transition matrix to file \"" + prism.getExportProductTransFilename() + "\"..."); prism.exportTransToFile(modelProduct, true, Prism.EXPORT_PLAIN, new File(prism.getExportProductTransFilename())); } catch (FileNotFoundException e) { - mainLog.println("\nWarning: Could not export product transition matrix to file \"" + prism.getExportProductTransFilename() + "\""); + mainLog.printWarning("Could not export product transition matrix to file \"" + prism.getExportProductTransFilename() + "\""); } } if (prism.getExportProductStates()) { @@ -465,7 +465,7 @@ public class NondetModelChecker extends NonProbModelChecker prism.exportTransToFile(modelProduct, true, Prism.EXPORT_PLAIN, new File(prism.getExportProductStatesFilename())); prism.exportStatesToFile(modelProduct, Prism.EXPORT_PLAIN, new File(prism.getExportProductStatesFilename())); } catch (FileNotFoundException e) { - mainLog.println("\nWarning: Could not export product state space to file \"" + prism.getExportProductStatesFilename() + "\""); + mainLog.printWarning("Could not export product state space to file \"" + prism.getExportProductStatesFilename() + "\""); } } @@ -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.print("\nWarning: probability bound in formula is" + " 0/1 so exact probabilities may not be computed\n"); + mainLog.printWarning("Probability bound in formula is" + " 0/1 so exact probabilities may not be computed\n"); // for fairness, we compute max here probs = computeUntilProbsQual(trans01, newb1, newb2, min && !fairness); } @@ -975,7 +975,7 @@ public class NondetModelChecker extends NonProbModelChecker mainLog.println("\nExporting target states info to file \"" + prism.getExportTargetFilename() + "\"..."); PrismMTBDD.ExportLabels(labels, labelNames, "l", model.getAllDDRowVars(), model.getODD(), Prism.EXPORT_PLAIN, prism.getExportTargetFilename()); } catch (FileNotFoundException e) { - mainLog.println("\nWarning: Could not export target to file \"" + prism.getExportTargetFilename() + "\""); + mainLog.printWarning("Could not export target to file \"" + prism.getExportTargetFilename() + "\""); } } @@ -1202,13 +1202,13 @@ public class NondetModelChecker extends NonProbModelChecker if (prism.getCheckZeroLoops()) { // need to deal with zero loops yet if (min && zeroCostEndComponents != null && zeroCostEndComponents.size() > 0) { - mainLog.println("\nWarning: PRISM detected your model contains " + zeroCostEndComponents.size() + " zero-reward " - + ((zeroCostEndComponents.size() == 1) ? "loop." : "loops.")); - mainLog.println("Your minimum rewards may be too low..."); + mainLog.printWarning("PRISM detected your model contains " + zeroCostEndComponents.size() + " zero-reward " + + ((zeroCostEndComponents.size() == 1) ? "loop." : "loops.\n") + + "Your minimum rewards may be too low..."); } } else if (min) { - mainLog.println("\nWarning: PRISM hasn't checked for zero-reward loops."); - mainLog.println("Your minimum rewards may be too low..."); + mainLog.printWarning("PRISM hasn't checked for zero-reward loops.\n" + + "Your minimum rewards may be too low..."); } // print out yes/no/maybe diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index a27bbc52..2b25d5ed 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -205,7 +205,7 @@ public class Prism implements PrismSettingsListener } catch(PrismException ex) { - System.err.println("Warning: Failed to create new PRISM settings file."); + mainLog.printWarning("Failed to create new PRISM settings file."); } } // add this Prism object as a listener @@ -1260,17 +1260,17 @@ public class Prism implements PrismSettingsListener { // can only do ordered version of export for MDPs if (model.getModelType() == ModelType.MDP) { - if (!ordered) mainLog.println("\nWarning: Cannot export unordered transition matrix for MDPs; using ordered."); + if (!ordered) mainLog.printWarning("Cannot export unordered transition matrix for MDPs; using ordered."); ordered = true; } // can only do ordered version of export for MRMC if (exportType == EXPORT_MRMC) { - if (!ordered) mainLog.println("\nWarning: Cannot export unordered transition matrix in MRMC format; using ordered."); + if (!ordered) mainLog.printWarning("Cannot export unordered transition matrix in MRMC format; using ordered."); ordered = true; } // can only do ordered version of export for rows format if (exportType == EXPORT_ROWS) { - if (!ordered) mainLog.println("\nWarning: Cannot export unordered transition matrix in rows format; using ordered."); + if (!ordered) mainLog.printWarning("Cannot export unordered transition matrix in rows format; using ordered."); ordered = true; } @@ -1341,17 +1341,17 @@ public class Prism implements PrismSettingsListener // can only do ordered version of export for MDPs if (model.getModelType() == ModelType.MDP) { - if (!ordered) mainLog.println("\nWarning: 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.println("\nWarning: 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 if (exportType == EXPORT_ROWS) { - if (!ordered) mainLog.println("\nWarning: Cannot export unordered transition matrix in rows format; using ordered."); + if (!ordered) mainLog.printWarning("Cannot export unordered transition matrix in rows format; using ordered."); ordered = true; } diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 21e8704d..29dc3e66 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -521,7 +521,7 @@ public class PrismCL // even if a new log is created shortly mainLog = new PrismFileLog("stdout"); techLog = new PrismFileLog("stdout"); - + // create prism object(s) prism = new Prism(mainLog, techLog); prismExpl = new PrismExplicit(mainLog, prism.getSettings()); @@ -747,7 +747,7 @@ public class PrismCL } // if requested, remove them else if (fixdl) { - mainLog.print("\nWarning: " + 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...\n"); model.fixDeadlocks(); } // otherwise print error and bail out @@ -846,7 +846,7 @@ public class PrismCL } if (exportPlainDeprecated) - mainLog.println("\nWarning: The -exportplain switch is now deprecated. Please use -exporttrans in future."); + mainLog.printWarning("The -exportplain switch is now deprecated. Please use -exporttrans in future."); } // export state rewards to a file @@ -984,7 +984,7 @@ public class PrismCL prism.doSteadyState(model, exportType, exportSteadyStateFile); } } else { - mainLog.println("\nWarning: Steady-state probabilities only computed for DTMCs/CTMCs."); + mainLog.printWarning("Steady-state probabilities only computed for DTMCs/CTMCs."); } } @@ -1034,7 +1034,7 @@ public class PrismCL prism.doTransient(model, i, exportType, exportTransientFile, importinitdist ? new File(importInitDistFilename) : null); } } else { - mainLog.println("\nWarning: Transient probabilities only computed for DTMCs/CTMCs."); + mainLog.printWarning("Transient probabilities only computed for DTMCs/CTMCs."); } } @@ -1045,6 +1045,11 @@ public class PrismCL // clear up and close down prism.closeDown(true); mainLog.println(); + if (mainLog.getNumberOfWarnings() > 0) + { + mainLog.println("Note that " + mainLog.getNumberOfWarnings() + + " warning(s) were produced during computation"); + } } /** @@ -1796,7 +1801,7 @@ public class PrismCL aSimMethod = new CIconfidence(simWidth, simNumSamples); } if (simApproxGiven) { - mainLog.println("\nWarning: Option -simapprox is not used for the CI method and is being ignored"); + mainLog.printWarning("Option -simapprox is not used for the CI method and is being ignored"); } } // ACI @@ -1818,7 +1823,7 @@ public class PrismCL aSimMethod = new ACIconfidence(simWidth, simNumSamples); } if (simApproxGiven) { - mainLog.println("\nWarning: Option -simapprox is not used for the ACI method and is being ignored"); + mainLog.printWarning("Option -simapprox is not used for the ACI method and is being ignored"); } } // APMC @@ -1840,7 +1845,7 @@ public class PrismCL aSimMethod = new APMCconfidence(simApprox, simNumSamples); } if (simWidthGiven) { - mainLog.println("\nWarning: Option -simwidth is not used for the APMC method and is being ignored"); + mainLog.printWarning("Option -simwidth is not used for the APMC method and is being ignored"); } } // SPRT @@ -1850,10 +1855,10 @@ public class PrismCL } aSimMethod = new SPRTMethod(simConfidence, simConfidence, simWidth); if (simApproxGiven) { - mainLog.println("\nWarning: Option -simapprox is not used for the SPRT method and is being ignored"); + mainLog.printWarning("Option -simapprox is not used for the SPRT method and is being ignored"); } if (simNumSamplesGiven) { - mainLog.println("\nWarning: Option -simsamples is not used for the SPRT method and is being ignored"); + mainLog.printWarning("Option -simsamples is not used for the SPRT method and is being ignored"); } } else throw new PrismException("Unknown simulation method \"" + simMethodName + "\""); diff --git a/prism/src/prism/PrismLog.java b/prism/src/prism/PrismLog.java index 313e70b4..d7ccd7ba 100644 --- a/prism/src/prism/PrismLog.java +++ b/prism/src/prism/PrismLog.java @@ -43,6 +43,29 @@ public abstract class PrismLog 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. + */ + public void resetNumberOfWarnings() + { + this.numberOfWarnings = 0; + } + + /** + * Returns the number of warnings that have been printed since the beginning + * or since the last reset of number of warnings. + * @return + */ + public int getNumberOfWarnings() + { + return this.numberOfWarnings; + } + /** * Returns the verbosity level of this log. The verbosity level * determines what messages will be printed. @@ -330,6 +353,21 @@ 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. + *

+ * Also increases {@link #numberOfWarnings} by one. This variable can be then + * queried using {@link #getNumberOfWarnings()} at the end of computation + * and the user can be appropriately informed that there were warnings + * generated. + * @param s The warning message. + */ + 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 3192cb21..bc3ba0a4 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -171,12 +171,12 @@ public class ProbModelChecker extends NonProbModelChecker // Check for trivial (i.e. stupid) cases if (pb != null) { if ((p == 0 && relOp.equals(">=")) || (p == 1 && relOp.equals("<="))) { - mainLog.print("\nWarning: checking for probability " + relOp + " " + p + mainLog.printWarning("Checking for probability " + relOp + " " + p + " - formula trivially satisfies all states\n"); JDD.Ref(reach); return new StateValuesMTBDD(reach, model); } else if ((p == 0 && relOp.equals("<")) || (p == 1 && relOp.equals(">"))) { - mainLog.print("\nWarning: checking for probability " + relOp + " " + p + mainLog.printWarning("Checking for probability " + relOp + " " + p + " - formula trivially satisfies no states\n"); return new StateValuesMTBDD(JDD.Constant(0), model); } @@ -184,7 +184,7 @@ public class ProbModelChecker extends NonProbModelChecker // Print a warning if Pmin/Pmax used if (relOp.equals("min=") || relOp.equals("max=")) { - mainLog.print("\nWarning: \"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\n"); } // Compute probabilities @@ -258,12 +258,12 @@ public class ProbModelChecker extends NonProbModelChecker // check for trivial (i.e. stupid) cases if (rb != null) { if (r == 0 && relOp.equals(">=")) { - mainLog.print("\nWarning: checking for reward " + relOp + " " + r + mainLog.printWarning("Checking for reward " + relOp + " " + r + " - formula trivially satisfies all states\n"); JDD.Ref(reach); return new StateValuesMTBDD(reach, model); } else if (r == 0 && relOp.equals("<")) { - mainLog.print("\nWarning: checking for reward " + relOp + " " + r + mainLog.printWarning("Checking for reward " + relOp + " " + r + " - formula trivially satisfies no states\n"); return new StateValuesMTBDD(JDD.Constant(0), model); } @@ -271,7 +271,7 @@ public class ProbModelChecker extends NonProbModelChecker // print a warning if Rmin/Rmax used if (relOp.equals("min=") || relOp.equals("max=")) { - mainLog.print("\nWarning: \"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\n"); } // compute rewards @@ -347,12 +347,12 @@ public class ProbModelChecker extends NonProbModelChecker // check for trivial (i.e. stupid) cases if (pb != null) { if ((p == 0 && relOp.equals(">=")) || (p == 1 && relOp.equals("<="))) { - mainLog.print("\nWarning: checking for probability " + relOp + " " + p + mainLog.printWarning("Checking for probability " + relOp + " " + p + " - formula trivially satisfies all states\n"); JDD.Ref(reach); return new StateValuesMTBDD(reach, model); } else if ((p == 0 && relOp.equals("<")) || (p == 1 && relOp.equals(">"))) { - mainLog.print("\nWarning: checking for probability " + relOp + " " + p + mainLog.printWarning("Checking for probability " + relOp + " " + p + " - formula trivially satisfies no states\n"); return new StateValuesMTBDD(JDD.Constant(0), model); } @@ -798,7 +798,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.print("\nWarning: probability bound in formula is" + mainLog.printWarning("Probability bound in formula is" + " 0/1 so exact probabilities may not be computed\n"); probs = computeUntilProbsQual(trans01, b1, b2); } @@ -1489,7 +1489,7 @@ public class ProbModelChecker extends NonProbModelChecker mainLog.println("\nExporting target states info to file \"" + prism.getExportTargetFilename() + "\"..."); PrismMTBDD.ExportLabels(labels, labelNames, "l", model.getAllDDRowVars(), model.getODD(), Prism.EXPORT_PLAIN, prism.getExportTargetFilename()); } catch (FileNotFoundException e) { - mainLog.println("\nWarning: Could not export target to file \"" + prism.getExportTargetFilename() + "\""); + mainLog.printWarning("Could not export target to file \"" + prism.getExportTargetFilename() + "\""); } } diff --git a/prism/src/pta/ForwardsReach.java b/prism/src/pta/ForwardsReach.java index db34517a..cf7fa7cb 100644 --- a/prism/src/pta/ForwardsReach.java +++ b/prism/src/pta/ForwardsReach.java @@ -259,7 +259,7 @@ public class ForwardsReach // Print a warning if there are no target states if (target.cardinality() == 0) - mainLog.println("Warning: There are no target states."); + mainLog.printWarning("There are no target states."); return graph; } @@ -401,7 +401,7 @@ public class ForwardsReach // Print a warning if there are no target states if (target.cardinality() == 0) - mainLog.println("Warning: There are no target states."); + mainLog.printWarning("There are no target states."); return graph; } diff --git a/prism/src/simulator/GenerateSimulationPath.java b/prism/src/simulator/GenerateSimulationPath.java index 5a4999e2..f9d74c47 100644 --- a/prism/src/simulator/GenerateSimulationPath.java +++ b/prism/src/simulator/GenerateSimulationPath.java @@ -215,7 +215,7 @@ public class GenerateSimulationPath // display warning if attempt to use "repeat=" option and not "deadlock" option if (simPathRepeat > 1 && simPathType != PathType.SIM_PATH_DEADLOCK) { simPathRepeat = 1; - mainLog.println("\nWarning: Ignoring \"repeat\" option - it is only valid when looking for deadlocks."); + mainLog.printWarning("Ignoring \"repeat\" option - it is only valid when looking for deadlocks."); } // generate path @@ -262,7 +262,7 @@ public class GenerateSimulationPath // display warning if a deterministic loop was detected (but not in case where multiple paths generated) if (simLoopCheck && engine.isPathLooping() && simPathRepeat == 1) { - mainLog.println("\nWarning: Deterministic loop detected after " + i + mainLog.printWarning("Deterministic loop detected after " + i + " steps (use loopcheck=false option to extend path)."); } @@ -282,7 +282,7 @@ public class GenerateSimulationPath // warning if stopped early if (simPathType == PathType.SIM_PATH_TIME && t < simPathTime) { - mainLog.println("\nWarning: Path terminated before time " + simPathTime + " because maximum path length (" + mainLog.printWarning("Path terminated before time " + simPathTime + " because maximum path length (" + maxPathLength + ") reached."); } } diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index af1ceba0..cfcd6fca 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()) { - System.out.println("Warning: 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.print("\nWarning: Deadlocks were found during simulation: self-loops were added\n"); + mainLog.printWarning("Deadlocks were found during simulation: self-loops were added\n"); // Print a warning if simulation was stopped by the user if (shouldStopSampling) - mainLog.print("\nWarning: Simulation was terminated before completion.\n"); + mainLog.printWarning("Simulation was terminated before completion.\n"); // write to feedback file with true to indicate that we have finished sampling // Write_Feedback(iteration_counter, numIters, true);