From a9dce99e48e57ef9c94a56e55b93ad4d4254583b Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Mon, 28 Aug 2017 12:45:46 +0200 Subject: [PATCH] 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 | 14 ++++++++++++++ 1 file changed, 14 insertions(+) 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"); }