diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 3b2b292a..33bdf847 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/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"); }