From 6afda907f6939dba8486c57b94b2dd17d4b39457 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Mon, 27 Jul 2015 07:15:55 +0000
Subject: [PATCH] Check <<>> operator for MDPs in explicit engine.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10420 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/explicit/ProbModelChecker.java | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java
index 18114f17..91ed563e 100644
--- a/prism/src/explicit/ProbModelChecker.java
+++ b/prism/src/explicit/ProbModelChecker.java
@@ -43,6 +43,7 @@ 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;
@@ -551,6 +552,14 @@ public class ProbModelChecker extends NonProbModelChecker
 		OpRelOpBound opInfo = expr.getRelopBoundInfo(constantValues);
 		MinMax minMax = opInfo.getMinMax(model.getModelType());
 
+		// 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);