From e113bff2c71ad716cdad281f25ab799fac362743 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Sun, 11 Sep 2016 11:18:42 +0000 Subject: [PATCH] ModelInfo: add method to query the existence of transition rewards, add check for explicit DTMC/CTMC reward construction During reward construction in the explicit engine using the new ModelGenerator functionality (see SVN 11772), the check for transition rewards was missing (he explicit engine currently does not support transition rewards for DTMCs and CTMCs). This commit adds functionality to ModelInfo to determine whether a reward structure defines transition rewards and adds a corresponding check during reward construction. Example: prism-examples/dice/dice.pm with R=?[ F s=7 ] and -explicit returns 0 instead of an error message. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11802 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/rewards/ConstructRewards.java | 5 +++++ prism/src/parser/ast/ModulesFile.java | 7 +++++++ prism/src/prism/ModelInfo.java | 9 ++++++++- prism/src/prism/TestModelGenerator.java | 6 ++++++ prism/src/simulator/ModulesFileModelGenerator.java | 6 ++++++ .../src/simulator/ModulesFileModelGeneratorSymbolic.java | 6 ++++++ 6 files changed, 38 insertions(+), 1 deletion(-) 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); + } }