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

@@ -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;
 			}
 		}

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;
 			}
 		}