Support <<>> and [[]] operators for MDP (only * or empty), all engines.

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

prism/src/explicit/ProbModelChecker.java

@@ -43,7 +43,6 @@ import parser.type.TypeDouble;
 import parser.type.TypePathBool;
 import parser.type.TypePathDouble;
 import prism.IntegerBound;
-import prism.ModelType;
 import prism.OpRelOpBound;
 import prism.PrismComponent;
 import prism.PrismException;
@@ -468,8 +467,12 @@ public class ProbModelChecker extends NonProbModelChecker
 	{
 		StateValues res;
 
+		// <<>> or [[]] operator
+		if (expr instanceof ExpressionStrategy) {
+			res = checkExpressionStrategy(model, (ExpressionStrategy) expr, statesOfInterest);
+		}
 		// P operator
-		if (expr instanceof ExpressionProb) {
+		else if (expr instanceof ExpressionProb) {
 			res = checkExpressionProb(model, (ExpressionProb) expr, statesOfInterest);
 		}
 		// R operator
@@ -480,10 +483,6 @@ public class ProbModelChecker extends NonProbModelChecker
 		else if (expr instanceof ExpressionSS) {
 			res = checkExpressionSteadyState(model, (ExpressionSS) expr);
 		}
-		// <<>> operator
-		else if (expr instanceof ExpressionStrategy) {
-			res = checkExpressionStrategy(model, (ExpressionStrategy) expr, statesOfInterest);
-		}
 		// Otherwise, use the superclass
 		else {
 			res = super.checkExpression(model, expr, statesOfInterest);
@@ -498,28 +497,36 @@ public class ProbModelChecker extends NonProbModelChecker
 	 */
 	protected StateValues checkExpressionStrategy(Model model, ExpressionStrategy expr, BitSet statesOfInterest) throws PrismException
 	{
-		// Only support <<>> right now, not [[]]
-		if (!expr.isThereExists())
-			throw new PrismNotSupportedException("The " + expr.getOperatorString() + " operator is not yet supported");
-
-		// Only support <<>> for MDPs right now
+		// Only support <<>>/[[]] for MDPs right now
 		if (!(this instanceof MDPModelChecker))
 			throw new PrismNotSupportedException("The " + expr.getOperatorString() + " operator is only supported for MDPs currently");
 
+		// Will we be quantifying universally or existentially over strategies/adversaries?
+		boolean forAll = !expr.isThereExists();
+		
 		// Extract coalition info
 		Coalition coalition = expr.getCoalition();
-		// Strip any parentheses (they might have been needless wrapped around a single P or R)
+		// For non-games (i.e., models with a single player), deal with the coalition operator here and then remove it
+		if (coalition != null && !model.getModelType().multiplePlayers()) {
+			if (coalition.isEmpty()) {
+				// An empty coalition negates the quantification ("*" has no effect)
+				forAll = !forAll;
+			}
+			coalition = null;
+		}
+
+		// Strip any parentheses (they might have been needlessly wrapped around a single P or R)
 		Expression exprSub = expr.getExpression();
 		while (Expression.isParenth(exprSub))
 			exprSub = ((ExpressionUnaryOp) exprSub).getOperand();
 		// Pass onto relevant method:
 		// P operator
 		if (exprSub instanceof ExpressionProb) {
-			return checkExpressionProb(model, (ExpressionProb) exprSub, false, coalition, statesOfInterest);
+			return checkExpressionProb(model, (ExpressionProb) exprSub, forAll, coalition, statesOfInterest);
 		}
 		// R operator
 		else if (exprSub instanceof ExpressionReward) {
-			return checkExpressionReward(model, (ExpressionReward) exprSub, false, coalition, statesOfInterest);
+			return checkExpressionReward(model, (ExpressionReward) exprSub, forAll, coalition, statesOfInterest);
 		}
 		// Anything else is an error 
 		else {
@@ -550,16 +557,8 @@ public class ProbModelChecker extends NonProbModelChecker
 	{
 		// Get info from P operator
 		OpRelOpBound opInfo = expr.getRelopBoundInfo(constantValues);
-		MinMax minMax = opInfo.getMinMax(model.getModelType());
+		MinMax minMax = opInfo.getMinMax(model.getModelType(), forAll);
 
-		// Deal with coalition operator, if present (just MDPs, currently)
-		if (coalition != null && model.getModelType() == ModelType.MDP) {
-			if (coalition.isEmpty()) {
-				// An empty coalition negates the min/max ("*" has no effect)
-				minMax = minMax.negate();
-			}
-		}
-		
 		// Compute probabilities
 		StateValues probs = checkProbPathFormula(model, expr.getExpression(), minMax, statesOfInterest);
 
@@ -827,10 +826,12 @@ public class ProbModelChecker extends NonProbModelChecker
 	}
 
 	/**
-	 * Model check a P operator expression and return the values for all states.
+	 * Model check an R operator expression and return the values for all states.
 	 */
 	protected StateValues checkExpressionReward(Model model, ExpressionReward expr, BitSet statesOfInterest) throws PrismException
 	{
+		// Use the default semantics for a standalone R operator
+		// (i.e. quantification over all strategies, and no game-coalition info)
 		return checkExpressionReward(model, expr, true, null, statesOfInterest);
 	}
 	
@@ -841,7 +842,7 @@ public class ProbModelChecker extends NonProbModelChecker
 	{
 		// Get info from R operator
 		OpRelOpBound opInfo = expr.getRelopBoundInfo(constantValues);
-		MinMax minMax = opInfo.getMinMax(model.getModelType());
+		MinMax minMax = opInfo.getMinMax(model.getModelType(), forAll);
 
 		// Build rewards
 		RewardStruct rewStruct = expr.getRewardStructByIndexObject(modulesFile, constantValues);

prism/src/prism/NondetModelChecker.java

@@ -43,11 +43,13 @@ import jdd.JDDNode;
 import jdd.JDDVars;
 import mtbdd.PrismMTBDD;
 import odd.ODDUtils;
+import parser.ast.Coalition;
 import parser.ast.Expression;
 import parser.ast.ExpressionFunc;
 import parser.ast.ExpressionProb;
 import parser.ast.ExpressionQuant;
 import parser.ast.ExpressionReward;
+import parser.ast.ExpressionStrategy;
 import parser.ast.ExpressionTemporal;
 import parser.ast.ExpressionUnaryOp;
 import parser.ast.PropertiesFile;
@@ -142,8 +144,12 @@ public class NondetModelChecker extends NonProbModelChecker
 	{
 		StateValues res;
 
+		// <<>> or [[]] operator
+		if (expr instanceof ExpressionStrategy) {
+			res = checkExpressionStrategy((ExpressionStrategy) expr);
+		}
 		// P operator
-		if (expr instanceof ExpressionProb) {
+		else if (expr instanceof ExpressionProb) {
 			res = checkExpressionProb((ExpressionProb) expr);
 		}
 		// R operator
@@ -174,14 +180,64 @@ public class NondetModelChecker extends NonProbModelChecker
 		return res;
 	}
 
+	/**
+	 * Model check a <<>> or [[]] operator expression and return the values for all states.
+	 */
+	protected StateValues checkExpressionStrategy(ExpressionStrategy expr) throws PrismException
+	{
+		// Will we be quantifying universally or existentially over strategies/adversaries?
+		boolean forAll = !expr.isThereExists();
+		
+		// Extract coalition info
+		Coalition coalition = expr.getCoalition();
+		// Deal with the coalition operator here and then remove it
+		if (coalition != null) {
+			if (coalition.isEmpty()) {
+				// An empty coalition negates the quantification ("*" has no effect)
+				forAll = !forAll;
+			}
+			coalition = null;
+		}
+
+		// Strip any parentheses (they might have been needlessly wrapped around a single P or R)
+		Expression exprSub = expr.getExpression();
+		while (Expression.isParenth(exprSub))
+			exprSub = ((ExpressionUnaryOp) exprSub).getOperand();
+		// Pass onto relevant method:
+		// P operator
+		if (exprSub instanceof ExpressionProb) {
+			return checkExpressionProb((ExpressionProb) exprSub, forAll);
+		}
+		// R operator
+		else if (exprSub instanceof ExpressionReward) {
+			return checkExpressionReward((ExpressionReward) exprSub, forAll);
+		}
+		// Anything else is an error 
+		else {
+			throw new PrismException("Unexpected operators in " + expr.getOperatorString() + " operator");
+		}
+	}
+	
 	/**
 	 * Model check a P operator expression and return the values for all states.
 	 */
 	protected StateValues checkExpressionProb(ExpressionProb expr) throws PrismException
+	{
+		// Use the default semantics for a standalone P operator
+		// (i.e. quantification over all strategies)
+		return checkExpressionProb(expr, true);
+	}
+	
+	/**
+	 * Model check a P operator expression and return the values for all states.
+	 * @param expr The P operator expression
+	 * @param forAll Are we checking "for all strategies" (true) or "there exists a strategy" (false)? [irrelevant for numerical (=?) queries] 
+	 */
+	protected StateValues checkExpressionProb(ExpressionProb expr, boolean forAll) throws PrismException
 	{
 		// Get info from P operator
 		OpRelOpBound opInfo = expr.getRelopBoundInfo(constantValues);
-		MinMax minMax = opInfo.getMinMax(model.getModelType());
+		MinMax minMax = opInfo.getMinMax(model.getModelType(), forAll);
 		
 		// Check for trivial (i.e. stupid) cases
 		if (opInfo.isTriviallyTrue()) {
@@ -220,13 +276,25 @@ public class NondetModelChecker extends NonProbModelChecker
 	}
 
 	/**
-	 * Model check an R operator expression and return the values for all states.
+	 * Model check n R operator expression and return the values for all states.
 	 */
 	protected StateValues checkExpressionReward(ExpressionReward expr) throws PrismException
+	{
+		// Use the default semantics for a standalone R operator
+		// (i.e. quantification over all strategies)
+		return checkExpressionReward(expr, true);
+	}
+	
+	/**
+	 * Model check an R operator expression and return the values for all states.
+	 * @param expr The R operator expression
+	 * @param forAll Are we checking "for all strategies" (true) or "there exists a strategy" (false)? [irrelevant for numerical (=?) queries] 
+	 */
+	protected StateValues checkExpressionReward(ExpressionReward expr, boolean forAll) throws PrismException
 	{
 		// Get info from R operator
 		OpRelOpBound opInfo = expr.getRelopBoundInfo(constantValues);
-		MinMax minMax = opInfo.getMinMax(model.getModelType());
+		MinMax minMax = opInfo.getMinMax(model.getModelType(), forAll);
 
 		// Get rewards
 		Object rs = expr.getRewardStructIndex();

prism/src/prism/OpRelOpBound.java

@@ -79,16 +79,28 @@ public class OpRelOpBound
 	}
 
 	public MinMax getMinMax(ModelType modelType) throws PrismException
+	{
+		return getMinMax(modelType, true);
+	}
+
+	public MinMax getMinMax(ModelType modelType, boolean forAll) throws PrismException
 	{
 		MinMax minMax = MinMax.blank();
 		if (modelType.nondeterministic()) {
-			if (relOp == RelOp.EQ && isNumeric()) {
-				throw new PrismException("Can't use \"" + op + "=?\" for nondeterministic models; use e.g. \"" + op + "min=?\" or \"" + op + "max=?\"");
+			if (!(modelType == ModelType.MDP || modelType == ModelType.CTMDP)) {
+				throw new PrismException("Don't know how to model check " + getTypeOfOperator() + " properties for " + modelType + "s");
 			}
-			if (modelType == ModelType.MDP || modelType == ModelType.CTMDP) {
-				minMax = (relOp.isLowerBound() || relOp.isMin()) ? MinMax.min() : MinMax.max();
+			if (isNumeric()) {
+				if (relOp == RelOp.EQ) {
+					throw new PrismException("Can't use \"" + op + "=?\" for nondeterministic models; use e.g. \"" + op + "min=?\" or \"" + op + "max=?\"");
+				}
+				minMax = relOp.isMin() ? MinMax.min() : MinMax.max();
 			} else {
-				throw new PrismException("Don't know how to model check " + getTypeOfOperator() + " properties for " + modelType + "s");
+				if (forAll) {
+					minMax = (relOp.isLowerBound() ) ? MinMax.min() : MinMax.max();
+				} else {
+					minMax = (relOp.isLowerBound() ) ? MinMax.max() : MinMax.min();
+				}
 			}
 		}
 		return minMax;