From 9735ff98d02315cc9a338ad36054cb2f5b94d397 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 7 Sep 2017 11:38:09 +0200 Subject: [PATCH] SolutionType is now a single vector instead of a struct --- ...seMdpRewardBoundedPcaaWeightVectorChecker.cpp | 16 ++++++++++------ .../MultiDimensionalRewardUnfolding.cpp | 15 +++++++-------- .../MultiDimensionalRewardUnfolding.h | 7 +------ 3 files changed, 18 insertions(+), 20 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp index a1784bea8..89065d57b 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp @@ -37,8 +37,10 @@ namespace storm { auto solution = rewardUnfolding.getInitialStateResult(initEpoch); // Todo: we currently assume precise results... - underApproxResult = solution.objectiveValues; - overApproxResult = solution.objectiveValues; + auto solutionIt = solution.begin(); + ++solutionIt; + underApproxResult = std::vector(solutionIt, solution.end()); + overApproxResult = underApproxResult; } @@ -62,7 +64,7 @@ namespace storm { } auto stepSolutionIt = epochModel.stepSolutions.begin(); for (auto const& choice : epochModel.stepChoices) { - b[choice] += stepSolutionIt->weightedValue; + b[choice] += stepSolutionIt->front(); ++stepSolutionIt; } @@ -79,8 +81,10 @@ namespace storm { swMinMaxSolving.stop(); swEqBuilding.start(); auto resultIt = result.begin(); + uint64_t solSize = this->objectives.size() + 1; for (auto const& state : epochModel.inStates) { - resultIt->weightedValue = x[state]; + resultIt->reserve(solSize); + resultIt->push_back(x[state]); ++resultIt; } @@ -103,7 +107,7 @@ namespace storm { b[state] = storm::utility::zero(); } if (epochModel.stepChoices.get(choice)) { - b[state] += epochModel.stepSolutions[epochModel.stepChoices.getNumberOfSetBitsBeforeIndex(choice)].objectiveValues[objIndex]; + b[state] += epochModel.stepSolutions[epochModel.stepChoices.getNumberOfSetBitsBeforeIndex(choice)][objIndex + 1]; } } swEqBuilding.stop(); @@ -113,7 +117,7 @@ namespace storm { swEqBuilding.start(); auto resultIt = result.begin(); for (auto const& state : epochModel.inStates) { - resultIt->objectiveValues.push_back(x[state]); + resultIt->push_back(x[state]); ++resultIt; } } diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp index 629c73a6f..e83cd02cc 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp @@ -28,6 +28,7 @@ namespace storm { template void MultiDimensionalRewardUnfolding::initialize() { swInit.start(); + STORM_LOG_ASSERT(!SingleObjectiveMode || (this->objectives.size() == 1), "Enabled single objective mode but there are multiple objectives."); std::vector> epochSteps; initializeObjectives(epochSteps); initializePossibleEpochSteps(epochSteps); @@ -415,17 +416,16 @@ namespace storm { template template::type> typename MultiDimensionalRewardUnfolding::SolutionType MultiDimensionalRewardUnfolding::getScaledSolution(SolutionType const& solution, ValueType const& scalingFactor) const { - //return solution * scalingFactor; + return solution * scalingFactor; } template template::type> typename MultiDimensionalRewardUnfolding::SolutionType MultiDimensionalRewardUnfolding::getScaledSolution(SolutionType const& solution, ValueType const& scalingFactor) const { SolutionType res; - res.weightedValue = solution.weightedValue * scalingFactor; - res.objectiveValues.reserve(solution.objectiveValues.size()); - for (auto const& sol : solution.objectiveValues) { - res.objectiveValues.push_back(sol * scalingFactor); + res.reserve(solution.size()); + for (auto const& sol : solution) { + res.push_back(sol * scalingFactor); } return res; } @@ -433,14 +433,13 @@ namespace storm { template template::type> void MultiDimensionalRewardUnfolding::addScaledSolution(SolutionType& solution, SolutionType const& solutionToAdd, ValueType const& scalingFactor) const { - // solution += solutionToAdd * scalingFactor; + solution += solutionToAdd * scalingFactor; } template template::type> void MultiDimensionalRewardUnfolding::addScaledSolution(SolutionType& solution, SolutionType const& solutionToAdd, ValueType const& scalingFactor) const { - solution.weightedValue += solutionToAdd.weightedValue * scalingFactor; - storm::utility::vector::addScaledVector(solution.objectiveValues, solutionToAdd.objectiveValues, scalingFactor); + storm::utility::vector::addScaledVector(solution, solutionToAdd, scalingFactor); } template diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h index 1b003d703..a591316c8 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h @@ -25,12 +25,7 @@ namespace storm { typedef std::vector Epoch; // The number of reward steps that are "left" for each dimension typedef uint64_t EpochClass; // Collection of epochs that consider the same epoch model -// typedef typename std::conditional>::type; SolutionType - - struct SolutionType { - ValueType weightedValue; - std::vector objectiveValues; - }; + typedef typename std::conditional>::type SolutionType; struct EpochModel { storm::storage::SparseMatrix epochMatrix;