From 1ce1446eb53fdfaa578a3aeb744add9f62574b80 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 21 Jul 2017 15:50:06 +0000 Subject: [PATCH] explicit.MDPModelChecker: support backward Gauss-Seidel during policy iteration git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12131 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/MDPModelChecker.java | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index fc2206de..b1f5165d 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -925,6 +925,8 @@ public class MDPModelChecker extends ProbModelChecker strat[i] = 0; } + boolean backwardsGS = (linEqMethod == LinEqMethod.BACKWARDS_GAUSS_SEIDEL); + // Start iterations iters = totalIters = 0; done = false; @@ -932,7 +934,7 @@ public class MDPModelChecker extends ProbModelChecker iters++; // Solve induced DTMC for strategy dtmc = new DTMCFromMDPMemorylessAdversary(mdp, strat); - res = mcDTMC.computeReachProbsGaussSeidel(dtmc, no, yes, reUseSoln ? soln : null, null); + res = mcDTMC.computeReachProbsGaussSeidel(dtmc, no, yes, reUseSoln ? soln : null, null, backwardsGS); soln = res.soln; totalIters += res.numIters; // Check if optimal, improve non-optimal choices @@ -1025,6 +1027,8 @@ public class MDPModelChecker extends ProbModelChecker strat[i] = 0; } + boolean backwardsGS = (linEqMethod == LinEqMethod.BACKWARDS_GAUSS_SEIDEL); + // Start iterations iters = totalIters = 0; done = false; @@ -1032,7 +1036,7 @@ public class MDPModelChecker extends ProbModelChecker iters++; // Solve induced DTMC for strategy dtmc = new DTMCFromMDPMemorylessAdversary(mdp, strat); - res = mcDTMC.computeReachProbsGaussSeidel(dtmc, no, yes, soln, null); + res = mcDTMC.computeReachProbsGaussSeidel(dtmc, no, yes, soln, null, backwardsGS); soln = res.soln; totalIters += res.numIters; // Check if optimal, improve non-optimal choices