diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp index 33c2301fa..2170ad0f2 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp @@ -46,7 +46,7 @@ namespace storm { void SparseMdpRewardBoundedPcaaWeightVectorChecker::computeEpochSolution(typename MultiDimensionalRewardUnfolding::Epoch const& epoch, std::vector const& weightVector) { auto const& epochModel = rewardUnfolding.setCurrentEpoch(epoch); swEqBuilding.start(); - std::vector::SolutionType> result(epochModel.epochMatrix.getRowGroupCount()); + std::vector::SolutionType> result(epochModel.relevantStates.getNumberOfSetBits()); // Formulate a min-max equation system max(A*x+b)=x for the weighted sum of the objectives @@ -72,14 +72,16 @@ namespace storm { minMaxSolver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize); minMaxSolver->setTrackScheduler(true); //minMaxSolver->setCachingEnabled(true); - std::vector x(result.size(), storm::utility::zero()); + std::vector x(epochModel.epochMatrix.getRowGroupCount(), storm::utility::zero()); swEqBuilding.stop(); swMinMaxSolving.start(); minMaxSolver->solveEquations(x, b); swMinMaxSolving.stop(); swEqBuilding.start(); - for (uint64_t state = 0; state < x.size(); ++state) { - result[state].weightedValue = x[state]; + auto resultIt = result.begin(); + for (auto const& state : epochModel.relevantStates) { + resultIt->weightedValue = x[state]; + ++resultIt; } // Formulate for each objective the linear equation system induced by the performed choices @@ -109,8 +111,10 @@ namespace storm { linEqSolver->solveEquations(x, b); swLinEqSolving.stop(); swEqBuilding.start(); - for (uint64_t state = 0; state < choices.size(); ++state) { - result[state].objectiveValues.push_back(x[state]); + auto resultIt = result.begin(); + for (auto const& state : epochModel.relevantStates) { + resultIt->objectiveValues.push_back(x[state]); + ++resultIt; } } swEqBuilding.stop(); diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp index beb26b600..b80727dfb 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp @@ -377,12 +377,12 @@ namespace storm { } template - void MultiDimensionalRewardUnfolding::setSolutionForCurrentEpoch(std::vector const& reducedModelStateSolutions) { + void MultiDimensionalRewardUnfolding::setSolutionForCurrentEpoch(std::vector const& relevantStateSolutions) { swInsertSol.start(); for (uint64_t productState = 0; productState < memoryProduct.getProduct().getNumberOfStates(); ++productState) { uint64_t reducedModelState = ecElimResult.oldToNewStateMapping[productState]; - if (reducedModelState < reducedModelStateSolutions.size()) { - setSolutionForCurrentEpoch(productState, reducedModelStateSolutions[reducedModelState]); + if (reducedModelState < epochModel.epochMatrix.getRowGroupCount() && epochModel.relevantStates.get(reducedModelState)) { + setSolutionForCurrentEpoch(productState, relevantStateSolutions[epochModel.relevantStates.getNumberOfSetBitsBeforeIndex(reducedModelState)]); } } swInsertSol.stop(); diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h index 97c0d3a52..8e864c21f 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h @@ -70,7 +70,7 @@ namespace storm { EpochModel const& setCurrentEpoch(Epoch const& epoch); - void setSolutionForCurrentEpoch(std::vector const& reducedModelStateSolutions); + void setSolutionForCurrentEpoch(std::vector const& relevantStateSolutions); SolutionType const& getInitialStateResult(Epoch const& epoch);