diff --git a/prism/src/explicit/rewards/ConstructRewards.java b/prism/src/explicit/rewards/ConstructRewards.java index b14485dd..e19e77a0 100644 --- a/prism/src/explicit/rewards/ConstructRewards.java +++ b/prism/src/explicit/rewards/ConstructRewards.java @@ -230,6 +230,11 @@ public class ConstructRewards */ public MCRewards buildMCRewardStructure(DTMC mc, ModelGenerator modelGen, int r) throws PrismException { + if (modelGen.rewardStructHasTransitionRewards(r)) { + // TODO + throw new PrismNotSupportedException("Explicit engine does not yet handle transition rewards for D/CTMCs"); + } + int numStates = mc.getNumStates(); List statesList = mc.getStatesList(); StateRewardsArray rewSA = new StateRewardsArray(numStates); diff --git a/prism/src/parser/ast/ModulesFile.java b/prism/src/parser/ast/ModulesFile.java index b3bab3c6..9faaf519 100644 --- a/prism/src/parser/ast/ModulesFile.java +++ b/prism/src/parser/ast/ModulesFile.java @@ -1183,6 +1183,13 @@ public class ModulesFile extends ASTElement implements ModelInfo findAllVars(varNames, varTypes); } + @Override + public boolean rewardStructHasTransitionRewards(int i) + { + RewardStruct rewStr = getRewardStruct(i); + return rewStr.getNumTransItems() > 0; + } + /** * Create a VarList object storing information about all variables in this model. * Assumes that values for constants have been provided for the model. diff --git a/prism/src/prism/ModelInfo.java b/prism/src/prism/ModelInfo.java index 440a7a93..c826737b 100644 --- a/prism/src/prism/ModelInfo.java +++ b/prism/src/prism/ModelInfo.java @@ -138,7 +138,14 @@ public interface ModelInfo * Returns null if index is out of range. */ public RewardStruct getRewardStruct(int i); - + + /** + * Returns true if the reward structure with index i + * (indexed from 0, not from 1 like at the user (property language) level) + * defines transition rewards. + */ + public boolean rewardStructHasTransitionRewards(int i); + // TODO: can we remove this? public VarList createVarList() throws PrismException; } diff --git a/prism/src/prism/TestModelGenerator.java b/prism/src/prism/TestModelGenerator.java index aee2db90..8721986e 100644 --- a/prism/src/prism/TestModelGenerator.java +++ b/prism/src/prism/TestModelGenerator.java @@ -164,6 +164,12 @@ public class TestModelGenerator extends DefaultModelGenerator } } + @Override + public boolean rewardStructHasTransitionRewards(int i) + { + return false; + } + @Override public VarList createVarList() { diff --git a/prism/src/simulator/ModulesFileModelGenerator.java b/prism/src/simulator/ModulesFileModelGenerator.java index e102dfb6..3dc753b8 100644 --- a/prism/src/simulator/ModulesFileModelGenerator.java +++ b/prism/src/simulator/ModulesFileModelGenerator.java @@ -414,4 +414,10 @@ public class ModulesFileModelGenerator extends DefaultModelGenerator } return transitionList; } + + @Override + public boolean rewardStructHasTransitionRewards(int i) + { + return modulesFile.rewardStructHasTransitionRewards(i); + } } diff --git a/prism/src/simulator/ModulesFileModelGeneratorSymbolic.java b/prism/src/simulator/ModulesFileModelGeneratorSymbolic.java index dd620b0d..718e81a0 100644 --- a/prism/src/simulator/ModulesFileModelGeneratorSymbolic.java +++ b/prism/src/simulator/ModulesFileModelGeneratorSymbolic.java @@ -462,4 +462,10 @@ public class ModulesFileModelGeneratorSymbolic extends DefaultModelGenerator imp } return constantList.getConstant(i); } + + @Override + public boolean rewardStructHasTransitionRewards(int i) + { + return modulesFile.rewardStructHasTransitionRewards(i); + } }