diff --git a/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp index f5137b0a7..0df580eab 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp @@ -309,7 +309,7 @@ namespace storm { } template - void RewardBoundedMdpPcaaWeightVectorChecker::updateCachedData(Environment const& env, typename helper::rewardbounded::MultiDimensionalRewardUnfolding::EpochModel const& epochModel, EpochCheckingData& cachedData, std::vector const& weightVector) { + void RewardBoundedMdpPcaaWeightVectorChecker::updateCachedData(Environment const& env, helper::rewardbounded::EpochModel const& epochModel, EpochCheckingData& cachedData, std::vector const& weightVector) { if (epochModel.epochMatrixChanged) { // Update the cached MinMaxSolver data diff --git a/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.h index 0013cdc3d..68fd403f0 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.h @@ -64,7 +64,7 @@ namespace storm { void computeEpochSolution(Environment const& env, typename helper::rewardbounded::MultiDimensionalRewardUnfolding::Epoch const& epoch, std::vector const& weightVector, EpochCheckingData& cachedData); - void updateCachedData(Environment const& env, typename helper::rewardbounded::MultiDimensionalRewardUnfolding::EpochModel const& epochModel, EpochCheckingData& cachedData, std::vector const& weightVector); + void updateCachedData(Environment const& env, typename helper::rewardbounded::EpochModel const& epochModel, EpochCheckingData& cachedData, std::vector const& weightVector); storm::utility::Stopwatch swAll, swEpochModelBuild, swEpochModelAnalysis; uint64_t numCheckedEpochs, numChecks; diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 0e5cf1849..28e799691 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -81,75 +81,6 @@ namespace storm { return result; } - template - std::vector analyzeTrivialDtmcEpochModel(typename rewardbounded::MultiDimensionalRewardUnfolding::EpochModel& epochModel) { - - std::vector epochResult; - epochResult.reserve(epochModel.epochInStates.getNumberOfSetBits()); - auto stepSolutionIt = epochModel.stepSolutions.begin(); - auto stepChoiceIt = epochModel.stepChoices.begin(); - for (auto const& state : epochModel.epochInStates) { - while (*stepChoiceIt < state) { - ++stepChoiceIt; - ++stepSolutionIt; - } - if (epochModel.objectiveRewardFilter.front().get(state)) { - if (*stepChoiceIt == state) { - epochResult.push_back(epochModel.objectiveRewards.front()[state] + *stepSolutionIt); - } else { - epochResult.push_back(epochModel.objectiveRewards.front()[state]); - } - } else { - if (*stepChoiceIt == state) { - epochResult.push_back(*stepSolutionIt); - } else { - epochResult.push_back(storm::utility::zero()); - } - } - } - return epochResult; - } - - template - std::vector analyzeNonTrivialDtmcEpochModel(Environment const& env, typename rewardbounded::MultiDimensionalRewardUnfolding::EpochModel& epochModel, std::vector& x, std::vector& b, std::unique_ptr>& linEqSolver, boost::optional const& lowerBound, boost::optional const& upperBound) { - - // Update some data for the case that the Matrix has changed - if (epochModel.epochMatrixChanged) { - x.assign(epochModel.epochMatrix.getRowGroupCount(), storm::utility::zero()); - storm::solver::GeneralLinearEquationSolverFactory linearEquationSolverFactory; - linEqSolver = linearEquationSolverFactory.create(env, epochModel.epochMatrix); - linEqSolver->setCachingEnabled(true); - auto req = linEqSolver->getRequirements(env); - if (lowerBound) { - linEqSolver->setLowerBound(lowerBound.get()); - req.clearLowerBounds(); - } - if (upperBound) { - linEqSolver->setUpperBound(upperBound.get()); - req.clearUpperBounds(); - } - STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked."); - } - - // 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 - linEqSolver->solveEquations(env, x, b); - - return storm::utility::vector::filterVector(x, epochModel.epochInStates); - } - template<> std::map SparseDtmcPrctlHelper::computeRewardBoundedValues(Environment const& env, storm::models::sparse::Dtmc const& model, std::shared_ptr rewardBoundedFormula) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The specified property is not supported by this value type."); @@ -184,8 +115,7 @@ namespace storm { // Set the correct equation problem format. storm::solver::GeneralLinearEquationSolverFactory linearEquationSolverFactory; rewardUnfolding.setEquationSystemFormatForEpochModel(linearEquationSolverFactory.getEquationProblemFormat(preciseEnv)); - bool convertToEquationSystem = linearEquationSolverFactory.getEquationProblemFormat(preciseEnv) == solver::LinearEquationSolverProblemFormat::EquationSystem; - + storm::utility::ProgressMeasurement progress("epochs"); progress.setMaxCount(epochOrder.size()); progress.startNewMeasurement(0); @@ -194,12 +124,7 @@ namespace storm { swBuild.start(); auto& epochModel = rewardUnfolding.setCurrentEpoch(epoch); swBuild.stop(); swCheck.start(); - // If the epoch matrix is empty we do not need to solve a linear equation system - if ((convertToEquationSystem && epochModel.epochMatrix.isIdentityMatrix()) || (!convertToEquationSystem && epochModel.epochMatrix.getEntryCount() == 0)) { - rewardUnfolding.setSolutionForCurrentEpoch(analyzeTrivialDtmcEpochModel(epochModel)); - } else { - rewardUnfolding.setSolutionForCurrentEpoch(analyzeNonTrivialDtmcEpochModel(preciseEnv, epochModel, x, b, linEqSolver, lowerBound, upperBound)); - } + rewardUnfolding.setSolutionForCurrentEpoch(epochModel.analyzeSingleObjective(preciseEnv, x, b, linEqSolver, lowerBound, upperBound)); swCheck.stop(); if (storm::settings::getModule().isExportCdfSet() && !rewardUnfolding.getEpochManager().hasBottomDimension(epoch)) { std::vector cdfEntry; diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 0a0ea992c..b28bcd6f0 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -90,103 +90,7 @@ namespace storm { return result; } - template - std::vector analyzeTrivialMdpEpochModel(OptimizationDirection dir, typename rewardbounded::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 analyzeNonTrivialMdpEpochModel(Environment const& env, OptimizationDirection dir, typename rewardbounded::MultiDimensionalRewardUnfolding::EpochModel& epochModel, std::vector& x, std::vector& b, std::unique_ptr>& minMaxSolver, boost::optional const& lowerBound, boost::optional const& upperBound) { - - // Update some data for the case that the Matrix has changed - if (epochModel.epochMatrixChanged) { - x.assign(epochModel.epochMatrix.getRowGroupCount(), storm::utility::zero()); - storm::solver::GeneralMinMaxLinearEquationSolverFactory minMaxLinearEquationSolverFactory; - minMaxSolver = minMaxLinearEquationSolverFactory.create(env, epochModel.epochMatrix); - minMaxSolver->setHasUniqueSolution(); - minMaxSolver->setOptimizationDirection(dir); - minMaxSolver->setCachingEnabled(true); - minMaxSolver->setTrackScheduler(true); - auto req = minMaxSolver->getRequirements(env, dir, false); - if (lowerBound) { - minMaxSolver->setLowerBound(lowerBound.get()); - req.clearLowerBounds(); - } - if (upperBound) { - minMaxSolver->setUpperBound(upperBound.get()); - req.clearUpperBounds(); - } - STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " 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(env, x, b); - - return storm::utility::vector::filterVector(x, epochModel.epochInStates); - } - + template std::map SparseMdpPrctlHelper::computeRewardBoundedValues(Environment const& env, OptimizationDirection dir, rewardbounded::MultiDimensionalRewardUnfolding& rewardUnfolding, storm::storage::BitVector const& initialStates) { storm::utility::Stopwatch swAll(true), swBuild, swCheck; @@ -218,12 +122,7 @@ namespace storm { swBuild.start(); auto& epochModel = rewardUnfolding.setCurrentEpoch(epoch); 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) { - rewardUnfolding.setSolutionForCurrentEpoch(analyzeTrivialMdpEpochModel(dir, epochModel)); - } else { - rewardUnfolding.setSolutionForCurrentEpoch(analyzeNonTrivialMdpEpochModel(preciseEnv, dir, epochModel, x, b, minMaxSolver, lowerBound, upperBound)); - } + rewardUnfolding.setSolutionForCurrentEpoch(epochModel.analyzeSingleObjective(preciseEnv, dir, x, b, minMaxSolver, lowerBound, upperBound)); swCheck.stop(); if (storm::settings::getModule().isExportCdfSet() && !rewardUnfolding.getEpochManager().hasBottomDimension(epoch)) { std::vector cdfEntry; diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/EpochModel.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/EpochModel.cpp new file mode 100644 index 000000000..37c39e691 --- /dev/null +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/EpochModel.cpp @@ -0,0 +1,248 @@ +#include "storm/modelchecker/prctl/helper/rewardbounded/EpochModel.h" +#include "storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.h" + +#include "storm/exceptions/UncheckedRequirementException.h" + +namespace storm { + namespace modelchecker { + namespace helper { + namespace rewardbounded { + + + + template + std::vector analyzeTrivialDtmcEpochModel(EpochModel& epochModel) { + + std::vector epochResult; + epochResult.reserve(epochModel.epochInStates.getNumberOfSetBits()); + auto stepSolutionIt = epochModel.stepSolutions.begin(); + auto stepChoiceIt = epochModel.stepChoices.begin(); + for (auto const& state : epochModel.epochInStates) { + while (*stepChoiceIt < state) { + ++stepChoiceIt; + ++stepSolutionIt; + } + if (epochModel.objectiveRewardFilter.front().get(state)) { + if (*stepChoiceIt == state) { + epochResult.push_back(epochModel.objectiveRewards.front()[state] + *stepSolutionIt); + } else { + epochResult.push_back(epochModel.objectiveRewards.front()[state]); + } + } else { + if (*stepChoiceIt == state) { + epochResult.push_back(*stepSolutionIt); + } else { + epochResult.push_back(storm::utility::zero()); + } + } + } + return epochResult; + } + + template + std::vector analyzeNonTrivialDtmcEpochModel(Environment const& env, EpochModel& epochModel, std::vector& x, std::vector& b, std::unique_ptr>& linEqSolver, boost::optional const& lowerBound, boost::optional const& upperBound) { + + // Update some data for the case that the Matrix has changed + if (epochModel.epochMatrixChanged) { + x.assign(epochModel.epochMatrix.getRowGroupCount(), storm::utility::zero()); + storm::solver::GeneralLinearEquationSolverFactory linearEquationSolverFactory; + linEqSolver = linearEquationSolverFactory.create(env, epochModel.epochMatrix); + linEqSolver->setCachingEnabled(true); + auto req = linEqSolver->getRequirements(env); + if (lowerBound) { + linEqSolver->setLowerBound(lowerBound.get()); + req.clearLowerBounds(); + } + if (upperBound) { + linEqSolver->setUpperBound(upperBound.get()); + req.clearUpperBounds(); + } + STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked."); + } + + // 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 + linEqSolver->solveEquations(env, x, b); + + return storm::utility::vector::filterVector(x, epochModel.epochInStates); + } + + + + template + std::vector analyzeTrivialMdpEpochModel(OptimizationDirection dir, 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 analyzeNonTrivialMdpEpochModel(Environment const& env, OptimizationDirection dir, EpochModel& epochModel, std::vector& x, std::vector& b, std::unique_ptr>& minMaxSolver, boost::optional const& lowerBound, boost::optional const& upperBound) { + + // Update some data for the case that the Matrix has changed + if (epochModel.epochMatrixChanged) { + x.assign(epochModel.epochMatrix.getRowGroupCount(), storm::utility::zero()); + storm::solver::GeneralMinMaxLinearEquationSolverFactory minMaxLinearEquationSolverFactory; + minMaxSolver = minMaxLinearEquationSolverFactory.create(env, epochModel.epochMatrix); + minMaxSolver->setHasUniqueSolution(); + minMaxSolver->setOptimizationDirection(dir); + minMaxSolver->setCachingEnabled(true); + minMaxSolver->setTrackScheduler(true); + auto req = minMaxSolver->getRequirements(env, dir, false); + if (lowerBound) { + minMaxSolver->setLowerBound(lowerBound.get()); + req.clearLowerBounds(); + } + if (upperBound) { + minMaxSolver->setUpperBound(upperBound.get()); + req.clearUpperBounds(); + } + STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " 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(env, x, b); + + return storm::utility::vector::filterVector(x, epochModel.epochInStates); + } + + template<> + std::vector EpochModel::analyzeSingleObjective( + const storm::Environment &env, std::vector &x, std::vector &b, + std::unique_ptr> &linEqSolver, + const boost::optional &lowerBound, const boost::optional &upperBound) { + STORM_LOG_ASSERT(epochMatrix.hasTrivialRowGrouping(), "This operation is only allowed if no nondeterminism is present."); + STORM_LOG_ASSERT(equationSolverProblemFormat.is_initialized(), "Unknown equation problem format."); + // If the epoch matrix is empty we do not need to solve a linear equation system + bool convertToEquationSystem = (equationSolverProblemFormat == storm::solver::LinearEquationSolverProblemFormat::EquationSystem); + if ((convertToEquationSystem && epochMatrix.isIdentityMatrix()) || (!convertToEquationSystem && epochMatrix.getEntryCount() == 0)) { + return analyzeTrivialDtmcEpochModel(*this); + } else { + return analyzeNonTrivialDtmcEpochModel(env, *this, x, b, linEqSolver, lowerBound, upperBound); + } + } + + template<> + std::vector EpochModel::analyzeSingleObjective( + const storm::Environment &env, storm::OptimizationDirection dir, std::vector &x, + std::vector &b, + std::unique_ptr> &minMaxSolver, + const boost::optional &lowerBound, const boost::optional &upperBound) { + // If the epoch matrix is empty we do not need to solve a linear equation system + if (epochMatrix.getEntryCount() == 0) { + return analyzeTrivialMdpEpochModel(dir, *this); + } else { + return analyzeNonTrivialMdpEpochModel(env, dir, *this, x, b, minMaxSolver, lowerBound, upperBound); + } + } + + template<> + std::vector EpochModel::analyzeSingleObjective( + const storm::Environment &env, std::vector &x, std::vector &b, + std::unique_ptr> &linEqSolver, + const boost::optional &lowerBound, const boost::optional &upperBound) { + STORM_LOG_ASSERT(epochMatrix.hasTrivialRowGrouping(), "This operation is only allowed if no nondeterminism is present."); + STORM_LOG_ASSERT(equationSolverProblemFormat.is_initialized(), "Unknown equation problem format."); + // If the epoch matrix is empty we do not need to solve a linear equation system + bool convertToEquationSystem = (equationSolverProblemFormat == storm::solver::LinearEquationSolverProblemFormat::EquationSystem); + if ((convertToEquationSystem && epochMatrix.isIdentityMatrix()) || (!convertToEquationSystem && epochMatrix.getEntryCount() == 0)) { + return analyzeTrivialDtmcEpochModel(*this); + } else { + return analyzeNonTrivialDtmcEpochModel(env, *this, x, b, linEqSolver, lowerBound, upperBound); + } + } + + template<> + std::vector EpochModel::analyzeSingleObjective( + const storm::Environment &env, storm::OptimizationDirection dir, std::vector &x, + std::vector &b, + std::unique_ptr> &minMaxSolver, + const boost::optional &lowerBound, const boost::optional &upperBound) { + // If the epoch matrix is empty we do not need to solve a linear equation system + if (epochMatrix.getEntryCount() == 0) { + return analyzeTrivialMdpEpochModel(dir, *this); + } else { + return analyzeNonTrivialMdpEpochModel(env, dir, *this, x, b, minMaxSolver, lowerBound, upperBound); + } + } + + template class EpochModel; + template class EpochModel; + template class EpochModel; + template class EpochModel; + } + } + } +} diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/EpochModel.h b/src/storm/modelchecker/prctl/helper/rewardbounded/EpochModel.h new file mode 100644 index 000000000..dae640ff5 --- /dev/null +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/EpochModel.h @@ -0,0 +1,48 @@ +#pragma once + +#include +#include "storm/storage/SparseMatrix.h" +#include "storm/storage/BitVector.h" +#include "storm/solver/LinearEquationSolverProblemFormat.h" +#include "storm/solver/OptimizationDirection.h" +#include "storm/solver/MinMaxLinearEquationSolver.h" +#include "storm/solver/LinearEquationSolver.h" + +namespace storm { + class Environment; + + namespace modelchecker { + namespace helper { + namespace rewardbounded { + template + struct EpochModel { + typedef typename std::conditional>::type SolutionType; + + bool epochMatrixChanged; + storm::storage::SparseMatrix epochMatrix; + storm::storage::BitVector stepChoices; + std::vector stepSolutions; + std::vector> objectiveRewards; + std::vector objectiveRewardFilter; + storm::storage::BitVector epochInStates; + /// In case of DTMCs we have different options for the equation problem format the epoch model will have. + boost::optional equationSolverProblemFormat; + + /*! + * Analyzes the epoch model, i.e., solves the represented equation system. This method assumes a nondeterministic model. + */ + std::vector analyzeSingleObjective(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector& b, std::unique_ptr>& minMaxSolver, boost::optional const& lowerBound, boost::optional const& upperBound); + + /*! + * Analyzes the epoch model, i.e., solves the represented equation system. This method assumes a deterministic model. + */ + std::vector analyzeSingleObjective(Environment const& env, std::vector& x, std::vector& b, std::unique_ptr>& linEqSolver, boost::optional const& lowerBound, boost::optional const& upperBound); + }; + + + + + } + } + } +} \ No newline at end of file diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp index 87d2b968d..4bd08a021 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp @@ -287,7 +287,7 @@ namespace storm { } template - typename MultiDimensionalRewardUnfolding::EpochModel& MultiDimensionalRewardUnfolding::setCurrentEpoch(Epoch const& epoch) { + EpochModel& MultiDimensionalRewardUnfolding::setCurrentEpoch(Epoch const& epoch) { STORM_LOG_DEBUG("Setting model for epoch " << epochManager.toString(epoch)); // Check if we need to update the current epoch class @@ -446,8 +446,8 @@ namespace storm { if (model.isOfType(storm::models::ModelType::Dtmc)) { assert(zeroObjRewardChoices.size() == productModel->getProduct().getNumberOfStates()); assert(stepChoices.size() == productModel->getProduct().getNumberOfStates()); - STORM_LOG_ASSERT(equationSolverProblemFormatForEpochModel.is_initialized(), "Linear equation problem format was not set."); - bool convertToEquationSystem = equationSolverProblemFormatForEpochModel.get() == storm::solver::LinearEquationSolverProblemFormat::EquationSystem; + STORM_LOG_ASSERT(epochModel.equationSolverProblemFormat.is_initialized(), "Linear equation problem format was not set."); + bool convertToEquationSystem = epochModel.equationSolverProblemFormat.get() == storm::solver::LinearEquationSolverProblemFormat::EquationSystem; // For DTMCs we consider the subsystem induced by the considered states. // The transitions for states with zero reward are filtered out to guarantee a unique solution of the eq-system. auto backwardTransitions = epochModel.epochMatrix.transpose(true); @@ -547,7 +547,7 @@ namespace storm { template void MultiDimensionalRewardUnfolding::setEquationSystemFormatForEpochModel(storm::solver::LinearEquationSolverProblemFormat eqSysFormat) { STORM_LOG_ASSERT(model.isOfType(storm::models::ModelType::Dtmc), "Trying to set the equation problem format although the model is not deterministic."); - equationSolverProblemFormatForEpochModel = eqSysFormat; + epochModel.equationSolverProblemFormat = eqSysFormat; } diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.h b/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.h index e1b96c64c..1c3851b4f 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.h +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.h @@ -6,6 +6,7 @@ #include "storm/storage/SparseMatrix.h" #include "storm/modelchecker/multiobjective/Objective.h" #include "storm/modelchecker/prctl/helper/rewardbounded/EpochManager.h" +#include "storm/modelchecker/prctl/helper/rewardbounded/EpochModel.h" #include "storm/modelchecker/prctl/helper/rewardbounded/ProductModel.h" #include "storm/modelchecker/prctl/helper/rewardbounded/Dimension.h" #include "storm/models/sparse/Model.h" @@ -27,17 +28,7 @@ namespace storm { typedef typename EpochManager::EpochClass EpochClass; typedef typename std::conditional>::type SolutionType; - - struct EpochModel { - bool epochMatrixChanged; - storm::storage::SparseMatrix epochMatrix; - storm::storage::BitVector stepChoices; - std::vector stepSolutions; - std::vector> objectiveRewards; - std::vector objectiveRewardFilter; - storm::storage::BitVector epochInStates; - }; - + /* * * @param model The (preprocessed) model @@ -52,7 +43,7 @@ namespace storm { Epoch getStartEpoch(); std::vector getEpochComputationOrder(Epoch const& startEpoch); - EpochModel& setCurrentEpoch(Epoch const& epoch); + EpochModel& setCurrentEpoch(Epoch const& epoch); void setEquationSystemFormatForEpochModel(storm::solver::LinearEquationSolverProblemFormat eqSysFormat); @@ -117,13 +108,10 @@ namespace storm { std::vector epochModelToProductChoiceMap; std::shared_ptr const> productStateToEpochModelInStateMap; std::set possibleEpochSteps; - - EpochModel epochModel; + + EpochModel epochModel; boost::optional currentEpoch; - - // In case of DTMCs we have different options for the equation problem format the epoch model will have. - boost::optional equationSolverProblemFormatForEpochModel; - + EpochManager epochManager; std::vector> dimensions;