From d2cfbb6096c07b7e0de43682dd24063f9c625065 Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 9 Feb 2018 12:09:50 +0100 Subject: [PATCH] fix issue where constraint based multi objective model checking lead to a stack overflow. --- .../SparseCbAchievabilityQuery.cpp | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp index ae03a7d9e..710fd92d3 100644 --- a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp +++ b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp @@ -138,12 +138,26 @@ 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()); - storm::expressions::Expression objValue = zero; + std::vector objectiveValues; for (uint_fast64_t choice = 0; choice < rewards.size(); ++choice) { if (!storm::utility::isZero(rewards[choice])) { - objValue = objValue + (this->expressionManager->rational(rewards[choice]) * expectedChoiceVariables[choice].getExpression()); + 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(); + // 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()); switch (obj.formula->getBound().comparisonType) {