From 194625a9c132c0a4cdf6587b23376b3a6341e516 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Mon, 28 Aug 2017 12:45:47 +0200
Subject: [PATCH] explicit.MDPModelChecker: for prob0e, generate strategy also
 for trivial case

---
 prism/src/explicit/MDPModelChecker.java | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java
index 1f015899..da00daf0 100644
--- a/prism/src/explicit/MDPModelChecker.java
+++ b/prism/src/explicit/MDPModelChecker.java
@@ -609,6 +609,11 @@ public class MDPModelChecker extends ProbModelChecker
 		if (target.cardinality() == 0) {
 			soln = new BitSet(mdp.getNumStates());
 			soln.set(0, mdp.getNumStates());
+
+			// for min, generate strategy, any choice (-2) is fine
+			if (min && strat != null) {
+				Arrays.fill(strat, -2);
+			}
 			return soln;
 		}