From 2c51d84fcd78176c840315141418a89e9f46cbe9 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sat, 18 Apr 2020 17:15:18 +0100 Subject: [PATCH] Report accuracy for statistical model checking too. --- prism/src/prism/Accuracy.java | 50 +++++++++-- prism/src/prism/Prism.java | 13 +-- prism/src/prism/Result.java | 9 +- prism/src/simulator/SimulatorEngine.java | 82 +++++++------------ prism/src/simulator/method/ACIwidth.java | 11 +++ prism/src/simulator/method/APMCMethod.java | 18 ++++ prism/src/simulator/method/CIMethod.java | 19 +++++ prism/src/simulator/method/CIwidth.java | 11 +++ prism/src/simulator/method/SPRTMethod.java | 13 +++ .../simulator/method/SimulationMethod.java | 8 ++ 10 files changed, 160 insertions(+), 74 deletions(-) diff --git a/prism/src/prism/Accuracy.java b/prism/src/prism/Accuracy.java index 17172632..90df499d 100644 --- a/prism/src/prism/Accuracy.java +++ b/prism/src/prism/Accuracy.java @@ -65,7 +65,12 @@ public class Accuracy * The type of accuracy: absolute or relative. */ private AccuracyType type; - + + /** + * If appropriate, the probability with which the accuracy is guaranteed + */ + private double probability = 1.0; + /** * Create an accuracy of the specified level. * For "bounded" accuracies, {@link Accuracy.DEFAULT_ERROR_BOUND} is assumed. @@ -135,6 +140,15 @@ public class Accuracy this.errorBound = errorBound; } + /** + * Set the probability with which the accuracy is guaranteed + * (for the case where the level is {@link AccuracyLevel.PROBABLY_BOUNDED}). + */ + public void setProbability(double probability) + { + this.probability = probability; + } + /** * Set the accuracy type (absolute or relative). */ @@ -248,6 +262,15 @@ public class Accuracy return result + getAbsoluteErrorBound(result) + fpErrorBound; } + /** + * Get the probability with which the accuracy is guaranteed + * (for the case where the level is {@link AccuracyLevel.PROBABLY_BOUNDED}; otherwise 1.0). + */ + public double getProbability() + { + return level == AccuracyLevel.PROBABLY_BOUNDED ? probability : 1.0; + } + /** * Get a string representation of the accuracy. * The actual result needs to be passed in, in order to @@ -264,15 +287,24 @@ public class Accuracy case ESTIMATED_BOUNDED: case PROBABLY_BOUNDED: default: - double d = (Double) result; - String s = "+/- " + getAbsoluteErrorBound(d); - if (level == AccuracyLevel.ESTIMATED_BOUNDED) { - s += " estimated"; - } else if (level == AccuracyLevel.PROBABLY_BOUNDED) { - s += " probably"; + // Numerical results + if (result instanceof Double) { + double d = (Double) result; + String s = "+/- " + getAbsoluteErrorBound(d); + if (level == AccuracyLevel.ESTIMATED_BOUNDED) { + s += " estimated"; + } else if (level == AccuracyLevel.PROBABLY_BOUNDED) { + s += " with probability " + getProbability(); + } + return s + "; rel err " + getRelativeErrorBound(d); + } + // Non-numerical: only really makes sense for "probably" + else if (level == AccuracyLevel.PROBABLY_BOUNDED) { + return "with probability " + getProbability(); } - return s + "; rel err " + getRelativeErrorBound(d); } + // Default to empty: will be ignored + return ""; } @Override @@ -291,7 +323,7 @@ public class Accuracy if (level == AccuracyLevel.ESTIMATED_BOUNDED) { s += " estimated"; } else if (level == AccuracyLevel.PROBABLY_BOUNDED) { - s += " probably"; + s += " with probability " + getProbability(); } return s; } diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 67110de5..a3a4635f 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -3246,8 +3246,6 @@ public class Prism extends PrismComponent implements PrismSettingsListener public Result modelCheckSimulator(PropertiesFile propertiesFile, Expression expr, Values definedPFConstants, State initialState, long maxPathLength, SimulationMethod simMethod) throws PrismException { - Object res = null; - // Print info mainLog.printSeparator(); mainLog.println("\nSimulating: " + expr); @@ -3265,9 +3263,9 @@ public class Prism extends PrismComponent implements PrismSettingsListener // Do simulation loadModelIntoSimulator(); - res = getSimulator().modelCheckSingleProperty(propertiesFile, expr, initialState, maxPathLength, simMethod); + Result res = getSimulator().modelCheckSingleProperty(propertiesFile, expr, initialState, maxPathLength, simMethod); - return new Result(res); + return res; } /** @@ -3287,8 +3285,6 @@ public class Prism extends PrismComponent implements PrismSettingsListener public Result[] modelCheckSimulatorSimultaneously(PropertiesFile propertiesFile, List exprs, Values definedPFConstants, State initialState, long maxPathLength, SimulationMethod simMethod) throws PrismException { - Object[] res = null; - // Print info mainLog.printSeparator(); mainLog.print("\nSimulating"); @@ -3315,11 +3311,8 @@ public class Prism extends PrismComponent implements PrismSettingsListener // Do simulation loadModelIntoSimulator(); - res = getSimulator().modelCheckMultipleProperties(propertiesFile, exprs, initialState, maxPathLength, simMethod); + Result[] resArray = getSimulator().modelCheckMultipleProperties(propertiesFile, exprs, initialState, maxPathLength, simMethod); - Result[] resArray = new Result[res.length]; - for (int i = 0; i < res.length; i++) - resArray[i] = new Result(res[i]); return resArray; } diff --git a/prism/src/prism/Result.java b/prism/src/prism/Result.java index f2838ebf..19ab6c4c 100644 --- a/prism/src/prism/Result.java +++ b/prism/src/prism/Result.java @@ -188,10 +188,13 @@ public class Result public String getResultAndAccuracy() { if (accuracy != null) { - return result.toString() + " (" + accuracy.toString(result) + ")"; - } else { - return result.toString(); + String accuracyString = accuracy.toString(result); + if (accuracyString != null && !"".equals(accuracyString)) { + return result.toString() + " (" + accuracy.toString(result) + ")"; + } } + // If accuracy is missing or blank, omit it + return result.toString(); } /** diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index 4878d9ed..bdf65b9a 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -50,6 +50,7 @@ import prism.PrismLangException; import prism.PrismLog; import prism.PrismNotSupportedException; import prism.PrismUtils; +import prism.Result; import prism.ResultsCollection; import prism.RewardGenerator; import prism.UndefinedConstants; @@ -1527,19 +1528,19 @@ public class SimulatorEngine extends PrismComponent * @param maxPathLength The maximum path length for sampling * @param simMethod Object specifying details of method to use for simulation */ - public Object modelCheckSingleProperty(PropertiesFile propertiesFile, Expression expr, State initialState, long maxPathLength, + public Result modelCheckSingleProperty(PropertiesFile propertiesFile, Expression expr, State initialState, long maxPathLength, SimulationMethod simMethod) throws PrismException { ArrayList exprs; - Object res[]; + Result res[]; // Just do this via the 'multiple properties' method exprs = new ArrayList(); exprs.add(expr); res = modelCheckMultipleProperties(propertiesFile, exprs, initialState, maxPathLength, simMethod); - if (res[0] instanceof PrismException) - throw (PrismException) res[0]; + if (res[0].getResult() instanceof PrismException) + throw (PrismException) res[0].getResult(); else return res[0]; } @@ -1548,7 +1549,7 @@ public class SimulatorEngine extends PrismComponent * Perform statistical/approximate model checking of properties on the current model, using the simulator. * Sampling starts from the initial state provided or, if null, the default * initial state is used, selecting randomly (each time) if there are more than one. - * Returns an array of results, some of which may be Exception objects if there were errors. + * Returns an array of results, some of which may contain Exception objects if there were errors. * In the case of an error which affects all properties, an exception is thrown. * Note: All constants in the model/property files must have already been defined. * @param propertiesFile Properties file containing property to check, constants defined @@ -1557,7 +1558,7 @@ public class SimulatorEngine extends PrismComponent * @param maxPathLength The maximum path length for sampling * @param simMethod Object specifying details of method to use for simulation */ - public Object[] modelCheckMultipleProperties(PropertiesFile propertiesFile, List exprs, State initialState, + public Result[] modelCheckMultipleProperties(PropertiesFile propertiesFile, List exprs, State initialState, long maxPathLength, SimulationMethod simMethod) throws PrismException { // Create path to be used @@ -1573,7 +1574,7 @@ public class SimulatorEngine extends PrismComponent mainLog.println("Simulation parameters: max path length=" + maxPathLength); // Add the properties to the simulator (after a check that they are valid) - Object[] results = new Object[exprs.size()]; + Result[] results = new Result[exprs.size()]; int[] indices = new int[exprs.size()]; int validPropsCount = 0; for (int i = 0; i < exprs.size(); i++) { @@ -1595,7 +1596,7 @@ public class SimulatorEngine extends PrismComponent throw e; } } catch (PrismException e) { - results[i] = e; + results[i] = new Result(e); indices[i] = -1; } } @@ -1607,55 +1608,41 @@ public class SimulatorEngine extends PrismComponent // Process the results for (int i = 0; i < results.length; i++) { - // If there was an earlier error, nothing to do + // If there was no earlier error, extract result etc. if (indices[i] != -1) { Sampler sampler = propertySamplers.get(indices[i]); - //mainLog.print("Simulation results: mean: " + sampler.getMeanValue()); - //mainLog.println(", variance: " + sampler.getVariance()); SimulationMethod sm = sampler.getSimulationMethod(); // Compute/print any missing parameters that need to be done after simulation sm.computeMissingParameterAfterSim(); // Extract result from SimulationMethod and store try { - results[i] = sm.getResult(sampler); + results[i] = new Result(sm.getResult(sampler)); + results[i].setAccuracy(sampler.getSimulationMethod().getResultAccuracy(sampler)); } catch (PrismException e) { - results[i] = e; + results[i] = new Result(e); } } } - String resultNote = ""; + // Warning for nondeterministic models if (results.length > 0) { ModelType currentModelType = modelGen.getModelType(); if (currentModelType.nondeterministic() && currentModelType.removeNondeterminism() != currentModelType) { - resultNote += " (with nondeterminism in " + currentModelType.name() + " being resolved uniformly)"; + mainLog.println("Warning: Nondeterminism in " + currentModelType.name() + " was resolved uniformly"); } } + // Display results to log if (results.length == 1) { - mainLog.print("\nSimulation method parameters: "); - mainLog.println((indices[0] == -1) ? "no simulation" : propertySamplers.get(indices[0]).getSimulationMethod().getParametersString()); - mainLog.print("\nSimulation result details: "); - mainLog.println((indices[0] == -1) ? "no simulation" : propertySamplers.get(indices[0]).getSimulationMethodResultExplanation()); - if (!(results[0] instanceof PrismException)) - mainLog.println("\nResult: " + results[0] + resultNote); + if (!(results[0].getResult() instanceof PrismException)) + mainLog.println("\nResult: " + results[0].getResultAndAccuracy()); } else { - mainLog.println("\nSimulation method parameters:"); - for (int i = 0; i < results.length; i++) { - mainLog.print(exprs.get(i) + " : "); - mainLog.println((indices[i] == -1) ? "no simulation" : propertySamplers.get(indices[i]).getSimulationMethod().getParametersString()); - } - mainLog.println("\nSimulation result details:"); - for (int i = 0; i < results.length; i++) { - mainLog.print(exprs.get(i) + " : "); - mainLog.println((indices[i] == -1) ? "no simulation" : propertySamplers.get(indices[i]).getSimulationMethodResultExplanation()); - } mainLog.println("\nResults:"); for (int i = 0; i < results.length; i++) - mainLog.println(exprs.get(i) + " : " + results[i] + resultNote); + mainLog.println(exprs.get(i) + " : " + results[i].getResultAndAccuracy()); } - + return results; } @@ -1697,7 +1684,7 @@ public class SimulatorEngine extends PrismComponent // Add the properties to the simulator (after a check that they are valid) int n = undefinedConstants.getNumPropertyIterations(); Values definedPFConstants = new Values(); - Object[] results = new Object[n]; + Result[] results = new Result[n]; Values[] pfcs = new Values[n]; int[] indices = new int[n]; @@ -1726,7 +1713,7 @@ public class SimulatorEngine extends PrismComponent throw e; } } catch (PrismException e) { - results[i] = e; + results[i] = new Result(e); indices[i] = -1; } undefinedConstants.iterateProperty(); @@ -1739,38 +1726,29 @@ public class SimulatorEngine extends PrismComponent // Process the results for (int i = 0; i < n; i++) { - // If there was an earlier error, nothing to do + // If there was no earlier error, extract result etc. if (indices[i] != -1) { Sampler sampler = propertySamplers.get(indices[i]); - //mainLog.print("Simulation results: mean: " + sampler.getMeanValue()); - //mainLog.println(", variance: " + sampler.getVariance()); SimulationMethod sm = sampler.getSimulationMethod(); // Compute/print any missing parameters that need to be done after simulation sm.computeMissingParameterAfterSim(); // Extract result from SimulationMethod and store try { - results[i] = sm.getResult(sampler); + results[i] = new Result(sm.getResult(sampler)); + results[i].setAccuracy(sampler.getSimulationMethod().getResultAccuracy(sampler)); } catch (PrismException e) { - results[i] = e; + results[i] = new Result(e); } } // Store result in the ResultsCollection - resultsCollection.setResult(undefinedConstants.getMFConstantValues(), pfcs[i], results[i]); + resultsCollection.setResult(undefinedConstants.getMFConstantValues(), pfcs[i], results[i].getResult()); } // Display results to log - mainLog.println("\nSimulation method parameters:"); - for (int i = 0; i < results.length; i++) { - mainLog.print(pfcs[i] + " : "); - mainLog.println((indices[i] == -1) ? "no simulation" : propertySamplers.get(indices[i]).getSimulationMethod().getParametersString()); - } - mainLog.println("\nSimulation result details:"); - for (int i = 0; i < results.length; i++) { - mainLog.print(pfcs[i] + " : "); - mainLog.println((indices[i] == -1) ? "no simulation" : propertySamplers.get(indices[i]).getSimulationMethodResultExplanation()); - } mainLog.println("\nResults:"); - mainLog.print(resultsCollection.toStringPartial(undefinedConstants.getMFConstantValues(), true, " ", " : ", false)); + for (int i = 0; i < results.length; i++) + mainLog.println(pfcs[i] + " : " + results[i].getResultAndAccuracy()); + //mainLog.print(resultsCollection.toStringPartial(undefinedConstants.getMFConstantValues(), true, " ", " : ", false)); } /** diff --git a/prism/src/simulator/method/ACIwidth.java b/prism/src/simulator/method/ACIwidth.java index 0eb0d3c8..d65aa3fd 100644 --- a/prism/src/simulator/method/ACIwidth.java +++ b/prism/src/simulator/method/ACIwidth.java @@ -27,6 +27,7 @@ package simulator.method; +import prism.Accuracy; import prism.PrismException; import simulator.sampler.Sampler; import cern.jet.stat.Probability; @@ -111,6 +112,16 @@ public final class ACIwidth extends CIMethod return super.getResult(sampler); } + @Override + public Accuracy getResultAccuracy(Sampler sampler) throws PrismException + { + // We may use 'width' to compute the result, so compute if necessary + // (this should never happen) + if (!missingParameterComputed) + computeMissingParameterAfterSim(); + return super.getResultAccuracy(sampler); + } + @Override public String getResultExplanation(Sampler sampler) throws PrismException { diff --git a/prism/src/simulator/method/APMCMethod.java b/prism/src/simulator/method/APMCMethod.java index 1ec1a5c1..ce0125ac 100644 --- a/prism/src/simulator/method/APMCMethod.java +++ b/prism/src/simulator/method/APMCMethod.java @@ -31,7 +31,10 @@ import parser.ast.Expression; import parser.ast.ExpressionProb; import parser.ast.ExpressionReward; import parser.ast.RelOp; +import prism.Accuracy; import prism.PrismException; +import prism.Accuracy.AccuracyLevel; +import prism.Accuracy.AccuracyType; import simulator.sampler.Sampler; /** @@ -168,6 +171,21 @@ public abstract class APMCMethod extends SimulationMethod } } + @Override + public Accuracy getResultAccuracy(Sampler sampler){ + Accuracy accuracy; + // Quantitative + if (prOp == 0) { + accuracy = new Accuracy(AccuracyLevel.PROBABLY_BOUNDED, approximation, AccuracyType.ABSOLUTE); + } + // Bounded (accuracy error bound is meaningless) + else { + accuracy = new Accuracy(AccuracyLevel.PROBABLY_BOUNDED, 0.0, AccuracyType.ABSOLUTE); + } + accuracy.setProbability(1.0 - confidence); + return accuracy; + } + @Override public String getResultExplanation(Sampler sampler){ return "Pr(|ans - " + sampler.getMeanValue() + "| < " + approximation + ") > " + (1.0 - confidence); diff --git a/prism/src/simulator/method/CIMethod.java b/prism/src/simulator/method/CIMethod.java index af1e2968..50e3b057 100644 --- a/prism/src/simulator/method/CIMethod.java +++ b/prism/src/simulator/method/CIMethod.java @@ -31,7 +31,10 @@ import parser.ast.Expression; import parser.ast.ExpressionProb; import parser.ast.ExpressionReward; import parser.ast.RelOp; +import prism.Accuracy; import prism.PrismException; +import prism.Accuracy.AccuracyLevel; +import prism.Accuracy.AccuracyType; import simulator.sampler.Sampler; /** @@ -159,6 +162,22 @@ public abstract class CIMethod extends SimulationMethod } } + @Override + public Accuracy getResultAccuracy(Sampler sampler) throws PrismException + { + Accuracy accuracy; + // Quantitative + if (prOp == 0) { + accuracy = new Accuracy(AccuracyLevel.PROBABLY_BOUNDED, width, AccuracyType.ABSOLUTE); + } + // Bounded (accuracy error bound is meaningless) + else { + accuracy = new Accuracy(AccuracyLevel.PROBABLY_BOUNDED, 0.0, AccuracyType.ABSOLUTE); + } + accuracy.setProbability(1.0 - confidence); + return accuracy; + } + @Override public String getResultExplanation(Sampler sampler) throws PrismException { diff --git a/prism/src/simulator/method/CIwidth.java b/prism/src/simulator/method/CIwidth.java index 2994a432..226a52a7 100644 --- a/prism/src/simulator/method/CIwidth.java +++ b/prism/src/simulator/method/CIwidth.java @@ -27,6 +27,7 @@ package simulator.method; +import prism.Accuracy; import prism.PrismException; import simulator.sampler.Sampler; import cern.jet.stat.Probability; @@ -112,6 +113,16 @@ public final class CIwidth extends CIMethod return super.getResult(sampler); } + @Override + public Accuracy getResultAccuracy(Sampler sampler) throws PrismException + { + // We may use 'width' to compute the result, so compute if necessary + // (this should never happen) + if (!missingParameterComputed) + computeMissingParameterAfterSim(); + return super.getResultAccuracy(sampler); + } + @Override public String getResultExplanation(Sampler sampler) throws PrismException { diff --git a/prism/src/simulator/method/SPRTMethod.java b/prism/src/simulator/method/SPRTMethod.java index b3a3adbc..2594643c 100644 --- a/prism/src/simulator/method/SPRTMethod.java +++ b/prism/src/simulator/method/SPRTMethod.java @@ -31,7 +31,10 @@ import parser.ast.Expression; import parser.ast.ExpressionProb; import parser.ast.ExpressionReward; import parser.ast.RelOp; +import prism.Accuracy; import prism.PrismException; +import prism.Accuracy.AccuracyLevel; +import prism.Accuracy.AccuracyType; import simulator.sampler.Sampler; import simulator.sampler.SamplerDouble; @@ -229,6 +232,16 @@ public final class SPRTMethod extends SimulationMethod return new Boolean(h0true); } + @Override + public Accuracy getResultAccuracy(Sampler sampler) throws PrismException + { + // Boolean result so accuracy error bound is meaningless + Accuracy accuracy = new Accuracy(AccuracyLevel.PROBABLY_BOUNDED, 0.0, AccuracyType.ABSOLUTE); + // TODO: handle case where alpha != beta (not used in PRISM atm) + accuracy.setProbability(1.0 - alpha); + return accuracy; + } + @Override public String getResultExplanation(Sampler sampler){ return computedIterations + " samples needed to decide property " + h0true; diff --git a/prism/src/simulator/method/SimulationMethod.java b/prism/src/simulator/method/SimulationMethod.java index cc5f052b..f9f8385b 100644 --- a/prism/src/simulator/method/SimulationMethod.java +++ b/prism/src/simulator/method/SimulationMethod.java @@ -28,6 +28,7 @@ package simulator.method; import parser.ast.Expression; +import prism.Accuracy; import prism.PrismException; import simulator.sampler.Sampler; @@ -126,6 +127,13 @@ public abstract class SimulationMethod implements Cloneable */ public abstract Object getResult(Sampler sampler) throws PrismException; + /** + * Get the accuracy of the (approximate) result for the property that simulation is being used to approximate. + * @param sampler The Sampler object for this simulation + * @throws PrismException if we can't get a result for some reason. + */ + public abstract Accuracy getResultAccuracy(Sampler sampler) throws PrismException; + /** * Get an explanation for the result of the simulation as a string. * @param sampler The Sampler object for this simulation (e.g. to get mean)