From 3f56c6668fd07f87968bdf9cb82783a7271be81a Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 10 Jun 2013 13:10:02 +0000 Subject: [PATCH] Miscellaneous code changes/tidies - trying to align with prism-games a bit. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6881 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/MDP.java | 21 +++++++------- prism/src/explicit/MDPModelChecker.java | 37 +++++++++++++------------ 2 files changed, 31 insertions(+), 27 deletions(-) diff --git a/prism/src/explicit/MDP.java b/prism/src/explicit/MDP.java index b9b31fb5..521853e7 100644 --- a/prism/src/explicit/MDP.java +++ b/prism/src/explicit/MDP.java @@ -26,12 +26,13 @@ package explicit; -import java.util.*; +import java.util.BitSet; +import java.util.Iterator; +import java.util.List; import java.util.Map.Entry; import prism.PrismException; - -import explicit.rewards.*; +import explicit.rewards.MDPRewards; /** * Interface for classes that provide (read) access to an explicit-state MDP. @@ -42,12 +43,12 @@ public interface MDP extends Model * Get the total number of choices (distributions) over all states. */ public int getNumChoices(); - + /** * Get the maximum number of choices (distributions) in any state. */ public int getMaxNumChoices(); - + /** * Get the action label (if any) for choice {@code i} of state {@code s}. */ @@ -61,7 +62,7 @@ public interface MDP extends Model /** * Get an iterator over the transitions from choice {@code i} of state {@code s}. */ - public Iterator> getTransitionsIterator(int s, int i); + public Iterator> getTransitionsIterator(int s, int i); /** * Perform a single step of precomputation algorithm Prob0, i.e., for states i in {@code subset}, @@ -74,7 +75,7 @@ public interface MDP extends Model * @param result Store results here */ public void prob0step(BitSet subset, BitSet u, boolean forall, BitSet result); - + /** * Perform a single step of precomputation algorithm Prob1, i.e., for states i in {@code subset}, * set bit i of {@code result} iff, for all/some choices, @@ -87,7 +88,7 @@ public interface MDP extends Model * @param result Store results here */ public void prob1step(BitSet subset, BitSet u, BitSet v, boolean forall, BitSet result); - + /** * Do a matrix-vector multiplication followed by min/max, i.e. one step of value iteration, * i.e. for all s: result[s] = min/max_k { sum_j P_k(s,j)*vect[j] } @@ -128,7 +129,7 @@ public interface MDP extends Model * @param vect Vector to multiply by */ public double mvMultSingle(int s, int k, double vect[]); - + /** * Do a Gauss-Seidel-style matrix-vector multiplication followed by min/max. * i.e. for all s: vect[s] = min/max_k { (sum_{j!=s} P_k(s,j)*vect[j]) / P_k(s,s) } @@ -190,7 +191,7 @@ public interface MDP extends Model * @return The maximum difference between old/new elements of {@code vect} */ public double mvMultRewGSMinMax(double vect[], MDPRewards mdpRewards, boolean min, BitSet subset, boolean complement, boolean absolute); - + /** * Do a single row of matrix-vector multiplication and sum of action reward followed by min/max. * i.e. return min/max_k { rew(s) + sum_j P_k(s,j)*vect[j] } diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index 1546094e..3cdef30a 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -126,7 +126,7 @@ public class MDPModelChecker extends ProbModelChecker res = computeNextProbs((MDP) model, target, min); return StateValues.createFromDoubleArray(res.soln, model); } - + /** * Compute probabilities for a bounded until operator. */ @@ -201,7 +201,7 @@ public class MDPModelChecker extends ProbModelChecker protected StateValues checkRewardFormula(Model model, MDPRewards modelRewards, Expression expr, boolean min) throws PrismException { StateValues rewards = null; - + if (expr instanceof ExpressionTemporal) { ExpressionTemporal exprTemp = (ExpressionTemporal) expr; switch (exprTemp.getOperator()) { @@ -212,7 +212,7 @@ public class MDPModelChecker extends ProbModelChecker throw new PrismException("Explicit engine does not yet handle the " + exprTemp.getOperatorSymbol() + " operator in the R operator"); } } - + if (rewards == null) throw new PrismException("Unrecognised operator in R operator"); @@ -258,7 +258,7 @@ public class MDPModelChecker extends ProbModelChecker long timer; timer = System.currentTimeMillis(); - + // Store num states n = mdp.getNumStates(); @@ -330,12 +330,12 @@ public class MDPModelChecker extends ProbModelChecker mdpSolnMethod = MDPSolnMethod.GAUSS_SEIDEL; mainLog.printWarning("Switching to MDP solution method \"" + mdpSolnMethod.fullName() + "\""); } - + // Check for some unsupported combinations if (mdpSolnMethod == MDPSolnMethod.VALUE_ITERATION && valIterDir == ValIterDir.ABOVE) { - if (!(precomp && prob0)) + if (!(precomp && prob0)) throw new PrismException("Precomputation (Prob0) must be enabled for value iteration from above"); - if (!min) + if (!min) throw new PrismException("Value iteration from above only works for minimum probabilities"); } @@ -651,7 +651,7 @@ public class MDPModelChecker extends ProbModelChecker msg += "\nConsider using a different numerical method or increasing the maximum number of iterations"; throw new PrismException(msg); } - + // Process adversary if (genAdv) { // Prune adversary @@ -749,7 +749,7 @@ public class MDPModelChecker extends ProbModelChecker msg += "\nConsider using a different numerical method or increasing the maximum number of iterations"; throw new PrismException(msg); } - + // Return results res = new ModelCheckerResult(); res.soln = soln; @@ -1027,7 +1027,7 @@ public class MDPModelChecker extends ProbModelChecker unknown.andNot(target); if (remain != null) unknown.and(remain); - + // Start iterations iters = 0; while (iters < k) { @@ -1087,7 +1087,8 @@ public class MDPModelChecker extends ProbModelChecker * @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. */ - public ModelCheckerResult computeReachRewards(MDP mdp, MDPRewards mdpRewards, BitSet target, boolean min, double init[], BitSet known) throws PrismException + public ModelCheckerResult computeReachRewards(MDP mdp, MDPRewards mdpRewards, BitSet target, boolean min, double init[], BitSet known) + throws PrismException { ModelCheckerResult res = null; BitSet inf; @@ -1166,7 +1167,8 @@ public class MDPModelChecker extends ProbModelChecker * @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. */ - protected ModelCheckerResult computeReachRewardsGaussSeidel(MDP mdp, MDPRewards mdpRewards, BitSet target, BitSet inf, boolean min, double init[], BitSet known) throws PrismException + protected ModelCheckerResult computeReachRewardsGaussSeidel(MDP mdp, MDPRewards mdpRewards, BitSet target, BitSet inf, boolean min, double init[], + BitSet known) throws PrismException { ModelCheckerResult res; BitSet unknown; @@ -1231,7 +1233,7 @@ public class MDPModelChecker extends ProbModelChecker msg += "\nConsider using a different numerical method or increasing the maximum number of iterations"; throw new PrismException(msg); } - + // Return results res = new ModelCheckerResult(); res.soln = soln; @@ -1251,7 +1253,8 @@ public class MDPModelChecker extends ProbModelChecker * @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. */ - protected ModelCheckerResult computeReachRewardsValIter(MDP mdp, MDPRewards mdpRewards, BitSet target, BitSet inf, boolean min, double init[], BitSet known) throws PrismException + protected ModelCheckerResult computeReachRewardsValIter(MDP mdp, MDPRewards mdpRewards, BitSet target, BitSet inf, boolean min, double init[], BitSet known) + throws PrismException { ModelCheckerResult res; BitSet unknown; @@ -1321,7 +1324,7 @@ public class MDPModelChecker extends ProbModelChecker msg += "\nConsider using a different numerical method or increasing the maximum number of iterations"; throw new PrismException(msg); } - + // Return results res = new ModelCheckerResult(); res.soln = soln; @@ -1353,7 +1356,7 @@ public class MDPModelChecker extends ProbModelChecker * @param mdp The MDP * @param adv The adversary */ - public void restrictAdversaryToReachableStates(MDP mdp,int adv[]) + public void restrictAdversaryToReachableStates(MDP mdp, int adv[]) { BitSet restrict = new BitSet(); BitSet explore = new BitSet(); @@ -1388,7 +1391,7 @@ public class MDPModelChecker extends ProbModelChecker adv[s] = -1; } } - + /** * Simple test program. */