Browse Source

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
master
Dave Parker 11 years ago
parent
commit
f699af97bc
  1. 7
      prism/src/param/ParamModelChecker.java
  2. 21
      prism/src/prism/Prism.java

7
prism/src/param/ParamModelChecker.java

@ -249,13 +249,6 @@ final public class ParamModelChecker extends PrismComponent
vals.clearExceptInit(); vals.clearExceptInit();
result.setResult(vals); 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 /* // Output plot to tex file
if (paramLower.length == 2) { if (paramLower.length == 2) {
try { try {

21
prism/src/prism/Prism.java

@ -2998,8 +2998,16 @@ public class Prism extends PrismComponent implements PrismSettingsListener
param.Function func = regVals.getResult(0).getInitStateValueAsFunction(); param.Function func = regVals.getResult(0).getInitStateValueAsFunction();
// Evaluate the function at an arbitrary point (should not depend on parameter values) // 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) })); BigRational rat = func.evaluate(new param.Point(new BigRational[] { new BigRational(0) }));
// Restore in result object
result.setResult(rat); 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; return result;
} }
@ -3044,7 +3052,16 @@ public class Prism extends PrismComponent implements PrismSettingsListener
mc.setModelBuilder(builder); mc.setModelBuilder(builder);
mc.setParameters(paramNames, paramLowerBounds, paramUpperBounds); mc.setParameters(paramNames, paramLowerBounds, paramUpperBounds);
mc.setModulesFileAndPropertiesFile(currentModulesFile, propertiesFile); 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;
} }
/** /**

Loading…
Cancel
Save