Fix explicit engine import of state rewards (need to add details to ModelInfo for it to work properly). Also catch attempts to export state rewards more cleanly in this case.

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

prism/src/explicit/rewards/ConstructRewards.java

@@ -230,6 +230,10 @@ public class ConstructRewards
 	 */
 	public MCRewards buildMCRewardStructure(DTMC mc, ModelGenerator modelGen, int r) throws PrismException
 	{
+		if (modelGen == null) {
+			throw new PrismException("No model generator to build reward structure");
+		}
+		
 		if (modelGen.rewardStructHasTransitionRewards(r)) {
 			// TODO
 			throw new PrismNotSupportedException("Explicit engine does not yet handle transition rewards for D/CTMCs");

prism/src/parser/ExplicitFiles2ModulesFile.java

@@ -43,6 +43,7 @@ import parser.ast.ExpressionLiteral;
 import parser.ast.LabelList;
 import parser.ast.Module;
 import parser.ast.ModulesFile;
+import parser.ast.RewardStruct;
 import parser.type.Type;
 import parser.type.TypeBool;
 import parser.type.TypeInt;
@@ -82,7 +83,7 @@ public class ExplicitFiles2ModulesFile extends PrismComponent
 	 * @param transFile transitions file
 	 * @param labelsFile labels file (may be {@code null})
 	 */
-	public ModulesFile buildModulesFile(File statesFile, File transFile, File labelsFile, ModelType typeOverride) throws PrismException
+	public ModulesFile buildModulesFile(File statesFile, File transFile, File labelsFile, File stateRewardsFile, ModelType typeOverride) throws PrismException
 	{
 		ModulesFile modulesFile;
 		ModelType modelType;
@@ -99,6 +100,11 @@ public class ExplicitFiles2ModulesFile extends PrismComponent
 		if (labelsFile != null) {
 			modulesFile.setLabelList(createLabelListFromLabelsFile(labelsFile));
 		}
+		
+		// Add a new (unnamed) reward structure if there is a state rewards file
+		if (stateRewardsFile != null) {
+			modulesFile.addRewardStruct(new RewardStruct());
+		}
 
 		// Set model type: if no preference stated, assume default of MDP
 		modelType = (typeOverride == null) ? ModelType.MDP : typeOverride;

prism/src/prism/Prism.java

@@ -1862,7 +1862,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 		clearBuiltModel();
 		// Construct ModulesFile
 		ExplicitFiles2ModulesFile ef2mf = new ExplicitFiles2ModulesFile(this);
-		currentModulesFile = ef2mf.buildModulesFile(statesFile, transFile, labelsFile, typeOverride);
+		currentModulesFile = ef2mf.buildModulesFile(statesFile, transFile, labelsFile, stateRewardsFile, typeOverride);
 		// Store explicit files info for later
 		explicitFilesStatesFile = statesFile;
 		explicitFilesTransFile = transFile;
@@ -2360,6 +2360,12 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 		int numRewardStructs = currentModelInfo.getNumRewardStructs();
 		if (numRewardStructs == 0) {
 			mainLog.println("\nOmitting state reward export as there are no reward structures");
+			return;
+		}
+		
+		if (currentModelSource == ModelSource.EXPLICIT_FILES && getExplicit()) {
+			mainLog.println("\nOmitting state reward export (not supported when importing files using the explicit engine)");
+			return;
 		}
 		
 		// Rows format does not apply to vectors