Sparse engine with -exportstrat: Fix crash during strategy initialization

When converting an MTBDD to an integer vector (as is done to prepare the storage for the computed strategy for Pmax-Until using the sparse engine), the MTBDD has to be zero for non-reachable states, as that could lead to out-of-bounds writes to the array during conversion.

This commit adds the required restriction to reach in prism.NondetModelChecker.

+ test case
+ fixes deref of 'yes' during initialization

prism-tests/bugfixes/stratgenreach.nm

@@ -0,0 +1,11 @@
+// bugfix: -exportstrat for MDP using -sparse, missing restriction
+// to reachable state space when initializing strategy storage vector
+
+mdp
+
+module m 
+  s: [0..2] init 0;
+
+  [a] s=0 -> 1/2:(s'=0) + 1/2:(s'=1);
+  [b] s=0 -> 1/3:(s'=2) + 2/3:(s'=1);
+endmodule

prism-tests/bugfixes/stratgenreach.nm.props

@@ -0,0 +1,2 @@
+// RESULT: 1.0
+Pmax=?[ F s=1 ]

prism-tests/bugfixes/stratgenreach.nm.props.args

@@ -0,0 +1 @@
+-sparse -exportstrat stratgenreach.nm.props.strat

prism-tests/bugfixes/stratgenreach.nm.props.strat

@@ -0,0 +1 @@
+0:a

prism/src/prism/NondetModelChecker.java

@@ -2048,7 +2048,10 @@ public class NondetModelChecker extends NonProbModelChecker
 				case Prism.SPARSE:
 					IntegerVector strat = null;
 					if (genStrat) {
-						JDDNode ddStrat = JDD.ITE(yes, JDD.Constant(-2), JDD.Constant(-1));
+						// prepare strategy storage for the sparse engine computation
+						JDDNode ddStrat = JDD.ITE(yes.copy(), JDD.Constant(-2), JDD.Constant(-1));
+						// restrict to the reachable state space of the model (required for conversion to integer array)
+						ddStrat = JDD.Times(ddStrat, reach.copy());
 						strat = new IntegerVector(ddStrat, allDDRowVars, odd);
 						JDD.Deref(ddStrat);
 					}