diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp index 2fa1ac2fe..b0a703660 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp @@ -49,17 +49,7 @@ namespace storm { auto initEpoch = rewardUnfolding.getStartEpoch(); auto epochOrder = rewardUnfolding.getEpochComputationOrder(initEpoch); EpochCheckingData cachedData; - ValueType precision = storm::utility::convertNumber(storm::settings::getModule().getPrecision()); - uint64_t epochCount = 0; - for (uint64_t dim = 0; dim < rewardUnfolding.getEpochManager().getDimensionCount(); ++dim) { - epochCount += rewardUnfolding.getEpochManager().getDimensionOfEpoch(initEpoch, dim) + 1; - } - if (storm::settings::getModule().isSoundSet()) { - precision = precision / storm::utility::convertNumber(epochCount); - } - if (numChecks == 1) { - STORM_PRINT_AND_LOG("Objective/Dimension/Epoch count is: " << this->objectives.size() << "/" << rewardUnfolding.getEpochManager().getDimensionCount() << "/" << epochOrder.size() << "." << std::endl); - } + ValueType precision = rewardUnfolding.getRequiredEpochModelPrecision(initEpoch, storm::utility::convertNumber(storm::settings::getModule().getPrecision())); storm::utility::ProgressMeasurement progress("epochs"); progress.setMaxCount(epochOrder.size()); diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp index fd86fecb4..6379b08b6 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp @@ -537,6 +537,16 @@ namespace storm { return stringstream.str(); } + template + ValueType MultiDimensionalRewardUnfolding::getRequiredEpochModelPrecision(Epoch const& startEpoch, ValueType const& precision) { + // if (storm::settings::getModule().isSoundSet()) { + uint64_t sumOfDimensions = 0; + for (uint64_t dim = 0; dim < epochManager.getDimensionCount(); ++dim) { + sumOfDimensions += epochManager.getDimensionOfEpoch(startEpoch, dim) + 1; + } + return precision / storm::utility::convertNumber(sumOfDimensions); + } + template void MultiDimensionalRewardUnfolding::setSolutionForCurrentEpoch(std::vector&& inStateSolutions) { STORM_LOG_ASSERT(currentEpoch, "Tried to set a solution for the current epoch, but no epoch was specified before."); diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h index 28c25747e..3486515d2 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h @@ -46,25 +46,18 @@ namespace storm { MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp const& model, std::vector> const& objectives); MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp const& model, std::shared_ptr objectiveFormula); - ~MultiDimensionalRewardUnfolding() { - 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 << " "; - } - std::cout << std::endl; - std::cout << "---------------------------------------------" << std::endl; - std::cout << std::endl; - - } + ~MultiDimensionalRewardUnfolding() = default; Epoch getStartEpoch(); std::vector getEpochComputationOrder(Epoch const& startEpoch); EpochModel& setCurrentEpoch(Epoch const& epoch); + /*! + * Returns the precision required for the analyzis of each epoch model in order to achieve the given overall precision + */ + ValueType getRequiredEpochModelPrecision(Epoch const& startEpoch, ValueType const& precision); + void setSolutionForCurrentEpoch(std::vector&& inStateSolutions); SolutionType const& getInitialStateResult(Epoch const& epoch); // Assumes that the initial state is unique SolutionType const& getInitialStateResult(Epoch const& epoch, uint64_t initialStateIndex); @@ -79,7 +72,6 @@ namespace storm { void initializeObjectives(std::vector& epochSteps); void computeMaxDimensionValues(); - void initializeMemoryProduct(std::vector const& epochSteps); diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 0d708ee06..0b687b97f 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -82,6 +82,105 @@ namespace storm { return result; } + + template + std::vector analyzeTrivialEpochModel(OptimizationDirection dir, typename storm::modelchecker::multiobjective::MultiDimensionalRewardUnfolding::EpochModel& epochModel) { + // Assert that the epoch model is indeed trivial + assert(epochModel.epochMatrix.getEntryCount() == 0); + + std::vector epochResult; + epochResult.reserve(epochModel.epochInStates.getNumberOfSetBits()); + + auto stepSolutionIt = epochModel.stepSolutions.begin(); + auto stepChoiceIt = epochModel.stepChoices.begin(); + for (auto const& state : epochModel.epochInStates) { + // Obtain the best choice for this state + ValueType bestValue; + uint64_t lastChoice = epochModel.epochMatrix.getRowGroupIndices()[state + 1]; + bool isFirstChoice = true; + for (uint64_t choice = epochModel.epochMatrix.getRowGroupIndices()[state]; choice < lastChoice; ++choice) { + while (*stepChoiceIt < choice) { + ++stepChoiceIt; + ++stepSolutionIt; + } + + ValueType choiceValue = storm::utility::zero(); + if (epochModel.objectiveRewardFilter.front().get(choice)) { + choiceValue += epochModel.objectiveRewards.front()[choice]; + } + if (*stepChoiceIt == choice) { + choiceValue += *stepSolutionIt; + } + + if (isFirstChoice) { + bestValue = std::move(choiceValue); + isFirstChoice = false; + } else { + if (storm::solver::minimize(dir)) { + if (choiceValue < bestValue) { + bestValue = std::move(choiceValue); + } + } else { + if (choiceValue > bestValue) { + bestValue = std::move(choiceValue); + } + } + } + } + // Insert the solution w.r.t. this choice + epochResult.push_back(std::move(bestValue)); + } + return epochResult; + } + + template + std::vector analyzeNonTrivialEpochModel(OptimizationDirection dir, typename storm::modelchecker::multiobjective::MultiDimensionalRewardUnfolding::EpochModel& epochModel, std::vector& x, std::vector& b, std::unique_ptr>& minMaxSolver, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ValueType const& precision, SolutionType const& type) { + + // Update some data for the case that the Matrix has changed + if (epochModel.epochMatrixChanged) { + x.assign(epochModel.epochMatrix.getRowGroupCount(), storm::utility::zero()); + minMaxSolver = minMaxLinearEquationSolverFactory.create(epochModel.epochMatrix); + minMaxSolver->setHasUniqueSolution(); + minMaxSolver->setPrecision(precision); + minMaxSolver->setOptimizationDirection(dir); + minMaxSolver->setCachingEnabled(true); + minMaxSolver->setTrackScheduler(true); + auto req = minMaxSolver->getRequirements(dir); + minMaxSolver->setLowerBound(storm::utility::zero()); + req.clearLowerBounds(); + if (type == SolutionType::UntilProbabilities) { + minMaxSolver->setUpperBound(storm::utility::one()); + req.clearUpperBounds(); + } else if (type == SolutionType::ExpectedRewards) { + // TODO + STORM_LOG_WARN_COND(!req.requiresUpperBounds(), "Upper bounds for expected reward are not specified."); + } + STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement was not checked."); + minMaxSolver->setRequirementsChecked(); + } else { + auto choicesTmp = minMaxSolver->getSchedulerChoices(); + minMaxSolver->setInitialScheduler(std::move(choicesTmp)); + } + + // Prepare the right hand side of the equation system + b.assign(epochModel.epochMatrix.getRowCount(), storm::utility::zero()); + std::vector const& objectiveValues = epochModel.objectiveRewards.front(); + for (auto const& choice : epochModel.objectiveRewardFilter.front()) { + b[choice] = objectiveValues[choice]; + } + auto stepSolutionIt = epochModel.stepSolutions.begin(); + for (auto const& choice : epochModel.stepChoices) { + b[choice] += *stepSolutionIt; + ++stepSolutionIt; + } + assert(stepSolutionIt == epochModel.stepSolutions.end()); + + // Solve the minMax equation system + minMaxSolver->solveEquations(x, b); + + return storm::utility::vector::filterVector(x, epochModel.epochInStates); + } + template std::map SparseMdpPrctlHelper::computeRewardBoundedValues(SolutionType const& type, OptimizationDirection dir, storm::modelchecker::multiobjective::MultiDimensionalRewardUnfolding& rewardUnfolding, storm::storage::BitVector const& initialStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { storm::utility::Stopwatch swAll(true), swBuild, swCheck; @@ -92,14 +191,8 @@ namespace storm { std::vector x, b; std::unique_ptr> minMaxSolver; - ValueType precision = storm::utility::convertNumber(storm::settings::getModule().getPrecision()); - uint64_t epochCount = 0; - for (uint64_t dim = 0; dim < rewardUnfolding.getEpochManager().getDimensionCount(); ++dim) { - epochCount += rewardUnfolding.getEpochManager().getDimensionOfEpoch(initEpoch, dim) + 1; - } - if (storm::settings::getModule().isSoundSet()) { - precision = precision / storm::utility::convertNumber(epochCount); - } + ValueType precision = rewardUnfolding.getRequiredEpochModelPrecision(initEpoch, storm::utility::convertNumber(storm::settings::getModule().getPrecision())); + storm::utility::ProgressMeasurement progress("epochs"); progress.setMaxCount(epochOrder.size()); progress.startNewMeasurement(0); @@ -110,95 +203,9 @@ namespace storm { swBuild.stop(); swCheck.start(); // If the epoch matrix is empty we do not need to solve a linear equation system if (epochModel.epochMatrix.getEntryCount() == 0) { - std::vector epochResult; - epochResult.reserve(epochModel.epochInStates.getNumberOfSetBits()); - - auto stepSolutionIt = epochModel.stepSolutions.begin(); - auto stepChoiceIt = epochModel.stepChoices.begin(); - for (auto const& state : epochModel.epochInStates) { - // Obtain the best choice for this state - ValueType bestValue; - uint64_t lastChoice = epochModel.epochMatrix.getRowGroupIndices()[state + 1]; - bool isFirstChoice = true; - for (uint64_t choice = epochModel.epochMatrix.getRowGroupIndices()[state]; choice < lastChoice; ++choice) { - while (*stepChoiceIt < choice) { - ++stepChoiceIt; - ++stepSolutionIt; - } - - ValueType choiceValue = storm::utility::zero(); - if (epochModel.objectiveRewardFilter.front().get(choice)) { - choiceValue += epochModel.objectiveRewards.front()[choice]; - } - if (*stepChoiceIt == choice) { - choiceValue += *stepSolutionIt; - } - - if (isFirstChoice) { - bestValue = std::move(choiceValue); - isFirstChoice = false; - } else { - if (storm::solver::minimize(dir)) { - if (choiceValue < bestValue) { - bestValue = std::move(choiceValue); - } - } else { - if (choiceValue > bestValue) { - bestValue = std::move(choiceValue); - } - } - } - } - // Insert the solution w.r.t. this choice - epochResult.push_back(std::move(bestValue)); - } - - rewardUnfolding.setSolutionForCurrentEpoch(std::move(epochResult)); + rewardUnfolding.setSolutionForCurrentEpoch(analyzeTrivialEpochModel(dir, epochModel)); } else { - // Update some data for the case that the Matrix has changed - if (epochModel.epochMatrixChanged) { - x.assign(epochModel.epochMatrix.getRowGroupCount(), storm::utility::zero()); - minMaxSolver = minMaxLinearEquationSolverFactory.create(epochModel.epochMatrix); - minMaxSolver->setHasUniqueSolution(); - minMaxSolver->setPrecision(precision); - minMaxSolver->setOptimizationDirection(dir); - minMaxSolver->setCachingEnabled(true); - minMaxSolver->setTrackScheduler(true); - auto req = minMaxSolver->getRequirements(dir); - minMaxSolver->setLowerBound(storm::utility::zero()); - req.clearLowerBounds(); - if (type == SolutionType::UntilProbabilities) { - minMaxSolver->setUpperBound(storm::utility::one()); - req.clearUpperBounds(); - } else if (type == SolutionType::ExpectedRewards) { - // TODO - STORM_LOG_WARN_COND(!req.requiresUpperBounds(), "Upper bounds for expected reward are not specified."); - } - STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement was not checked."); - minMaxSolver->setRequirementsChecked(); - } else { - auto choicesTmp = minMaxSolver->getSchedulerChoices(); - minMaxSolver->setInitialScheduler(std::move(choicesTmp)); - } - - // Prepare the right hand side of the equation system - b.assign(epochModel.epochMatrix.getRowCount(), storm::utility::zero()); - std::vector const& objectiveValues = epochModel.objectiveRewards.front(); - for (auto const& choice : epochModel.objectiveRewardFilter.front()) { - b[choice] = objectiveValues[choice]; - } - auto stepSolutionIt = epochModel.stepSolutions.begin(); - for (auto const& choice : epochModel.stepChoices) { - b[choice] += *stepSolutionIt; - ++stepSolutionIt; - } - assert(stepSolutionIt == epochModel.stepSolutions.end()); - - // Solve the minMax equation system - minMaxSolver->solveEquations(x, b); - - // Plug in the result into the reward unfolding - rewardUnfolding.setSolutionForCurrentEpoch(storm::utility::vector::filterVector(x, epochModel.epochInStates)); + rewardUnfolding.setSolutionForCurrentEpoch(analyzeNonTrivialEpochModel(dir, epochModel, x, b, minMaxSolver, minMaxLinearEquationSolverFactory, precision, type)); } swCheck.stop(); ++numCheckedEpochs;