s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

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
master
Joachim Klein 9 years ago
parent
452d89e411
commit
1ce1446eb5
1 changed files with 6 additions and 2 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 8
      prism/src/explicit/MDPModelChecker.java

8
prism/src/explicit/MDPModelChecker.java
View File

@ -925,6 +925,8 @@ public class MDPModelChecker extends ProbModelChecker
strat[i] = 0; strat[i] = 0;
} }
boolean backwardsGS = (linEqMethod == LinEqMethod.BACKWARDS_GAUSS_SEIDEL);
// Start iterations // Start iterations
iters = totalIters = 0; iters = totalIters = 0;
done = false; done = false;
@ -932,7 +934,7 @@ public class MDPModelChecker extends ProbModelChecker
iters++; iters++;
// Solve induced DTMC for strategy // Solve induced DTMC for strategy
dtmc = new DTMCFromMDPMemorylessAdversary(mdp, strat); 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; soln = res.soln;
totalIters += res.numIters; totalIters += res.numIters;
// Check if optimal, improve non-optimal choices // Check if optimal, improve non-optimal choices
@ -1025,6 +1027,8 @@ public class MDPModelChecker extends ProbModelChecker
strat[i] = 0; strat[i] = 0;
} }
boolean backwardsGS = (linEqMethod == LinEqMethod.BACKWARDS_GAUSS_SEIDEL);
// Start iterations // Start iterations
iters = totalIters = 0; iters = totalIters = 0;
done = false; done = false;
@ -1032,7 +1036,7 @@ public class MDPModelChecker extends ProbModelChecker
iters++; iters++;
// Solve induced DTMC for strategy // Solve induced DTMC for strategy
dtmc = new DTMCFromMDPMemorylessAdversary(mdp, strat); 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; soln = res.soln;
totalIters += res.numIters; totalIters += res.numIters;
// Check if optimal, improve non-optimal choices // Check if optimal, improve non-optimal choices

Write Preview
Loading…
Cancel
Save