diff --git a/prism/src/param/ModelBuilder.java b/prism/src/param/ModelBuilder.java index 98c4026c..1b67a5e4 100644 --- a/prism/src/param/ModelBuilder.java +++ b/prism/src/param/ModelBuilder.java @@ -382,6 +382,8 @@ public final class ModelBuilder extends PrismComponent } model.setFunctionFactory(functionFactory); + mainLog.println(); + mainLog.print("Reachable states exploration and model construction"); mainLog.println(" done in " + ((System.currentTimeMillis() - timer) / 1000.0) + " secs."); diff --git a/prism/src/param/ParamModelChecker.java b/prism/src/param/ParamModelChecker.java index c23a43f3..7394eed4 100644 --- a/prism/src/param/ParamModelChecker.java +++ b/prism/src/param/ParamModelChecker.java @@ -265,10 +265,20 @@ final public class ParamModelChecker extends PrismComponent RegionValues vals = checkExpression(paramModel, expr, needStates); timer = System.currentTimeMillis() - timer; mainLog.println("\nTime for model checking: " + timer / 1000.0 + " seconds."); + + // Store result result = new Result(); vals.clearExceptInit(); result.setResult(vals); - mainLog.println(result); + + // Print result to log + String resultString = "Result"; + if (!("Result".equals(expr.getResultName()))) + resultString += " (" + expr.getResultName().toLowerCase() + ")"; + resultString += ": " + result.getResultString(); + mainLog.print("\n" + resultString); + + /* // Output plot to tex file if (paramLower.length == 2) { try { FileOutputStream file = new FileOutputStream("out.tex"); @@ -281,7 +291,7 @@ final public class ParamModelChecker extends PrismComponent } catch (Exception e) { throw new PrismException("file could not be written"); } - } + }*/ return result; } diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 633865cb..a565f61f 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -2887,10 +2887,21 @@ public class Prism extends PrismComponent implements PrismSettingsListener if (paramNames == null) { throw new PrismException("Must specify some parameters when using " + "the parametric analysis"); } + + Values definedPFConstants = propertiesFile.getConstantValues(); Values constlist = currentModulesFile.getConstantValues(); for (int pnr = 0; pnr < paramNames.length; pnr++) { constlist.removeValue(paramNames[pnr]); } + + // Print info + mainLog.printSeparator(); + mainLog.println("\nParametric model checking: " + prop); + if (currentDefinedMFConstants != null && currentDefinedMFConstants.getNumValues() > 0) + mainLog.println("Model constants: " + currentDefinedMFConstants); + if (definedPFConstants != null && definedPFConstants.getNumValues() > 0) + mainLog.println("Property constants: " + definedPFConstants); + param.ModelBuilder builder = new ModelBuilder(this); builder.setModulesFile(currentModulesFile); builder.setParameters(paramNames, paramLowerBounds, paramUpperBounds);