diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index 31e5aeb6..ac6b3bc3 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -819,7 +819,8 @@ public class MDPModelChecker extends ProbModelChecker done = true; diff = 0; for (i = 0; i < n; i++) { - // NB: We must not check 'no' states (may look non-optimal) + // Don't look at no/yes states - we don't store adversary info for them, + // so they might appear non-optimal if (no.get(i) || yes.get(i)) continue; if (!PrismUtils.doublesAreClose(soln[i], soln2[i], termCritParam, termCrit == TermCrit.ABSOLUTE)) { @@ -860,7 +861,7 @@ public class MDPModelChecker extends ProbModelChecker double soln[], soln2[]; boolean done; long timer; - int policy[]; + int adv[]; DTMCModelChecker mcDTMC; DTMC dtmc; @@ -887,18 +888,18 @@ public class MDPModelChecker extends ProbModelChecker for (i = 0; i < n; i++) soln[i] = soln2[i] = yes.get(i) ? 1.0 : 0.0; - // Generate initial policy - policy = new int[n]; + // Generate initial adversary + adv = new int[n]; for (i = 0; i < n; i++) - policy[i] = 0; + adv[i] = 0; // Start iterations iters = totalIters = 0; done = false; while (!done) { iters++; - // Solve policy - dtmc = new DTMCFromMDPMemorylessAdversary(mdp, policy); + // Solve induced DTMC for adversary + dtmc = new DTMCFromMDPMemorylessAdversary(mdp, adv); res = mcDTMC.computeReachProbsGaussSeidel(dtmc, no, yes, soln, null); soln = res.soln; totalIters += res.numIters; @@ -907,14 +908,15 @@ public class MDPModelChecker extends ProbModelChecker done = true; diff = 0; for (i = 0; i < n; i++) { - // NB: We must not check 'no' states (may look non-optimal) + // Don't look at no/yes states - we don't store adversary info for them, + // so they might appear non-optimal if (no.get(i) || yes.get(i)) continue; if (!PrismUtils.doublesAreClose(soln[i], soln2[i], termCritParam, termCrit == TermCrit.ABSOLUTE)) { done = false; diff++; List opt = mdp.mvMultMinMaxSingleChoices(i, soln, min, soln2[i]); - policy[i] = opt.get(0); + adv[i] = opt.get(0); } } }