From 9d29f369e263c9cba2e843501a5cbf52d1faaa59 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Fri, 16 Oct 2020 13:12:40 +0200 Subject: [PATCH] fixed incorrect hanlding of lra objecties in bounded phase --- .../multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp | 2 +- .../multiobjective/pcaa/StandardMdpPcaaWeightVectorChecker.cpp | 2 +- .../multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp index 8b67a031a..029e8244f 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp @@ -116,7 +116,7 @@ namespace storm { std::vector optimalChoicesAtCurrentEpoch(PS.getNumberOfStates(), std::numeric_limits::max()); // Stores the objectives for which we need to compute values in the current time epoch. - storm::storage::BitVector consideredObjectives = this->objectivesWithNoUpperTimeBound; + storm::storage::BitVector consideredObjectives = this->objectivesWithNoUpperTimeBound & ~this->lraObjectives; auto upperTimeBoundIt = upperTimeBounds.begin(); uint_fast64_t currentEpoch = upperTimeBounds.empty() ? 0 : upperTimeBoundIt->first; diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardMdpPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardMdpPcaaWeightVectorChecker.cpp index cadd5f217..ef08399db 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardMdpPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardMdpPcaaWeightVectorChecker.cpp @@ -83,7 +83,7 @@ namespace storm { } // Stores the objectives for which we need to compute values in the current time epoch. - storm::storage::BitVector consideredObjectives = this->objectivesWithNoUpperTimeBound; + storm::storage::BitVector consideredObjectives = this->objectivesWithNoUpperTimeBound & ~this->lraObjectives; auto stepBoundIt = stepBounds.begin(); uint_fast64_t currentEpoch = stepBounds.empty() ? 0 : stepBoundIt->first; diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp index 677b7987c..13621f683 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp @@ -161,7 +161,7 @@ namespace storm { unboundedIndividualPhase(env, weightVector); // Only invoke boundedPhase if necessarry, i.e., if there is at least one objective with a time bound for (auto const& obj : this->objectives) { - if (!obj.formula->getSubformula().isTotalRewardFormula()) { + if (!obj.formula->getSubformula().isTotalRewardFormula() && !obj.formula->getSubformula().isLongRunAverageRewardFormula()) { boundedPhase(env, weightVector, weightedRewardVector); break; }