From c867d63120f22f4a10b66d0d68a55cf5168504da Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 12 Oct 2018 14:25:02 +0200 Subject: [PATCH] imported patch iteration-method-jacobi-mdp-explicit.patch --- prism/src/explicit/IterationMethodJacobi.java | 41 ++++++++++++++++--- prism/src/explicit/MDP.java | 37 +++++++++++++++++ 2 files changed, 73 insertions(+), 5 deletions(-) diff --git a/prism/src/explicit/IterationMethodJacobi.java b/prism/src/explicit/IterationMethodJacobi.java index 83a8c8b1..0f41518e 100644 --- a/prism/src/explicit/IterationMethodJacobi.java +++ b/prism/src/explicit/IterationMethodJacobi.java @@ -30,7 +30,6 @@ import common.IntSet; import explicit.rewards.MCRewards; import explicit.rewards.MDPRewards; import prism.PrismException; -import prism.PrismNotSupportedException; /** * IterationMethod that encapsulates the functionality of the Jacobi method. @@ -106,27 +105,59 @@ class IterationMethodJacobi extends IterationMethod { @Override public IterationValIter forMvMultMinMax(MDP mdp, boolean min, int[] strat) throws PrismException { - throw new PrismNotSupportedException("Jacobi not supported for MDPs"); + return new TwoVectorIteration(mdp, null) { + @Override + public void doIterate(IntSet states) + { + mdp.mvMultJacMinMax(soln, min, soln2, states.iterator(), strat); + } + }; } @Override public IterationIntervalIter forMvMultMinMaxInterval(MDP mdp, boolean min, int[] strat, boolean fromBelow, boolean enforceMonotonicity, boolean checkMonotonicity) throws PrismException { - throw new PrismNotSupportedException("Jacobi not supported for MDPs"); + IterationPostProcessor post = (soln, soln2, states) -> { + twoVectorPostProcessing(soln, soln2, states, fromBelow, enforceMonotonicity, checkMonotonicity); + }; + + return new TwoVectorIteration(mdp, post) { + @Override + public void doIterate(IntSet states) + { + mdp.mvMultJacMinMax(soln, min, soln2, states.iterator(), strat); + } + }; } @Override public IterationValIter forMvMultRewMinMax(MDP mdp, MDPRewards rewards, boolean min, int[] strat) throws PrismException { - throw new PrismNotSupportedException("Jacobi not supported for MDPs"); + return new TwoVectorIteration(mdp, null) { + @Override + public void doIterate(IntSet states) + { + mdp.mvMultJacRewMinMax(soln, rewards, min, soln2, states.iterator(), strat); + } + }; } @Override public IterationIntervalIter forMvMultRewMinMaxInterval(MDP mdp, MDPRewards rewards, boolean min, int[] strat, boolean fromBelow, boolean enforceMonotonicity, boolean checkMonotonicity) throws PrismException { - throw new PrismNotSupportedException("Jacobi not supported for MDPs"); + IterationPostProcessor post = (soln, soln2, states) -> { + twoVectorPostProcessing(soln, soln2, states, fromBelow, enforceMonotonicity, checkMonotonicity); + }; + + return new TwoVectorIteration(mdp, post) { + @Override + public void doIterate(IntSet states) + { + mdp.mvMultJacRewMinMax(soln, rewards, min, soln2, states.iterator(), strat); + } + }; } @Override diff --git a/prism/src/explicit/MDP.java b/prism/src/explicit/MDP.java index 613d0a20..8ded101a 100644 --- a/prism/src/explicit/MDP.java +++ b/prism/src/explicit/MDP.java @@ -322,6 +322,24 @@ public interface MDP extends MDPGeneric } } + /** + * Do a Jacobi-style matrix-vector multiplication followed by min/max. + * i.e. for all s: min/max_k { (sum_{j!=s} P_k(s,j)*vect[j]) / 1-P_k(s,s) } + * Optionally, store optimal (memoryless) strategy info. + * @param vect Vector to multiply by (and store the result in) + * @param min Min or max for (true=min, false=max) + * @param result Vector to store result in + * @param states Perform computation for these rows, in the iteration order + * @param strat Storage for (memoryless) strategy choice indices (ignored if null) + */ + public default void mvMultJacMinMax(double vect[], boolean min, double result[], PrimitiveIterator.OfInt states, int strat[]) + { + while (states.hasNext()) { + final int s = states.nextInt(); + vect[s] = mvMultMinMaxSingle(s, vect, min, strat); + } + } + /** * Do a single row of Jacobi-style matrix-vector multiplication followed by min/max. * i.e. return min/max_k { (sum_{j!=s} P_k(s,j)*vect[j]) / 1-P_k(s,s) } @@ -600,6 +618,25 @@ public interface MDP extends MDPGeneric } } + /** + * Do a Jacobi-style matrix-vector multiplication and sum of rewards followed by min/max, i.e. one step of value iteration. + * i.e. for all s: result[s] = min/max_k { rew(s) + rew_k(s) + (sum_{j!=s} P_k(s,j)*vect[j]) / 1-P_k(s,s) } + * Optionally, store optimal (memoryless) strategy info. + * @param vect Vector to multiply by + * @param mdpRewards The rewards + * @param min Min or max for (true=min, false=max) + * @param result Vector to store result in + * @param states Perform computation for these rows, in the iteration order + * @param strat Storage for (memoryless) strategy choice indices (ignored if null) + */ + public default void mvMultJacRewMinMax(double vect[], MDPRewards mdpRewards, boolean min, double result[], PrimitiveIterator.OfInt states, int strat[]) + { + while (states.hasNext()) { + final int s = states.nextInt(); + result[s] = mvMultRewJacMinMaxSingle(s, vect, mdpRewards, min, strat); + } + } + /** * Do a single row of Jacobi-style matrix-vector multiplication and sum of rewards followed by min/max. * i.e. return min/max_k { rew(s) + rew_k(s) + (sum_{j!=s} P_k(s,j)*vect[j]) / 1-P_k(s,s) }