Fixes in strategy generation for expected rewards in explicit engine (should only check for strict changes in max case).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7005 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/explicit/MDPSimple.java

@@ -874,8 +874,10 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple
 		minmax += mdpRewards.getStateReward(s);
 		// If strategy generation is enabled, store optimal choice
 		if (strat != null & !first) {
-			// Only remember strictly better choices (required for max)
-			if (strat[s] == -1 || (min && minmax < vect[s]) || (!min && minmax > vect[s])) {
+			// For max, only remember strictly better choices
+			if (min) {
+				strat[s] = stratCh;
+			} else if (strat[s] == -1 || minmax > vect[s]) {
 				strat[s] = stratCh;
 			}
 		}
@@ -925,8 +927,10 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple
 		minmax += mdpRewards.getStateReward(s);
 		// If strategy generation is enabled, store optimal choice
 		if (strat != null & !first) {
-			// Only remember strictly better choices (required for max)
-			if (strat[s] == -1 || (min && minmax < vect[s]) || (!min && minmax > vect[s])) {
+			// For max, only remember strictly better choices
+			if (min) {
+				strat[s] = stratCh;
+			} else if (strat[s] == -1 || minmax > vect[s]) {
 				strat[s] = stratCh;
 			}
 		}

prism/src/explicit/MDPSparse.java

@@ -947,8 +947,10 @@ public class MDPSparse extends MDPExplicit
 		minmax += mdpRewards.getStateReward(s);
 		// If strategy generation is enabled, store optimal choice
 		if (strat != null & !first) {
-			// Only remember strictly better choices (required for max)
-			if (strat[s] == -1 || (min && minmax < vect[s]) || (!min && minmax > vect[s])) {
+			// For max, only remember strictly better choices
+			if (min) {
+				strat[s] = stratCh;
+			} else if (strat[s] == -1 || minmax > vect[s]) {
 				strat[s] = stratCh;
 			}
 		}
@@ -995,8 +997,10 @@ public class MDPSparse extends MDPExplicit
 		minmax += mdpRewards.getStateReward(s);
 		// If strategy generation is enabled, store optimal choice
 		if (strat != null & !first) {
-			// Only remember strictly better choices (required for max)
-			if (strat[s] == -1 || (min && minmax < vect[s]) || (!min && minmax > vect[s])) {
+			// For max, only remember strictly better choices
+			if (min) {
+				strat[s] = stratCh;
+			} else if (strat[s] == -1 || minmax > vect[s]) {
 				strat[s] = stratCh;
 			}
 		}