From 0a5e0b620372a217e6a816f749ecdeed6d06cba0 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 29 Aug 2014 22:39:32 +0000 Subject: [PATCH] Additional checks in explicit MDP model checker: don't allow policy iteration methods to be use when 'known' values are passed in (from Joachim Klein). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9157 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/MDPModelChecker.java | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index 4aef3652..9ae60d5c 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -208,7 +208,8 @@ public class MDPModelChecker extends ProbModelChecker * @param min Min or max probabilities (true=min, false=max) * @param init Optionally, an initial solution vector (may be overwritten) * @param known Optionally, a set of states for which the exact answer is known - * Note: if 'known' is specified (i.e. is non-null, 'init' must also be given and is used for the exact values. + * Note: if 'known' is specified (i.e. is non-null, 'init' must also be given and is used for the exact values). + * Also, 'known' values cannot be passed for some solution methods, e.g. policy iteration. */ public ModelCheckerResult computeReachProbs(MDP mdp, BitSet remain, BitSet target, boolean min, double init[], BitSet known) throws PrismException { @@ -233,6 +234,11 @@ public class MDPModelChecker extends ProbModelChecker if (!min) throw new PrismException("Value iteration from above only works for minimum probabilities"); } + if (mdpSolnMethod == MDPSolnMethod.POLICY_ITERATION || mdpSolnMethod == MDPSolnMethod.MODIFIED_POLICY_ITERATION) { + if (known != null) { + throw new PrismException("Policy iteration methods cannot be passed 'known' values for some states"); + } + } // Start probabilistic reachability timer = System.currentTimeMillis(); @@ -1127,7 +1133,8 @@ public class MDPModelChecker extends ProbModelChecker * @param min Min or max rewards (true=min, false=max) * @param init Optionally, an initial solution vector (may be overwritten) * @param known Optionally, a set of states for which the exact answer is known - * Note: if 'known' is specified (i.e. is non-null, 'init' must also be given and is used for the exact values. + * Note: if 'known' is specified (i.e. is non-null, 'init' must also be given and is used for the exact values). + * Also, 'known' values cannot be passed for some solution methods, e.g. policy iteration. */ public ModelCheckerResult computeReachRewards(MDP mdp, MDPRewards mdpRewards, BitSet target, boolean min, double init[], BitSet known) throws PrismException @@ -1146,6 +1153,13 @@ public class MDPModelChecker extends ProbModelChecker mainLog.printWarning("Switching to MDP solution method \"" + mdpSolnMethod.fullName() + "\""); } + // Check for some unsupported combinations + if (mdpSolnMethod == MDPSolnMethod.POLICY_ITERATION) { + if (known != null) { + throw new PrismException("Policy iteration methods cannot be passed 'known' values for some states"); + } + } + // Start expected reachability timer = System.currentTimeMillis(); mainLog.println("\nStarting expected reachability (" + (min ? "min" : "max") + ")...");