From 3db0ff124fa1382858e1b97b304133ba321a05d9 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 9 Sep 2020 15:29:34 +0200 Subject: [PATCH] Started to make multiobjective reward analysis aware of LRA formulas. --- .../preprocessing/SparseMultiObjectiveRewardAnalysis.cpp | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectiveRewardAnalysis.cpp b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectiveRewardAnalysis.cpp index 3c9c0e6a4..2e88fda25 100644 --- a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectiveRewardAnalysis.cpp +++ b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectiveRewardAnalysis.cpp @@ -52,9 +52,12 @@ namespace storm { storm::storage::BitVector zeroRewardChoices(preprocessorResult.preprocessedModel->getNumberOfChoices(), true); for (auto const& obj : preprocessorResult.objectives) { if (obj.formula->isRewardOperatorFormula()) { - STORM_LOG_WARN_COND(obj.formula->getSubformula().isTotalRewardFormula() || obj.formula->getSubformula().isCumulativeRewardFormula(), "Analyzing reachability reward formulas is not supported properly."); - auto const& rewModel = preprocessorResult.preprocessedModel->getRewardModel(obj.formula->asRewardOperatorFormula().getRewardModelName()); - zeroRewardChoices &= rewModel.getChoicesWithZeroReward(transitions); + if (obj.formula->getSubformula().isTotalRewardFormula() || obj.formula->getSubformula().isCumulativeRewardFormula()) { + auto const& rewModel = preprocessorResult.preprocessedModel->getRewardModel(obj.formula->asRewardOperatorFormula().getRewardModelName()); + zeroRewardChoices &= rewModel.getChoicesWithZeroReward(transitions); + } else { + STORM_LOG_WARN_COND(obj.formula->getSubformula().isLongRunAverageRewardFormula(), "Analyzing subformula " << obj.formula->getSubformula() << " is not supported properly."); + } } }