imported patch iteration-method-jacobi-mdp-explicit.patch

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

prism/src/explicit/MDP.java

@@ -322,6 +322,24 @@ public interface MDP extends MDPGeneric<Double>
 		}
 	}
 
+	/**
+	 * 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<Double>
 		}
 	}
 
+	/**
+	 * 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) }