diff --git a/src/storm/utility/FilteredRewardModel.h b/src/storm/utility/FilteredRewardModel.h index 32dc13521..5280cfd98 100644 --- a/src/storm/utility/FilteredRewardModel.h +++ b/src/storm/utility/FilteredRewardModel.h @@ -8,9 +8,8 @@ namespace storm { namespace utility { - /* - * This class wraps around a + * This class wraps around a Reward model where certain reward types are disabled. */ template class FilteredRewardModel { @@ -45,20 +44,25 @@ namespace storm { RewardModelType const* rewardModel; }; - template - FilteredRewardModel createFilteredRewardModel(ModelType const& model, CheckTaskType const& checkTask) { - auto const& baseRewardModel = checkTask.isRewardModelSet() ? model.getRewardModel(checkTask.getRewardModel()) : model.getUniqueRewardModel(); - if (checkTask.getFormula().hasRewardAccumulation()) { - auto const& acc = checkTask.getFormula().getRewardAccumulation(); - STORM_LOG_THROW(model.isDiscreteTimeModel() || !acc.isExitSet() || !baseRewardModel.hasStateRewards(), storm::exceptions::NotSupportedException, "Exit rewards for continuous time models are not supported."); + template + FilteredRewardModel createFilteredRewardModel(RewardModelType const& baseRewardModel, bool isDiscreteTimeModel, FormulaType const& formula) { + if (formula.hasRewardAccumulation()) { + auto const& acc = formula.getRewardAccumulation(); + STORM_LOG_THROW(isDiscreteTimeModel || !acc.isExitSet() || !baseRewardModel.hasStateRewards(), storm::exceptions::NotSupportedException, "Exit rewards for continuous time models are not supported."); // Check which of the available reward types are allowed. - bool hasStateRewards = model.isDiscreteTimeModel() ? acc.isExitSet() : acc.isTimeSet(); + bool hasStateRewards = isDiscreteTimeModel ? acc.isExitSet() : acc.isTimeSet(); bool hasStateActionRewards = acc.isStepsSet(); bool hasTransitionRewards = acc.isStepsSet(); - return FilteredRewardModel(baseRewardModel, hasStateRewards, hasStateActionRewards, hasTransitionRewards); + return FilteredRewardModel(baseRewardModel, hasStateRewards, hasStateActionRewards, hasTransitionRewards); } else { - return FilteredRewardModel(baseRewardModel, true, true, true); + return FilteredRewardModel(baseRewardModel, true, true, true); } } + + template + FilteredRewardModel createFilteredRewardModel(ModelType const& model, CheckTaskType const& checkTask) { + auto const& baseRewardModel = checkTask.isRewardModelSet() ? model.getRewardModel(checkTask.getRewardModel()) : model.getUniqueRewardModel(); + return createFilteredRewardModel(baseRewardModel, model.isDiscreteTimeModel(), checkTask.getFormula()); + } } } \ No newline at end of file