Bug fix in (recent) explicit engine simple->sparse conversion of actions.

And a test case.

prism-tests/bugfixes/mdp-action-storage-bug.prism

@@ -0,0 +1,11 @@
+mdp
+
+module M
+
+	s:[0..3];
+	
+	[a] s=0 -> (s'=2);
+	[b] s=2 -> (s'=1);
+
+endmodule
+

prism-tests/bugfixes/mdp-action-storage-bug.prism.props

@@ -0,0 +1,2 @@
+// RESULT: true
+P>=1 [ F s=1 ];

prism-tests/bugfixes/mdp-action-storage-bug.prism.props.args

@@ -0,0 +1,2 @@
+-ex
+-m

prism/src/explicit/ChoiceActionsSimple.java

@@ -166,6 +166,8 @@ public class ChoiceActionsSimple
 	 * Convert to "sparse" storage for a given model,
 	 * i.e., a single array where all actions are stored in
 	 * order, per state and then per choice.
+	 * A corresponding NondetModel is required because the
+	 * number of states and choices per state may be unknown.
 	 * If this action storage is completely empty,
 	 * then this method may simply return null.
 	 */
@@ -180,7 +182,7 @@ public class ChoiceActionsSimple
 			for (int s = 0; s < numStates; s++) {
 				int numChoices = model.getNumChoices(s);
 				for (int i = 0; i < numChoices; i++) {
-					arr[count++] = model.getAction(s, i);
+					arr[count++] = getAction(s, i);
 				}
 			}
 			return arr;

prism/src/explicit/MDPSparse.java

@@ -231,7 +231,9 @@ public class MDPSparse extends MDPExplicit
 		}
 		choiceStarts[numDistrs] = numTransitions;
 		rowStarts[numStates] = numDistrs;
-		actions = mdp.actions.convertToSparseStorage(mdp);
+		// Copy the actions too
+		// Note: could pass 'mdp' or 'this' to convertToSparseStorage (use latter for consistency)
+		actions = mdp.actions.convertToSparseStorage(this);
 	}
 
 	/**
@@ -295,7 +297,9 @@ public class MDPSparse extends MDPExplicit
 		}
 		choiceStarts[numDistrs] = numTransitions;
 		rowStarts[numStates] = numDistrs;
-		actions = mdp.actions.convertToSparseStorage(mdp);
+		// Copy the actions too (after permuting)
+		// Note: we pass _this_ new, permuted model to convertToSparseStorage
+		actions = new ChoiceActionsSimple(mdp.actions, permut).convertToSparseStorage(this);
 	}
 
 	/**