From d54e92533ca56c5babe88f70118b7e170da42a80 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 12 Sep 2011 20:41:10 +0000 Subject: [PATCH] Another fix for adv gen in explicit engine: min probs should not be treated as for max probs. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3691 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/MDPSimple.java | 6 ++++-- prism/src/explicit/MDPSparse.java | 6 ++++-- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/prism/src/explicit/MDPSimple.java b/prism/src/explicit/MDPSimple.java index 0350c95f..cdf21677 100644 --- a/prism/src/explicit/MDPSimple.java +++ b/prism/src/explicit/MDPSimple.java @@ -721,8 +721,10 @@ public class MDPSimple extends ModelExplicit implements MDP, ModelSimple } // 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])) { + // For max, only remember strictly better choices + if (min) { + adv[s] = advCh; + } else if (adv[s] == -1 || minmax > vect[s]) { adv[s] = advCh; } } diff --git a/prism/src/explicit/MDPSparse.java b/prism/src/explicit/MDPSparse.java index 46c5d121..cf3feebe 100644 --- a/prism/src/explicit/MDPSparse.java +++ b/prism/src/explicit/MDPSparse.java @@ -785,8 +785,10 @@ public class MDPSparse extends ModelExplicit implements MDP } // 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])) { + // For max, only remember strictly better choices + if (min) { + adv[s] = advCh; + } else if (adv[s] == -1 || minmax > vect[s]) { adv[s] = advCh; } }