Refactor explicit model checkers a bit, including changes to way min/max info is passed around (should generalise to games more nicely).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8643 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/explicit/CTMCModelChecker.java

@@ -53,10 +53,8 @@ public class CTMCModelChecker extends DTMCModelChecker
 	
 	// Model checking functions
 
-	/**
-	 * Model check a time-bounded until operator; return vector of probabilities for all states.
-	 */
-	protected StateValues checkProbBoundedUntil(Model model, ExpressionTemporal expr) throws PrismException
+	@Override
+	protected StateValues checkProbBoundedUntil(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException
 	{
 		double lTime, uTime; // time bounds
 		Expression exprTmp;

prism/src/explicit/CTMDPModelChecker.java

@@ -51,7 +51,8 @@ public class CTMDPModelChecker extends MDPModelChecker
 	
 	// Model checking functions
 
-	protected StateValues checkProbBoundedUntil(Model model, ExpressionTemporal expr, boolean min) throws PrismException
+	@Override
+	protected StateValues checkProbBoundedUntil(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException
 	{
 		double uTime;
 		BitSet b1, b2;
@@ -76,7 +77,7 @@ public class CTMDPModelChecker extends MDPModelChecker
 			// prob is 1 in b2 states, 0 otherwise
 			probs = StateValues.createFromBitSetAsDoubles(b2, model);
 		} else {
-			res = computeBoundedUntilProbs((CTMDP) model, b1, b2, uTime, min);
+			res = computeBoundedUntilProbs((CTMDP) model, b1, b2, uTime, minMax.isMin());
 			probs = StateValues.createFromDoubleArray(res.soln, model);
 		}
 

prism/src/explicit/DTMCModelChecker.java

@@ -34,7 +34,6 @@ import java.util.Vector;
 
 import parser.ast.Expression;
 import parser.ast.ExpressionTemporal;
-import parser.ast.ExpressionUnaryOp;
 import parser.type.TypeDouble;
 import prism.DRA;
 import prism.Pair;
@@ -58,74 +57,8 @@ public class DTMCModelChecker extends ProbModelChecker
 
 	// Model checking functions
 
-	/**
-	 * Compute probabilities for the contents of a P operator.
-	 */
-	protected StateValues checkProbPathFormula(Model model, Expression expr) throws PrismException
-	{
-		// Test whether this is a simple path formula (i.e. PCTL)
-		// and then pass control to appropriate method. 
-		if (expr.isSimplePathFormula()) {
-			return checkProbPathFormulaSimple(model, expr);
-		} else {
-			return checkProbPathFormulaLTL(model, expr, false);
-		}
-	}
-
-	/**
-	 * Compute probabilities for a simple, non-LTL path operator.
-	 */
-	protected StateValues checkProbPathFormulaSimple(Model model, Expression expr) throws PrismException
-	{
-		StateValues probs = null;
-
-		// Negation/parentheses
-		if (expr instanceof ExpressionUnaryOp) {
-			ExpressionUnaryOp exprUnary = (ExpressionUnaryOp) expr;
-			// Parentheses
-			if (exprUnary.getOperator() == ExpressionUnaryOp.PARENTH) {
-				// Recurse
-				probs = checkProbPathFormulaSimple(model, exprUnary.getOperand());
-			}
-			// Negation
-			else if (exprUnary.getOperator() == ExpressionUnaryOp.NOT) {
-				// Compute, then subtract from 1 
-				probs = checkProbPathFormulaSimple(model, exprUnary.getOperand());
-				probs.timesConstant(-1.0);
-				probs.plusConstant(1.0);
-			}
-		}
-		// Temporal operators
-		else if (expr instanceof ExpressionTemporal) {
-			ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
-			// Next
-			if (exprTemp.getOperator() == ExpressionTemporal.P_X) {
-				probs = checkProbNext(model, exprTemp);
-			}
-			// Until
-			else if (exprTemp.getOperator() == ExpressionTemporal.P_U) {
-				if (exprTemp.hasBounds()) {
-					probs = checkProbBoundedUntil(model, exprTemp);
-				} else {
-					probs = checkProbUntil(model, exprTemp);
-				}
-			}
-			// Anything else - convert to until and recurse
-			else {
-				probs = checkProbPathFormulaSimple(model, exprTemp.convertToUntilForm());
-			}
-		}
-
-		if (probs == null)
-			throw new PrismException("Unrecognised path operator in P operator");
-
-		return probs;
-	}
-
-	/**
-	 * Compute probabilities for a next operator.
-	 */
-	protected StateValues checkProbNext(Model model, ExpressionTemporal expr) throws PrismException
+	@Override
+	protected StateValues checkProbNext(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException
 	{
 		BitSet target = null;
 		ModelCheckerResult res = null;
@@ -137,10 +70,8 @@ public class DTMCModelChecker extends ProbModelChecker
 		return StateValues.createFromDoubleArray(res.soln, model);
 	}
 
-	/**
-	 * Compute probabilities for a bounded until operator.
-	 */
-	protected StateValues checkProbBoundedUntil(Model model, ExpressionTemporal expr) throws PrismException
+	@Override
+	protected StateValues checkProbBoundedUntil(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException
 	{
 		int time;
 		BitSet b1, b2;
@@ -174,10 +105,8 @@ public class DTMCModelChecker extends ProbModelChecker
 		return probs;
 	}
 
-	/**
-	 * Compute probabilities for an (unbounded) until operator.
-	 */
-	protected StateValues checkProbUntil(Model model, ExpressionTemporal expr) throws PrismException
+	@Override
+	protected StateValues checkProbUntil(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException
 	{
 		BitSet b1, b2;
 		StateValues probs = null;
@@ -199,10 +128,8 @@ public class DTMCModelChecker extends ProbModelChecker
 		return probs;
 	}
 
-	/**
-	 * Compute probabilities for an LTL path formula
-	 */
-	protected StateValues checkProbPathFormulaLTL(Model model, Expression expr, boolean qual) throws PrismException
+	@Override
+	protected StateValues checkProbPathFormulaLTL(Model model, Expression expr, boolean qual, MinMax minMax) throws PrismException
 	{
 		LTLModelChecker mcLtl;
 		StateValues probsProduct, probs;

prism/src/explicit/MDPModelChecker.java

@@ -34,7 +34,6 @@ import java.util.Vector;
 
 import parser.ast.Expression;
 import parser.ast.ExpressionTemporal;
-import parser.ast.ExpressionUnaryOp;
 import parser.type.TypeDouble;
 import prism.DRA;
 import prism.Pair;
@@ -64,74 +63,8 @@ public class MDPModelChecker extends ProbModelChecker
 	
 	// Model checking functions
 
-	/**
-	 * Compute probabilities for the contents of a P operator.
-	 */
-	protected StateValues checkProbPathFormula(NondetModel model, Expression expr, boolean min) throws PrismException
-	{
-		// Test whether this is a simple path formula (i.e. PCTL)
-		// and then pass control to appropriate method. 
-		if (expr.isSimplePathFormula()) {
-			return checkProbPathFormulaSimple(model, expr, min);
-		} else {
-			return checkProbPathFormulaLTL(model, expr, min);
-		}
-	}
-
-	/**
-	 * Compute probabilities for a simple, non-LTL path operator.
-	 */
-	protected StateValues checkProbPathFormulaSimple(NondetModel model, Expression expr, boolean min) throws PrismException
-	{
-		StateValues probs = null;
-
-		// Negation/parentheses
-		if (expr instanceof ExpressionUnaryOp) {
-			ExpressionUnaryOp exprUnary = (ExpressionUnaryOp) expr;
-			// Parentheses
-			if (exprUnary.getOperator() == ExpressionUnaryOp.PARENTH) {
-				// Recurse
-				probs = checkProbPathFormulaSimple(model, exprUnary.getOperand(), min);
-			}
-			// Negation
-			else if (exprUnary.getOperator() == ExpressionUnaryOp.NOT) {
-				// Compute, then subtract from 1 
-				probs = checkProbPathFormulaSimple(model, exprUnary.getOperand(), !min);
-				probs.timesConstant(-1.0);
-				probs.plusConstant(1.0);
-			}
-		}
-		// Temporal operators
-		else if (expr instanceof ExpressionTemporal) {
-			ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
-			// Next
-			if (exprTemp.getOperator() == ExpressionTemporal.P_X) {
-				probs = checkProbNext(model, exprTemp, min);
-			}
-			// Until
-			else if (exprTemp.getOperator() == ExpressionTemporal.P_U) {
-				if (exprTemp.hasBounds()) {
-					probs = checkProbBoundedUntil(model, exprTemp, min);
-				} else {
-					probs = checkProbUntil(model, exprTemp, min);
-				}
-			}
-			// Anything else - convert to until and recurse
-			else {
-				probs = checkProbPathFormulaSimple(model, exprTemp.convertToUntilForm(), min);
-			}
-		}
-
-		if (probs == null)
-			throw new PrismException("Unrecognised path operator in P operator");
-
-		return probs;
-	}
-
-	/**
-	 * Compute probabilities for a next operator.
-	 */
-	protected StateValues checkProbNext(NondetModel model, ExpressionTemporal expr, boolean min) throws PrismException
+	@Override
+	protected StateValues checkProbNext(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException
 	{
 		BitSet target = null;
 		ModelCheckerResult res = null;
@@ -139,14 +72,12 @@ public class MDPModelChecker extends ProbModelChecker
 		// Model check the operand
 		target = checkExpression(model, expr.getOperand2()).getBitSet();
 
-		res = computeNextProbs((MDP) model, target, min);
+		res = computeNextProbs((MDP) model, target, minMax.isMin());
 		return StateValues.createFromDoubleArray(res.soln, model);
 	}
 
-	/**
-	 * Compute probabilities for a bounded until operator.
-	 */
-	protected StateValues checkProbBoundedUntil(NondetModel model, ExpressionTemporal expr, boolean min) throws PrismException
+	@Override
+	protected StateValues checkProbBoundedUntil(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException
 	{
 		int time;
 		BitSet b1, b2;
@@ -179,17 +110,15 @@ public class MDPModelChecker extends ProbModelChecker
 			// prob is 1 in b2 states, 0 otherwise
 			probs = StateValues.createFromBitSetAsDoubles(b2, model);
 		} else {
-			res = computeBoundedUntilProbs((MDP) model, b1, b2, time, min);
+			res = computeBoundedUntilProbs((MDP) model, b1, b2, time, minMax.isMin());
 			probs = StateValues.createFromDoubleArray(res.soln, model);
 		}
 
 		return probs;
 	}
 
-	/**
-	 * Compute probabilities for an (unbounded) until operator.
-	 */
-	protected StateValues checkProbUntil(NondetModel model, ExpressionTemporal expr, boolean min) throws PrismException
+	@Override
+	protected StateValues checkProbUntil(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException
 	{
 		BitSet b1, b2;
 		StateValues probs = null;
@@ -205,17 +134,15 @@ public class MDPModelChecker extends ProbModelChecker
 		// mainLog.print(" states, b2 = " + JDD.GetNumMintermsString(b2,
 		// allDDRowVars.n()) + " states\n");
 
-		res = computeUntilProbs((MDP) model, b1, b2, min);
+		res = computeUntilProbs((MDP) model, b1, b2, minMax.isMin());
 		probs = StateValues.createFromDoubleArray(res.soln, model);
 		result.setStrategy(res.strat);
 
 		return probs;
 	}
 
-	/**
-	 * Compute probabilities for an LTL path formula
-	 */
-	protected StateValues checkProbPathFormulaLTL(NondetModel model, Expression expr, boolean min) throws PrismException
+	@Override
+	protected StateValues checkProbPathFormulaLTL(Model model, Expression expr, boolean qual, MinMax minMax) throws PrismException
 	{
 		LTLModelChecker mcLtl;
 		StateValues probsProduct, probs;
@@ -240,7 +167,7 @@ public class MDPModelChecker extends ProbModelChecker
 		// Convert LTL formula to deterministic Rabin automaton (DRA)
 		// For min probabilities, need to negate the formula
 		// (add parentheses to allow re-parsing if required)
-		if (min) {
+		if (minMax.isMin()) {
 			ltl = Expression.Not(Expression.Parenth(ltl));
 		}
 		mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")...");
@@ -268,7 +195,7 @@ public class MDPModelChecker extends ProbModelChecker
 		probsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachProbs((MDP) modelProduct, acceptingMECs, false).soln, modelProduct);
 
 		// Subtract from 1 if we're model checking a negated formula for regular Pmin
-		if (min) {
+		if (minMax.isMin()) {
 			probsProduct.timesConstant(-1.0);
 			probsProduct.plusConstant(1.0);
 		}

prism/src/explicit/MinMax.java

@@ -0,0 +1,78 @@
+//==============================================================================
+//	
+//	Copyright (c) 2014-
+//	Authors:
+//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/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 explicit;
+
+/**
+ * Class to store info about types of probabilities that are to be computed
+ * (typically how to quantify over strategies, e.g. "min" or "max"). 
+ */
+public class MinMax
+{
+	// Info about quantification over a single class of strategies/adversaries
+	
+	protected boolean min;
+	
+	public void setMin(boolean min)
+	{
+		this.min = min;
+	}
+	
+	public boolean isMin()
+	{
+		return min;
+	}
+	
+	public boolean isMax()
+	{
+		return !min;
+	}
+	
+	// Create a new instance by applying some operation
+	
+	public MinMax negate()
+	{
+		MinMax neg = new MinMax();
+		neg.setMin(!isMin());
+		return neg;
+	}
+	
+	// Utility methods to create instances of this class
+	
+	public static MinMax min()
+	{
+		MinMax minMax = new MinMax();
+		minMax.setMin(true);
+		return minMax;
+	}
+	
+	public static MinMax max()
+	{
+		MinMax minMax = new MinMax();
+		minMax.setMin(false);
+		return minMax;
+	}
+}

prism/src/explicit/ProbModelChecker.java

@@ -32,6 +32,8 @@ import parser.ast.Expression;
 import parser.ast.ExpressionProb;
 import parser.ast.ExpressionReward;
 import parser.ast.ExpressionSS;
+import parser.ast.ExpressionTemporal;
+import parser.ast.ExpressionUnaryOp;
 import parser.ast.RelOp;
 import parser.ast.RewardStruct;
 import prism.ModelType;
@@ -466,8 +468,6 @@ public class ProbModelChecker extends NonProbModelChecker
 		Expression pb; // Probability bound (expression)
 		double p = 0; // Probability bound (actual value)
 		RelOp relOp; // Relational operator
-		boolean min = false; // For nondeterministic models, are we finding min (true) or max (false) probs
-		ModelType modelType = model.getModelType();
 
 		StateValues probs = null;
 
@@ -479,29 +479,11 @@ public class ProbModelChecker extends NonProbModelChecker
 			if (p < 0 || p > 1)
 				throw new PrismException("Invalid probability bound " + p + " in P operator");
 		}
-		min = relOp.isLowerBound() || relOp.isMin();
 
 		// Compute probabilities
-		switch (modelType) {
-		case CTMC:
-			probs = ((CTMCModelChecker) this).checkProbPathFormula(model, expr.getExpression());
-			break;
-		case CTMDP:
-			probs = ((CTMDPModelChecker) this).checkProbPathFormula((NondetModel) model, expr.getExpression(), min);
-			break;
-		case DTMC:
-			probs = ((DTMCModelChecker) this).checkProbPathFormula(model, expr.getExpression());
-			break;
-		case MDP:
-			probs = ((MDPModelChecker) this).checkProbPathFormula((NondetModel) model, expr.getExpression(), min);
-			break;
-		/*case STPG:
-			probs = ((STPGModelChecker) this).checkProbPathFormula(model, expr.getExpression(), min);
-			break;*/
-		default:
-			throw new PrismException("Cannot model check " + expr + " for a " + modelType);
-		}
-
+		MinMax minMax = (relOp.isLowerBound() || relOp.isMin()) ? MinMax.min() : MinMax.max();
+		probs = checkProbPathFormula(model, expr.getExpression(), minMax);
+		
 		// Print out probabilities
 		if (getVerbosity() > 5) {
 			mainLog.print("\nProbabilities (non-zero only) for all states:\n");
@@ -520,6 +502,106 @@ public class ProbModelChecker extends NonProbModelChecker
 		}
 	}
 
+	/**
+	 * Compute probabilities for the contents of a P operator.
+	 */
+	protected StateValues checkProbPathFormula(Model model, Expression expr, MinMax minMax) throws PrismException
+	{
+		// Test whether this is a simple path formula (i.e. PCTL)
+		// and then pass control to appropriate method. 
+		if (expr.isSimplePathFormula()) {
+			return checkProbPathFormulaSimple(model, expr, minMax);
+		} else {
+			return checkProbPathFormulaLTL(model, expr, false, minMax);
+		}
+	}
+
+	/**
+	 * Compute probabilities for a simple, non-LTL path operator.
+	 */
+	protected StateValues checkProbPathFormulaSimple(Model model, Expression expr, MinMax minMax) throws PrismException
+	{
+		StateValues probs = null;
+
+		// Negation/parentheses
+		if (expr instanceof ExpressionUnaryOp) {
+			ExpressionUnaryOp exprUnary = (ExpressionUnaryOp) expr;
+			// Parentheses
+			if (exprUnary.getOperator() == ExpressionUnaryOp.PARENTH) {
+				// Recurse
+				probs = checkProbPathFormulaSimple(model, exprUnary.getOperand(), minMax);
+			}
+			// Negation
+			else if (exprUnary.getOperator() == ExpressionUnaryOp.NOT) {
+				// Compute, then subtract from 1 
+				probs = checkProbPathFormulaSimple(model, exprUnary.getOperand(), minMax.negate());
+				probs.timesConstant(-1.0);
+				probs.plusConstant(1.0);
+			}
+		}
+		// Temporal operators
+		else if (expr instanceof ExpressionTemporal) {
+			ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
+			// Next
+			if (exprTemp.getOperator() == ExpressionTemporal.P_X) {
+				probs = checkProbNext(model, exprTemp, minMax);
+			}
+			// Until
+			else if (exprTemp.getOperator() == ExpressionTemporal.P_U) {
+				if (exprTemp.hasBounds()) {
+					probs = checkProbBoundedUntil(model, exprTemp, minMax);
+				} else {
+					probs = checkProbUntil(model, exprTemp, minMax);
+				}
+			}
+			// Anything else - convert to until and recurse
+			else {
+				probs = checkProbPathFormulaSimple(model, exprTemp.convertToUntilForm(), minMax);
+			}
+		}
+
+		if (probs == null)
+			throw new PrismException("Unrecognised path operator in P operator");
+
+		return probs;
+	}
+
+	/**
+	 * Compute probabilities for a next operator.
+	 */
+	protected StateValues checkProbNext(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException
+	{
+		// To be overridden by subclasses
+		throw new PrismException("Computation not implemented yet");
+	}
+	
+	/**
+	 * Compute probabilities for a bounded until operator.
+	 */
+	protected StateValues checkProbBoundedUntil(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException
+	{
+		// To be overridden by subclasses
+		throw new PrismException("Computation not implemented yet");
+	}
+	
+	/**
+	 * Compute probabilities for an (unbounded) until operator.
+	 */
+	protected StateValues checkProbUntil(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException
+	{
+		// To be overridden by subclasses
+		throw new PrismException("Computation not implemented yet");
+	}
+	
+	/**
+	 * Compute probabilities for an LTL path formula
+	 */
+	protected StateValues checkProbPathFormulaLTL(Model model, Expression expr, boolean qual, MinMax minMax) throws PrismException
+	{
+		// To be overridden by subclasses
+		throw new PrismException("Computation not implemented yet");
+	}
+	
 	/**
 	 * Model check an R operator expression and return the values for all states.
 	 */