diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp index 385c72b1e..3f7063f2d 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp @@ -85,136 +85,200 @@ namespace storm { template void SparseMdpRewardBoundedPcaaWeightVectorChecker::computeEpochSolution(typename MultiDimensionalRewardUnfolding::Epoch const& epoch, std::vector const& weightVector, EpochCheckingData& cachedData) { - auto& epochModel = rewardUnfolding.setCurrentEpoch(epoch); - updateCachedData(epochModel, cachedData, weightVector); - ++numCheckedEpochs; - swEqBuilding.start(); + ++numCheckedEpochs; + swEpochModelBuild.start(); + auto& epochModel = rewardUnfolding.setCurrentEpoch(epoch); + swEpochModelBuild.stop(); + swEpochModelAnalysis.start(); std::vector::SolutionType> result; result.reserve(epochModel.epochInStates.getNumberOfSetBits()); uint64_t solutionSize = this->objectives.size() + 1; - - // Formulate a min-max equation system max(A*x+b)=x for the weighted sum of the objectives - swAux1.start(); - assert(cachedData.bMinMax.capacity() >= epochModel.epochMatrix.getRowCount()); - assert(cachedData.xMinMax.size() == epochModel.epochMatrix.getRowGroupCount()); - cachedData.bMinMax.assign(epochModel.epochMatrix.getRowCount(), storm::utility::zero()); - for (uint64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { - ValueType weight = storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType()) ? -weightVector[objIndex] : weightVector[objIndex]; - if (!storm::utility::isZero(weight)) { - std::vector const& objectiveReward = epochModel.objectiveRewards[objIndex]; - for (auto const& choice : epochModel.objectiveRewardFilter[objIndex]) { - cachedData.bMinMax[choice] += weight * objectiveReward[choice]; + + // If the epoch matrix is empty we do not need to solve linear equation systems + if (epochModel.epochMatrix.getEntryCount() == 0) { + std::vector weights = weightVector; + for (uint64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { + if (storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType())) { + weights[objIndex] *= -storm::utility::one(); } } - } - auto stepSolutionIt = epochModel.stepSolutions.begin(); - for (auto const& choice : epochModel.stepChoices) { - cachedData.bMinMax[choice] += stepSolutionIt->front(); - ++stepSolutionIt; - } - swAux1.stop(); - - // Invoke the min max solver - swEqBuilding.stop(); - swMinMaxSolving.start(); - cachedData.minMaxSolver->solveEquations(cachedData.xMinMax, cachedData.bMinMax); - swMinMaxSolving.stop(); - swEqBuilding.start(); - for (auto const& state : epochModel.epochInStates) { - result.emplace_back(); - result.back().reserve(solutionSize); - result.back().push_back(cachedData.xMinMax[state]); - } - - // Check whether the linear equation solver needs to be updated - auto const& choices = cachedData.minMaxSolver->getSchedulerChoices(); - if (cachedData.schedulerChoices != choices) { - std::vector choicesTmp = choices; - cachedData.minMaxSolver->setInitialScheduler(std::move(choicesTmp)); - swAux2.start(); - ++numSchedChanges; - cachedData.schedulerChoices = choices; - storm::solver::GeneralLinearEquationSolverFactory linEqSolverFactory; - bool needEquationSystem = linEqSolverFactory.getEquationProblemFormat() == storm::solver::LinearEquationSolverProblemFormat::EquationSystem; - storm::storage::SparseMatrix subMatrix = epochModel.epochMatrix.selectRowsFromRowGroups(choices, needEquationSystem); - if (needEquationSystem) { - subMatrix.convertToEquationSystem(); - } - cachedData.linEqSolver = linEqSolverFactory.create(std::move(subMatrix)); - cachedData.linEqSolver->setCachingEnabled(true); - swAux2.stop(); - } - - // Formulate for each objective the linear equation system induced by the performed choices - swAux3.start(); - assert(cachedData.bLinEq.size() == choices.size()); - for (uint64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { - auto const& obj = this->objectives[objIndex]; - std::vector const& objectiveReward = epochModel.objectiveRewards[objIndex]; - auto rowGroupIndexIt = epochModel.epochMatrix.getRowGroupIndices().begin(); - auto choiceIt = choices.begin(); - auto stepChoiceIt = epochModel.stepChoices.begin(); + auto stepSolutionIt = epochModel.stepSolutions.begin(); - std::vector& x = cachedData.xLinEq[objIndex]; - auto xIt = x.begin(); - for (auto& b_i : cachedData.bLinEq) { - uint64_t i = *rowGroupIndexIt + *choiceIt; - if (epochModel.objectiveRewardFilter[objIndex].get(i)) { - b_i = objectiveReward[i]; - } else { - b_i = storm::utility::zero(); - } - while (*stepChoiceIt < i) { - ++stepChoiceIt; - ++stepSolutionIt; - } - if (i == *stepChoiceIt) { - b_i += (*stepSolutionIt)[objIndex + 1]; - ++stepChoiceIt; - ++stepSolutionIt; + auto stepChoiceIt = epochModel.stepChoices.begin(); + for (auto const& state : epochModel.epochInStates) { + // Obtain the best choice for this state according to the weighted combination of objectives + ValueType bestValue; + uint64_t bestChoice = std::numeric_limits::max(); + auto bestChoiceStepSolutionIt = epochModel.stepSolutions.end(); + uint64_t lastChoice = epochModel.epochMatrix.getRowGroupIndices()[state + 1]; + bool firstChoice = true; + for (uint64_t choice = epochModel.epochMatrix.getRowGroupIndices()[state]; choice < lastChoice; ++choice) { + ValueType choiceValue = storm::utility::zero(); + // Obtain the (weighted) objective rewards + for (uint64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { + if (epochModel.objectiveRewardFilter[objIndex].get(choice)) { + choiceValue += weights[objIndex] * epochModel.objectiveRewards[objIndex][choice]; + } + } + + // Obtain the step solution if this is a step choice + while (*stepChoiceIt < choice) { + ++stepChoiceIt; + ++stepSolutionIt; + } + if (*stepChoiceIt == choice) { + choiceValue += stepSolutionIt->front(); + // Check if this choice is better + if (firstChoice || choiceValue > bestValue) { + bestValue = std::move(choiceValue); + bestChoice = choice; + bestChoiceStepSolutionIt = stepSolutionIt; + } + } else if (firstChoice || choiceValue > bestValue) { + bestValue = std::move(choiceValue); + bestChoice = choice; + bestChoiceStepSolutionIt = epochModel.stepSolutions.end(); + } + firstChoice = false; } - // We can already set x_i correctly if row i is empty. - // Appearingly, some linear equation solvers struggle to converge otherwise. - if (epochModel.epochMatrix.getRow(i).getNumberOfEntries() == 0) { - *xIt = b_i; + + // Insert the solution w.r.t. this choice + result.emplace_back(); + result.back().reserve(solutionSize); + result.back().push_back(std::move(bestValue)); + + if (bestChoiceStepSolutionIt != epochModel.stepSolutions.end()) { + for (uint64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { + if (epochModel.objectiveRewardFilter[objIndex].get(bestChoice)) { + result.back().push_back((epochModel.objectiveRewards[objIndex][bestChoice] + (*bestChoiceStepSolutionIt)[objIndex + 1])); + } else { + result.back().push_back((*bestChoiceStepSolutionIt)[objIndex + 1]); + } + } + } else { + for (uint64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { + if (epochModel.objectiveRewardFilter[objIndex].get(bestChoice)) { + result.back().push_back((epochModel.objectiveRewards[objIndex][bestChoice])); + } else { + result.back().push_back(storm::utility::zero()); + } + } } - ++xIt; - ++rowGroupIndexIt; - ++choiceIt; } - assert(x.size() == choices.size()); - auto req = cachedData.linEqSolver->getRequirements(); - cachedData.linEqSolver->clearBounds(); - if (obj.lowerResultBound) { - req.clearLowerBounds(); - cachedData.linEqSolver->setLowerBound(*obj.lowerResultBound); + } else { + + + updateCachedData(epochModel, cachedData, weightVector); + + + // Formulate a min-max equation system max(A*x+b)=x for the weighted sum of the objectives + assert(cachedData.bMinMax.capacity() >= epochModel.epochMatrix.getRowCount()); + assert(cachedData.xMinMax.size() == epochModel.epochMatrix.getRowGroupCount()); + cachedData.bMinMax.assign(epochModel.epochMatrix.getRowCount(), storm::utility::zero()); + for (uint64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { + ValueType weight = storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType()) ? -weightVector[objIndex] : weightVector[objIndex]; + if (!storm::utility::isZero(weight)) { + std::vector const& objectiveReward = epochModel.objectiveRewards[objIndex]; + for (auto const& choice : epochModel.objectiveRewardFilter[objIndex]) { + cachedData.bMinMax[choice] += weight * objectiveReward[choice]; + } + } } - if (obj.upperResultBound) { - cachedData.linEqSolver->setUpperBound(*obj.upperResultBound); - req.clearUpperBounds(); + auto stepSolutionIt = epochModel.stepSolutions.begin(); + for (auto const& choice : epochModel.stepChoices) { + cachedData.bMinMax[choice] += stepSolutionIt->front(); + ++stepSolutionIt; } - STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement of the LinearEquationSolver was not met."); - swEqBuilding.stop(); - swLinEqSolving.start(); - cachedData.linEqSolver->solveEquations(x, cachedData.bLinEq); - swLinEqSolving.stop(); - swEqBuilding.start(); - auto resultIt = result.begin(); + + // Invoke the min max solver + cachedData.minMaxSolver->solveEquations(cachedData.xMinMax, cachedData.bMinMax); for (auto const& state : epochModel.epochInStates) { - resultIt->push_back(x[state]); - ++resultIt; + result.emplace_back(); + result.back().reserve(solutionSize); + result.back().push_back(cachedData.xMinMax[state]); + } + + // Check whether the linear equation solver needs to be updated + auto const& choices = cachedData.minMaxSolver->getSchedulerChoices(); + if (cachedData.schedulerChoices != choices) { + std::vector choicesTmp = choices; + cachedData.minMaxSolver->setInitialScheduler(std::move(choicesTmp)); + ++numSchedChanges; + cachedData.schedulerChoices = choices; + storm::solver::GeneralLinearEquationSolverFactory linEqSolverFactory; + bool needEquationSystem = linEqSolverFactory.getEquationProblemFormat() == storm::solver::LinearEquationSolverProblemFormat::EquationSystem; + storm::storage::SparseMatrix subMatrix = epochModel.epochMatrix.selectRowsFromRowGroups(choices, needEquationSystem); + if (needEquationSystem) { + subMatrix.convertToEquationSystem(); + } + cachedData.linEqSolver = linEqSolverFactory.create(std::move(subMatrix)); + cachedData.linEqSolver->setCachingEnabled(true); + } + + // Formulate for each objective the linear equation system induced by the performed choices + assert(cachedData.bLinEq.size() == choices.size()); + for (uint64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { + auto const& obj = this->objectives[objIndex]; + std::vector const& objectiveReward = epochModel.objectiveRewards[objIndex]; + auto rowGroupIndexIt = epochModel.epochMatrix.getRowGroupIndices().begin(); + auto choiceIt = choices.begin(); + auto stepChoiceIt = epochModel.stepChoices.begin(); + auto stepSolutionIt = epochModel.stepSolutions.begin(); + std::vector& x = cachedData.xLinEq[objIndex]; + auto xIt = x.begin(); + for (auto& b_i : cachedData.bLinEq) { + uint64_t i = *rowGroupIndexIt + *choiceIt; + if (epochModel.objectiveRewardFilter[objIndex].get(i)) { + b_i = objectiveReward[i]; + } else { + b_i = storm::utility::zero(); + } + while (*stepChoiceIt < i) { + ++stepChoiceIt; + ++stepSolutionIt; + } + if (i == *stepChoiceIt) { + b_i += (*stepSolutionIt)[objIndex + 1]; + ++stepChoiceIt; + ++stepSolutionIt; + } + // We can already set x_i correctly if row i is empty. + // Appearingly, some linear equation solvers struggle to converge otherwise. + if (epochModel.epochMatrix.getRow(i).getNumberOfEntries() == 0) { + *xIt = b_i; + } + ++xIt; + ++rowGroupIndexIt; + ++choiceIt; + } + assert(x.size() == choices.size()); + auto req = cachedData.linEqSolver->getRequirements(); + cachedData.linEqSolver->clearBounds(); + if (obj.lowerResultBound) { + req.clearLowerBounds(); + cachedData.linEqSolver->setLowerBound(*obj.lowerResultBound); + } + if (obj.upperResultBound) { + cachedData.linEqSolver->setUpperBound(*obj.upperResultBound); + req.clearUpperBounds(); + } + STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement of the LinearEquationSolver was not met."); + cachedData.linEqSolver->solveEquations(x, cachedData.bLinEq); + auto resultIt = result.begin(); + for (auto const& state : epochModel.epochInStates) { + resultIt->push_back(x[state]); + ++resultIt; + } } } - swEqBuilding.stop(); - swAux3.stop(); rewardUnfolding.setSolutionForCurrentEpoch(std::move(result)); + swEpochModelAnalysis.stop(); } template void SparseMdpRewardBoundedPcaaWeightVectorChecker::updateCachedData(typename MultiDimensionalRewardUnfolding::EpochModel const& epochModel, EpochCheckingData& cachedData, std::vector const& weightVector) { if (epochModel.epochMatrixChanged) { - swDataUpdate.start(); // Update the cached MinMaxSolver data cachedData.bMinMax.resize(epochModel.epochMatrix.getRowCount()); @@ -249,7 +313,6 @@ namespace storm { for (auto& x_o : cachedData.xLinEq) { x_o.assign(epochModel.epochMatrix.getRowGroupCount(), storm::utility::zero()); } - swDataUpdate.stop(); } } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h index 836aafce6..77a4d89b8 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h @@ -30,17 +30,13 @@ namespace storm { virtual ~SparseMdpRewardBoundedPcaaWeightVectorChecker() { swAll.stop(); std::cout << "WVC statistics: " << std::endl; - std::cout << " overall: " << swAll << " seconds." << std::endl; + std::cout << " overall Time: " << swAll << " seconds." << std::endl; std::cout << "---------------------------------------------" << std::endl; - std::cout << " Sched changed " << numSchedChanges << "/" << numCheckedEpochs << " times." << std::endl; - std::cout << " dataUpdate: " << swDataUpdate << " seconds." << std::endl; - std::cout << " eqSysBuilding: " << swEqBuilding << " seconds." << std::endl; - std::cout << " MinMaxSolving: " << swMinMaxSolving << " seconds." << std::endl; - std::cout << " LinEqSolving: " << swLinEqSolving << " seconds." << std::endl; - std::cout << " Aux1StopWatch: " << swAux1 << " seconds." << std::endl; - std::cout << " Aux2StopWatch: " << swAux2 << " seconds." << std::endl; - std::cout << " Aux3StopWatch: " << swAux3 << " seconds." << std::endl; - + std::cout << " #checked weight vectors:" << numChecks << "." << std::endl; + std::cout << " #checked epochs:" << numCheckedEpochs << "." << std::endl; + std::cout << "#Sched reused from prev. ep.: " << (numCheckedEpochs - numSchedChanges) << "." << std::endl; + std::cout << " Epoch Model building time: " << swEpochModelBuild << " seconds." << std::endl; + std::cout << " Epoch Model checking time: " << swEpochModelAnalysis << " seconds." << std::endl; } @@ -81,7 +77,7 @@ namespace storm { void updateCachedData(typename MultiDimensionalRewardUnfolding::EpochModel const& epochModel, EpochCheckingData& cachedData, std::vector const& weightVector); - storm::utility::Stopwatch swAll, swDataUpdate, swEqBuilding, swLinEqSolving, swMinMaxSolving, swAux1, swAux2, swAux3; + storm::utility::Stopwatch swAll, swEpochModelBuild, swEpochModelAnalysis; uint64_t numSchedChanges, numCheckedEpochs, numChecks; MultiDimensionalRewardUnfolding rewardUnfolding; diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp index 248d1ee8b..ad680f154 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp @@ -58,12 +58,10 @@ namespace storm { maxSolutionsStored = 0; - swInit.start(); STORM_LOG_ASSERT(!SingleObjectiveMode || (this->objectives.size() == 1), "Enabled single objective mode but there are multiple objectives."); std::vector epochSteps; initializeObjectives(epochSteps); initializeMemoryProduct(epochSteps); - swInit.stop(); } template @@ -291,7 +289,6 @@ namespace storm { epochModel.epochMatrixChanged = false; } - swSetEpoch.start(); bool containsLowerBoundedObjective = false; for (auto const& dimension : dimensions) { if (!dimension.isUpperBounded) { @@ -364,7 +361,6 @@ namespace storm { assert(epochModel.stepChoices.getNumberOfSetBits() == epochModel.stepSolutions.size()); currentEpoch = epoch; - swSetEpoch.stop(); /* std::cout << "Epoch model for epoch " << storm::utility::vector::toString(epoch) << std::endl; std::cout << "Matrix: " << std::endl << epochModel.epochMatrix << std::endl; @@ -384,7 +380,6 @@ namespace storm { void MultiDimensionalRewardUnfolding::setCurrentEpochClass(Epoch const& epoch) { EpochClass epochClass = epochManager.getEpochClass(epoch); // std::cout << "Setting epoch class for epoch " << epochManager.toString(epoch) << std::endl; - swSetEpochClass.start(); auto productObjectiveRewards = productModel->computeObjectiveRewards(epochClass, objectives); storm::storage::BitVector stepChoices(productModel->getProduct().getNumberOfChoices(), false); @@ -455,34 +450,25 @@ namespace storm { epochModel.objectiveRewards.push_back(std::move(reducedModelObjRewards)); } - swAux4.start(); - swAux1.start(); epochModel.epochInStates = storm::storage::BitVector(epochModel.epochMatrix.getRowGroupCount(), false); for (auto const& productState : productInStates) { STORM_LOG_ASSERT(ecElimResult.oldToNewStateMapping[productState] < epochModel.epochMatrix.getRowGroupCount(), "Selected product state does not exist in the epoch model."); epochModel.epochInStates.set(ecElimResult.oldToNewStateMapping[productState], true); } - swAux1.stop(); - swAux2.start(); std::vector toEpochModelInStatesMap(productModel->getProduct().getNumberOfStates(), std::numeric_limits::max()); std::vector epochModelStateToInStateMap = epochModel.epochInStates.getNumberOfSetBitsBeforeIndices(); for (auto const& productState : productInStates) { toEpochModelInStatesMap[productState] = epochModelStateToInStateMap[ecElimResult.oldToNewStateMapping[productState]]; } productStateToEpochModelInStateMap = std::make_shared const>(std::move(toEpochModelInStatesMap)); - swAux2.stop(); - swAux3.start(); epochModel.objectiveRewardFilter.clear(); for (auto const& objRewards : epochModel.objectiveRewards) { epochModel.objectiveRewardFilter.push_back(storm::utility::vector::filterZero(objRewards)); epochModel.objectiveRewardFilter.back().complement(); } - swAux3.stop(); - swAux4.stop(); - swSetEpochClass.stop(); epochModelSizes.push_back(epochModel.epochMatrix.getRowGroupCount()); } @@ -544,7 +530,6 @@ namespace storm { template void MultiDimensionalRewardUnfolding::setSolutionForCurrentEpoch(std::vector&& inStateSolutions) { - swInsertSol.start(); STORM_LOG_ASSERT(currentEpoch, "Tried to set a solution for the current epoch, but no epoch was specified before."); STORM_LOG_ASSERT(inStateSolutions.size() == epochModel.epochInStates.getNumberOfSetBits(), "Invalid number of solutions."); @@ -575,7 +560,6 @@ namespace storm { epochSolutions[currentEpoch.get()] = std::move(solution); maxSolutionsStored = std::max((uint64_t) epochSolutions.size(), maxSolutionsStored); - swInsertSol.stop(); } diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h index ea30c7923..a269ab1e9 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h @@ -47,20 +47,10 @@ namespace storm { MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp const& model, std::shared_ptr objectiveFormula); ~MultiDimensionalRewardUnfolding() { - std::cout << "Unfolding statistics: " << std::endl; - std::cout << " init: " << swInit << " seconds." << std::endl; - std::cout << " setEpoch: " << swSetEpoch << " seconds." << std::endl; - std::cout << " setEpochClass: " << swSetEpochClass << " seconds." << std::endl; - std::cout << " findSolutions: " << swFindSol << " seconds." << std::endl; - std::cout << " insertSolutions: " << swInsertSol << " seconds." << std::endl; - std::cout << " aux1StopWatch: " << swAux1 << " seconds." << std::endl; - std::cout << " aux2StopWatch: " << swAux2 << " seconds." << std::endl; - std::cout << " aux3StopWatch: " << swAux3 << " seconds." << std::endl; - std::cout << " aux4StopWatch: " << swAux4 << " seconds." << std::endl; - std::cout << "---------------------------------------------" << std::endl; - std::cout << " Product size: " << productModel->getProduct().getNumberOfStates() << std::endl; - std::cout << "maxSolutionsStored: " << maxSolutionsStored << std::endl; - std::cout << " Epoch model sizes: "; + std::cout << "Implicit unfolding statistics: " << std::endl; + std::cout << " Memory Product size: " << productModel->getProduct().getNumberOfStates() << std::endl; + std::cout << " maxSolutionsStored: " << maxSolutionsStored << std::endl; + std::cout << "Occurring Epoch model sizes: "; for (auto const& i : epochModelSizes) { std::cout << i << " "; }