From f699af97bcaaed588ed26113992bee8d94bdf75c Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sun, 7 Dec 2014 01:45:28 +0000 Subject: [PATCH] Move printout of result for parametric result to allow reuse in exact model checking. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9387 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/param/ParamModelChecker.java | 7 ------- prism/src/prism/Prism.java | 21 +++++++++++++++++++-- 2 files changed, 19 insertions(+), 9 deletions(-) diff --git a/prism/src/param/ParamModelChecker.java b/prism/src/param/ParamModelChecker.java index 2b1d85f5..1e0945f0 100644 --- a/prism/src/param/ParamModelChecker.java +++ b/prism/src/param/ParamModelChecker.java @@ -249,13 +249,6 @@ final public class ParamModelChecker extends PrismComponent vals.clearExceptInit(); result.setResult(vals); - // 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 { diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 49b09d52..ef30b695 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -2998,8 +2998,16 @@ public class Prism extends PrismComponent implements PrismSettingsListener param.Function func = regVals.getResult(0).getInitStateValueAsFunction(); // Evaluate the function at an arbitrary point (should not depend on parameter values) BigRational rat = func.evaluate(new param.Point(new BigRational[] { new BigRational(0) })); - + // Restore in result object result.setResult(rat); + + // Print result to log + String resultString = "Result"; + if (!("Result".equals(prop.getExpression().getResultName()))) + resultString += " (" + prop.getExpression().getResultName().toLowerCase() + ")"; + resultString += ": " + result.getResultString(); + mainLog.print("\n" + resultString); + return result; } @@ -3044,7 +3052,16 @@ public class Prism extends PrismComponent implements PrismSettingsListener mc.setModelBuilder(builder); mc.setParameters(paramNames, paramLowerBounds, paramUpperBounds); mc.setModulesFileAndPropertiesFile(currentModulesFile, propertiesFile); - return mc.check(modelExpl, prop.getExpression()); + Result result = mc.check(modelExpl, prop.getExpression()); + + // Print result to log + String resultString = "Result"; + if (!("Result".equals(prop.getExpression().getResultName()))) + resultString += " (" + prop.getExpression().getResultName().toLowerCase() + ")"; + resultString += ": " + result.getResultString(); + mainLog.print("\n" + resultString); + + return result; } /**