From ba96fde3c980396879bee868f119b3ee88b6505a Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 1 Mar 2018 10:27:11 +0100 Subject: [PATCH] fixed sum that was too much nested --- .../SparseCbAchievabilityQuery.cpp | 23 +++++---------- src/storm/utility/ExpressionHelper.cpp | 29 +++++++++++++++++++ src/storm/utility/ExpressionHelper.h | 28 ++++++++++++++++++ 3 files changed, 65 insertions(+), 15 deletions(-) create mode 100644 src/storm/utility/ExpressionHelper.cpp create mode 100644 src/storm/utility/ExpressionHelper.h diff --git a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp index 710fd92d3..5a65bd502 100644 --- a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp +++ b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp @@ -9,6 +9,7 @@ #include "storm/utility/vector.h" #include "storm/utility/solver.h" #include "storm/utility/Stopwatch.h" +#include "storm/utility/ExpressionHelper.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/modules/CoreSettings.h" @@ -99,11 +100,13 @@ namespace storm { for (auto& var : expectedChoiceVariables) { solver->add(var.getExpression() >= zero); } - storm::expressions::Expression bottomStateSum = zero; + std::vector bottomStateVarsAsExpression; + bottomStateVarsAsExpression.reserve(bottomStateVariables.size()); for (auto& var : bottomStateVariables) { solver->add(var.getExpression() >= zero); - bottomStateSum = bottomStateSum + var.getExpression(); + bottomStateVarsAsExpression.push_back(var.getExpression()); } + auto bottomStateSum = storm::utility::ExpressionHelper(this->expressionManager).sum(std::move(bottomStateVarsAsExpression)); solver->add(bottomStateSum == one); // assert that the "incoming" value of each state equals the "outgoing" value @@ -138,25 +141,15 @@ namespace storm { STORM_LOG_THROW(obj.formula->hasBound(), storm::exceptions::InvalidOperationException, "Invoked achievability query but no bound was specified for at least one objective."); STORM_LOG_THROW(obj.formula->asRewardOperatorFormula().hasRewardModelName(), storm::exceptions::InvalidOperationException, "Expected reward operator with a reward model name. Got " << *obj.formula << " instead."); std::vector rewards = getActionBasedExpectedRewards(obj.formula->asRewardOperatorFormula().getRewardModelName()); + + // Get the sum of all objective values std::vector objectiveValues; for (uint_fast64_t choice = 0; choice < rewards.size(); ++choice) { if (!storm::utility::isZero(rewards[choice])) { objectiveValues.push_back(this->expressionManager->rational(rewards[choice]) * expectedChoiceVariables[choice].getExpression()); } } - - // Get the sum of all objective values - // As the sum can potentially have many summands, we want to make sure that the formula tree is (roughly balanced) - auto vIt = objectiveValues.begin(); - while (objectiveValues.size() > 1) { - if (vIt == objectiveValues.end() || vIt == objectiveValues.end() - 1) { - vIt = objectiveValues.begin(); - } - *vIt = *vIt + objectiveValues.back(); - objectiveValues.pop_back(); - ++vIt; - } - storm::expressions::Expression objValue = objectiveValues.empty() ? zero : objectiveValues.front(); + auto objValue = storm::utility::ExpressionHelper(this->expressionManager).sum(std::move(objectiveValues)); // We need to actually evaluate the threshold as rational number. Otherwise a threshold like '<=16/9' might be considered as 1 due to integer division storm::expressions::Expression threshold = this->expressionManager->rational(obj.formula->getThreshold().evaluateAsRational()); diff --git a/src/storm/utility/ExpressionHelper.cpp b/src/storm/utility/ExpressionHelper.cpp new file mode 100644 index 000000000..219d6e39c --- /dev/null +++ b/src/storm/utility/ExpressionHelper.cpp @@ -0,0 +1,29 @@ +#include "storm/utility/ExpressionHelper.h" +#include "storm/utility/constants.h" + +namespace storm { + namespace utility { + + ExpressionHelper::ExpressionHelper(std::shared_ptr const& expressionManager) : manager(expressionManager) { + // Intentionally left empty + } + + storm::expressions::Expression ExpressionHelper::sum(std::vector&& summands) const { + if (summands.empty()) { + return manager->rational(storm::utility::zero()); + } + // As the sum can potentially have many summands, we want to make sure that the formula tree is (roughly balanced) + auto it = summands.begin(); + while (summands.size() > 1) { + if (it == summands.end() || it == summands.end() - 1) { + it = summands.begin(); + } + *it = *it + summands.back(); + summands.pop_back(); + ++it; + } + return summands.front(); + } + + } +} \ No newline at end of file diff --git a/src/storm/utility/ExpressionHelper.h b/src/storm/utility/ExpressionHelper.h new file mode 100644 index 000000000..6c171a286 --- /dev/null +++ b/src/storm/utility/ExpressionHelper.h @@ -0,0 +1,28 @@ +#pragma once + +#include +#include +#include "storm/storage/expressions/Expression.h" +#include "storm/storage/expressions/ExpressionManager.h" + +namespace storm { + namespace utility { + + class ExpressionHelper { + + public: + ExpressionHelper(std::shared_ptr const& expressionManager); + + /*! + * Creates an expression that is the sum over all the given summands. + */ + storm::expressions::Expression sum(std::vector&& summands) const; + + private: + + std::shared_ptr manager; + }; + + + } +} \ No newline at end of file