Report accuracy for statistical model checking too.

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;
 		}

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<Expression> 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;
 	}
 

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();
 	}
 	
 	/**

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<Expression> exprs;
-		Object res[];
+		Result res[];
 
 		// Just do this via the 'multiple properties' method
 		exprs = new ArrayList<Expression>();
 		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<Expression> exprs, State initialState,
+	public Result[] modelCheckMultipleProperties(PropertiesFile propertiesFile, List<Expression> 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));
 	}
 
 	/**

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
 	{

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);

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
 	{

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
 	{

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;

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)