From 139c86f6a05bdbade906b2ce5f78918d949b70ff Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 25 Sep 2020 23:24:42 +0200 Subject: [PATCH] Fixes for multi-obj LRA --- .../pcaa/StandardPcaaWeightVectorChecker.cpp | 9 +++++++-- src/storm/transformer/MemoryIncorporation.cpp | 2 +- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp index a22e3b42a..f4629a325 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp @@ -117,7 +117,7 @@ namespace storm { for (auto objIndex : lraObjectives) { ValueType weight = storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType()) ? -weightVector[objIndex] : weightVector[objIndex]; storm::utility::vector::addScaledVector(weightedRewardVector, actionRewards[objIndex], weight); - if (!stateRewards[objIndex].empty()) { + if (!stateRewards.empty() && !stateRewards[objIndex].empty()) { weightedStateRewardVector->resize(transitionMatrix.getRowGroupCount(), storm::utility::zero()); storm::utility::vector::addScaledVector(weightedStateRewardVector.get(), stateRewards[objIndex], weight); } @@ -332,6 +332,11 @@ namespace storm { auto const& mec = lraMecDecomposition->mecs[mecIndex]; auto const& mecValue = lraMecDecomposition->auxMecValues[mecIndex]; uint64_t ecqState = ecQuotient->originalToEcqStateMapping[mec.begin()->first]; + if (ecqState >= ecQuotient->matrix.getRowGroupCount()) { + // The mec was not part of the ecquotient. This means that it must have value 0. + // No further processing is needed. + continue; + } uint64_t ecqChoice = ecQuotient->ecqStayInEcChoices.getNextSetIndex(ecQuotient->matrix.getRowGroupIndices()[ecqState]); STORM_LOG_ASSERT(ecqChoice < ecQuotient->matrix.getRowGroupIndices()[ecqState + 1], "Unable to find choice that represents staying inside the (eliminated) ec."); auto& ecqChoiceValue = ecQuotient->auxChoiceValues[ecqChoice]; @@ -413,7 +418,7 @@ namespace storm { if (lraObjectives.get(objIndex)) { auto actionValueGetter = [&] (uint64_t const& a) { return actionRewards[objIndex][transitionMatrix.getRowGroupIndices()[a] + this->optimalChoices[a]]; }; typename storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper::ValueGetter stateValueGetter; - if (stateRewards[objIndex].empty()) { + if (stateRewards.empty() || stateRewards[objIndex].empty()) { stateValueGetter = [] (uint64_t const&) { return storm::utility::zero(); }; } else { stateValueGetter = [&] (uint64_t const& s) { return stateRewards[objIndex][s]; }; diff --git a/src/storm/transformer/MemoryIncorporation.cpp b/src/storm/transformer/MemoryIncorporation.cpp index 36a87e6e8..5879cde50 100644 --- a/src/storm/transformer/MemoryIncorporation.cpp +++ b/src/storm/transformer/MemoryIncorporation.cpp @@ -74,7 +74,7 @@ namespace storm { auto notPhi = std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, subsubFormula.asGloballyFormula().getSubformula().asSharedPointer()); memory = memory.product(getGoalMemory(model, *notPhi)); } else { - STORM_LOG_THROW(subsubFormula.isTotalRewardFormula() || subsubFormula.isCumulativeRewardFormula(), storm::exceptions::NotSupportedException, "The given Formula " << subsubFormula << " is not supported."); + STORM_LOG_THROW(subFormula->isLongRunAverageOperatorFormula() || subsubFormula.isTotalRewardFormula() || subsubFormula.isCumulativeRewardFormula() || subsubFormula.isLongRunAverageRewardFormula(), storm::exceptions::NotSupportedException, "The given Formula " << subsubFormula << " is not supported."); } }