From f49ce60f1baad9755624e7aa5f6ea829c4a18c0c Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 8 Sep 2011 19:51:59 +0000 Subject: [PATCH] Fixes in explicit MDP adversary generation (min case can give wrong answer). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3629 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/MDPSimple.java | 18 ++++++++++-------- prism/src/explicit/MDPSparse.java | 18 ++++++++++-------- 2 files changed, 20 insertions(+), 16 deletions(-) diff --git a/prism/src/explicit/MDPSimple.java b/prism/src/explicit/MDPSimple.java index 8e4fd924..60db7605 100644 --- a/prism/src/explicit/MDPSimple.java +++ b/prism/src/explicit/MDPSimple.java @@ -692,7 +692,7 @@ public class MDPSimple extends ModelExplicit implements MDP, ModelSimple @Override public double mvMultMinMaxSingle(int s, double vect[], boolean min, int adv[]) { - int j, k; + int j, k, advCh = -1; double d, prob, minmax; boolean first; List step; @@ -713,17 +713,19 @@ public class MDPSimple extends ModelExplicit implements MDP, ModelSimple if (first || (min && d < minmax) || (!min && d > minmax)) { minmax = d; // If adversary generation is enabled, remember optimal choice - if (adv != null) { - // Only remember strictly better choices - // (required if either player is doing max) - if (adv[s] == -1 || (min && minmax < vect[s]) || (!min && minmax > vect[s])) { - adv[s] = j; - } - } + if (adv != null) + advCh = j; } first = false; j++; } + // If adversary generation is enabled, store optimal choice + if (adv != null & !first) { + // Only remember strictly better choices (required for max) + if (adv[s] == -1 || (min && minmax < vect[s]) || (!min && minmax > vect[s])) { + adv[s] = advCh; + } + } return minmax; } diff --git a/prism/src/explicit/MDPSparse.java b/prism/src/explicit/MDPSparse.java index b0ba62a0..6b2ce2a5 100644 --- a/prism/src/explicit/MDPSparse.java +++ b/prism/src/explicit/MDPSparse.java @@ -758,7 +758,7 @@ public class MDPSparse extends ModelExplicit implements MDP @Override public double mvMultMinMaxSingle(int s, double vect[], boolean min, int adv[]) { - int j, k, l1, h1, l2, h2; + int j, k, l1, h1, l2, h2, advCh = -1; double d, minmax; boolean first; @@ -778,16 +778,18 @@ public class MDPSparse extends ModelExplicit implements MDP if (first || (min && d < minmax) || (!min && d > minmax)) { minmax = d; // If adversary generation is enabled, remember optimal choice - if (adv != null) { - // Only remember strictly better choices - // (required if either player is doing max) - if (adv[s] == -1 || (min && minmax < vect[s]) || (!min && minmax > vect[s])) { - adv[s] = j - l1; - } - } + if (adv != null) + advCh = j - l1; } first = false; } + // If adversary generation is enabled, store optimal choice + if (adv != null & !first) { + // Only remember strictly better choices (required for max) + if (adv[s] == -1 || (min && minmax < vect[s]) || (!min && minmax > vect[s])) { + adv[s] = advCh; + } + } return minmax; }