diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index ac6b3bc3..13d34fd4 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -768,7 +768,7 @@ public class MDPModelChecker extends ProbModelChecker protected ModelCheckerResult computeReachProbsPolIter(MDP mdp, BitSet no, BitSet yes, boolean min) throws PrismException { ModelCheckerResult res; - int i, n, iters, totalIters, diff; + int i, n, iters, totalIters; double soln[], soln2[]; boolean done; long timer; @@ -817,7 +817,6 @@ public class MDPModelChecker extends ProbModelChecker // Check if optimal, improve non-optimal choices mdp.mvMultMinMax(soln, min, soln2, null, false, null); done = true; - diff = 0; for (i = 0; i < n; i++) { // Don't look at no/yes states - we don't store adversary info for them, // so they might appear non-optimal @@ -825,7 +824,6 @@ public class MDPModelChecker extends ProbModelChecker continue; if (!PrismUtils.doublesAreClose(soln[i], soln2[i], termCritParam, termCrit == TermCrit.ABSOLUTE)) { done = false; - diff++; List opt = mdp.mvMultMinMaxSingleChoices(i, soln, min, soln2[i]); // If update adversary if strictly better if (!opt.contains(adv[i])) @@ -857,7 +855,7 @@ public class MDPModelChecker extends ProbModelChecker protected ModelCheckerResult computeReachProbsModPolIter(MDP mdp, BitSet no, BitSet yes, boolean min) throws PrismException { ModelCheckerResult res; - int i, n, iters, totalIters, diff; + int i, n, iters, totalIters; double soln[], soln2[]; boolean done; long timer; @@ -906,7 +904,6 @@ public class MDPModelChecker extends ProbModelChecker // Check if optimal, improve non-optimal choices mdp.mvMultMinMax(soln, min, soln2, null, false, null); done = true; - diff = 0; for (i = 0; i < n; i++) { // Don't look at no/yes states - we don't store adversary info for them, // so they might appear non-optimal @@ -914,7 +911,6 @@ public class MDPModelChecker extends ProbModelChecker continue; if (!PrismUtils.doublesAreClose(soln[i], soln2[i], termCritParam, termCrit == TermCrit.ABSOLUTE)) { done = false; - diff++; List opt = mdp.mvMultMinMaxSingleChoices(i, soln, min, soln2[i]); adv[i] = opt.get(0); }