From b888840a8a277e538c8d5f16f864b29048e9e5e5 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Mon, 28 Aug 2017 12:45:46 +0200 Subject: [PATCH] Multi objective checking: fairness unsupported Check and throw exception if fairness is requested for multi-objective analysis --- prism/src/prism/NondetModelChecker.java | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 33bdf847..d983aae7 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -381,6 +381,11 @@ public class NondetModelChecker extends NonProbModelChecker */ protected StateValues checkExpressionMultiObjective(List exprs, boolean forAll, JDDNode statesOfInterest) throws PrismException { + if (fairness) { + JDD.Deref(statesOfInterest); + throw new PrismNotSupportedException("Multi-objective reasoning under fairness currently not supported"); + } + // For now, just support a single expression (which may encode a Boolean combination of objectives) if (exprs.size() > 1) { JDD.Deref(statesOfInterest); @@ -489,7 +494,13 @@ public class NondetModelChecker extends NonProbModelChecker boolean hasMaxReward = false; //boolean hasLTLconstraint = false; + if (fairness) { + JDD.Deref(statesOfInterest); + throw new PrismNotSupportedException("Multi-objective reasoning under fairness currently not supported"); + } + if (doIntervalIteration) { + JDD.Deref(statesOfInterest); throw new PrismNotSupportedException("Interval iteration currently not supported for multi-objective reasoning"); }