symbolic MDP checking: fairness for Rmax[ F ... ] not supported

Check and throw exception if fairness is requested for Rmax[F].

Rmin[F] and Rmax[C] computations are unaffected by PRISM's fairness.

prism/src/prism/NondetModelChecker.java

@@ -1423,6 +1423,12 @@ public class NondetModelChecker extends NonProbModelChecker
 		JDDNode b;
 		StateValues rewards = null;
 
+		if (fairness && !min) {
+			// Rmax with fairness not supported; Rmin computation is unaffected
+			JDD.Deref(statesOfInterest);
+			throw new PrismNotSupportedException("Maximum reward computation currently not supported under fairness.");
+		}
+
 		// currently, ignore statesOfInterest
 		JDD.Deref(statesOfInterest);
 
@@ -1467,6 +1473,12 @@ public class NondetModelChecker extends NonProbModelChecker
 		NondetModelChecker mcProduct;
 		long l;
 
+		if (fairness && !min) {
+			// Rmax with fairness not supported; Rmin computation is unaffected
+			JDD.Deref(statesOfInterest);
+			throw new PrismNotSupportedException("Maximum reward computation currently not supported under fairness.");
+		}
+
 		if (Expression.containsTemporalTimeBounds(expr)) {
 			if (model.getModelType().continuousTime()) {
 				JDD.Deref(statesOfInterest);
@@ -2185,6 +2197,8 @@ public class NondetModelChecker extends NonProbModelChecker
 		// Local copy of setting
 		int engine = this.engine;
 
+		// For Rmax[ C ] computation, fairness does not affect the result
+
 		if (doIntervalIteration) {
 			throw new PrismNotSupportedException("Interval iteration for total rewards is currently not supported");
 		}