diff --git a/prism/src/explicit/rewards/ConstructRewards.java b/prism/src/explicit/rewards/ConstructRewards.java index e19e77a0..0ef9d089 100644 --- a/prism/src/explicit/rewards/ConstructRewards.java +++ b/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"); diff --git a/prism/src/parser/ExplicitFiles2ModulesFile.java b/prism/src/parser/ExplicitFiles2ModulesFile.java index 487fdc34..257cb741 100644 --- a/prism/src/parser/ExplicitFiles2ModulesFile.java +++ b/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; diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index cbc22327..48c63317 100644 --- a/prism/src/prism/Prism.java +++ b/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