|
|
|
@ -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<Integer> opt = mdp.mvMultMinMaxSingleChoices(i, soln, min, soln2[i]); |
|
|
|
policy[i] = opt.get(0); |
|
|
|
adv[i] = opt.get(0); |
|
|
|
} |
|
|
|
} |
|
|
|
} |
|
|
|
|