code: //==============================================================================
  //	
  //	Copyright (c) 2002-
  //	Authors:
  //	* Vincent Nimal <vincent.nimal@comlab.ox.ac.uk> (University of Oxford)
  //	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
  //	
  //------------------------------------------------------------------------------
  //	
  //	This file is part of PRISM.
  //	
  //	PRISM is free software; you can redistribute it and/or modify
  //	it under the terms of the GNU General Public License as published by
  //	the Free Software Foundation; either version 2 of the License, or
  //	(at your option) any later version.
  //	
  //	PRISM is distributed in the hope that it will be useful,
  //	but WITHOUT ANY WARRANTY; without even the implied warranty of
  //	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  //	GNU General Public License for more details.
  //	
  //	You should have received a copy of the GNU General Public License
  //	along with PRISM; if not, write to the Free Software Foundation,
  //	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
  //	
  //==============================================================================
  
  package simulator.method;
  
  import parser.ast.Expression;
  import parser.ast.ExpressionProb;
  import parser.ast.ExpressionReward;
  import parser.ast.RelOp;
  import prism.PrismException;
  import simulator.sampler.Sampler;
  
  /**
   * SimulationMethod class(es) for the APMC ("approximate probabilistic model checking")
   * approach of Herault/Lassaigne/Magniette/Peyronnet (VMCAI'04).
   */
  public abstract class APMCMethod extends SimulationMethod
  {
  	// Has the missing parameter been computed yet?
  	protected boolean missingParameterComputed;
  	
  	// APMC parameters:
  	// Approximation (epsilon)
  	protected double approximation;
  	// Confidence (delta)
  	protected double confidence;
  	// Number of samples
  	protected int numSamples;
  
  	// Property info
  	// Operator in P/R: 0=quantitative, -1=lower bound, 1=upper bound
  	protected int prOp;
  	// Probability/reward bound (if any)
  	protected double theta;
  	
  	/**
  	 * Constructor: initialise but don't set any parameters.
  	 */
  	public APMCMethod()
  	{
  		missingParameterComputed = false;
  		approximation = 0.0;
  		confidence = 0.0;
  		numSamples = 0;
  	}
  
  	@Override
  	public String getName()
  	{
  		return "APMC";
  	}
  
  	@Override
  	public String getFullName()
  	{
  		return "Approximate Probabilistic Model Checking";
  	}
  
  	@Override
  	public void reset()
  	{
  		missingParameterComputed = false;
  	}
  
  	public abstract void computeMissingParameterBeforeSim() throws PrismException;
  	
  	@Override
  	public void setExpression(Expression expr) throws PrismException
  	{
  		Expression bound;
  		RelOp relOp;
  		
  		// For P properties...
  		if (expr instanceof ExpressionProb) {
  			bound = ((ExpressionProb) expr).getProb();
  			relOp = ((ExpressionProb) expr).getRelOp();
  		}
  		// For R properties...
  		else if (expr instanceof ExpressionReward) {
  			bound = ((ExpressionReward) expr).getReward();
  			relOp = ((ExpressionReward) expr).getRelOp();
  		}
  		// Other (error)
  		else {
  			throw new PrismException("Cannot approximate " + expr + " using simulation");
  		}
  
  		// Process bound/relop
  		if (bound == null) {
  			prOp = 0;
  			theta = -1.0; // junk
  		} else {
  			prOp = relOp.isLowerBound() ? -1 : 1;
  			theta = bound.evaluateDouble();
  		}
  	}
  	
  	@Override
  	public void computeMissingParameterAfterSim()
  	{
  		// Nothing to do (always computed before simulation)
  	}
  
  	public abstract Object getMissingParameter() throws PrismException;
  	
  	public abstract String getParametersString();
  	
  	@Override
  	public boolean shouldStopNow(int iters, Sampler sampler)
  	{
  		return iters >= numSamples;
  	}
  
  	@Override
  	public int getProgress(int iters, Sampler sampler)
  	{
  		// Easy: percentage of iters done so far
  		return ((10 * iters) / numSamples) * 10;
  	}
  
  	@Override
  	public Object getResult(Sampler sampler) throws PrismException
  	{
  		double estimate = sampler.getMeanValue();
  		switch (prOp) {
  		case 0: // 0=quantitative
  			return new Double(estimate);
  		case -1: // -1=lower bound
  			if (estimate >= theta + approximation)
  				return new Boolean(true);
  			else if (estimate <= theta - approximation)
  				return new Boolean(false);
  			else
  				throw new PrismException("Approximation is not precise enough to get a result");
  		case 1: // 1=upper bound
  			if (estimate >= theta + approximation)
  				return new Boolean(false);
  			else if (estimate <= theta - approximation)
  				return new Boolean(true);
  			else
  				throw new PrismException("Approximation is not precise enough to get a result");
  		default:
  			throw new PrismException("Unknown property type");
  		}
  	}
  	
  	@Override
  	public String getResultExplanation(Sampler sampler){
  		return "Pr(|ans - " + sampler.getMeanValue() + "| < " + approximation + ") > " + (1.0 - confidence);
  	}
  }
  