From dc82a6ef672fb06ec46e3bce040ec5a81ad7236c Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 21 Jul 2017 22:48:02 +0000 Subject: [PATCH] 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 | 4 ++++ prism/src/parser/ExplicitFiles2ModulesFile.java | 8 +++++++- prism/src/prism/Prism.java | 8 +++++++- 3 files changed, 18 insertions(+), 2 deletions(-) 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