diff --git a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 9af12ad97..6b0cfd419 100644 --- a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -164,9 +164,34 @@ namespace storm { template template std::vector SparseMdpPrctlHelper::computeReachabilityRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { - // Only compute the result if the model has at least one reward this->getModel(). + // Only compute the result if the reward model is not empty. STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); - + return computeReachabilityRewardsHelper(minimize, transitionMatrix, backwardTransitions, + [&rewardModel] (uint_fast64_t rowCount, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates) { + return rewardModel.getTotalRewardVector(rowCount, transitionMatrix, maybeStates); + }, + targetStates, qualitative, minMaxLinearEquationSolverFactory); + } + + template + std::vector SparseMdpPrctlHelper::computeReachabilityRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& intervalRewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + // Only compute the result if the reward model is not empty. + STORM_LOG_THROW(!intervalRewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); + return computeReachabilityRewardsHelper(minimize, transitionMatrix, backwardTransitions, + [&] (uint_fast64_t rowCount, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates) { + std::vector fullIntervalRewardVector = intervalRewardModel.getTotalRewardVector(rowCount, transitionMatrix, maybeStates); + std::vector result(rowCount); + uint_fast64_t currentPosition = 0; + for (auto position : maybeStates) { + result[currentPosition] = minimize ? fullIntervalRewardVector[position].lower() : fullIntervalRewardVector[position].upper(); + } + return result; + }, + targetStates, qualitative, minMaxLinearEquationSolverFactory); + } + + template + std::vector SparseMdpPrctlHelper::computeReachabilityRewardsHelper(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { // Determine which states have a reward of infinity by definition. storm::storage::BitVector infinityStates; storm::storage::BitVector trueStates(transitionMatrix.getRowCount(), true); @@ -199,11 +224,11 @@ namespace storm { storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, false); // Prepare the right-hand side of the equation system. - std::vector b = rewardModel.getTotalRewardVector(submatrix.getRowCount(), transitionMatrix, maybeStates); + std::vector b = totalStateRewardVectorGetter(submatrix.getRowCount(), transitionMatrix, maybeStates); // Create vector for results for maybe states. std::vector x(maybeStates.getNumberOfSetBits()); - + // Solve the corresponding system of equations. std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(submatrix); solver->solveEquationSystem(minimize, x, b); @@ -417,7 +442,7 @@ namespace storm { template std::vector SparseMdpPrctlHelper::computeInstantaneousRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, uint_fast64_t stepCount, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template std::vector SparseMdpPrctlHelper::computeCumulativeRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template std::vector SparseMdpPrctlHelper::computeReachabilityRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - + } } } diff --git a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h index b584e5d28..95b5dbb1c 100644 --- a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h +++ b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h @@ -9,7 +9,16 @@ #include "src/utility/solver.h" +#include "src/adapters/CarlAdapter.h" + namespace storm { + namespace models { + namespace sparse { + template + class StandardRewardModel; + } + } + namespace modelchecker { namespace helper { @@ -30,10 +39,14 @@ namespace storm { template static std::vector computeReachabilityRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + + static std::vector computeReachabilityRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& intervalRewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); static std::vector computeLongRunAverage(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); private: + static std::vector computeReachabilityRewardsHelper(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static ValueType computeLraForMaximalEndComponent(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& goalStates, storm::storage::MaximalEndComponent const& mec); }; diff --git a/src/utility/storm.h b/src/utility/storm.h index 35960d474..b54ee42d6 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -33,6 +33,7 @@ // Model headers. #include "src/models/ModelBase.h" #include "src/models/sparse/Model.h" +#include "src/models/sparse/StandardRewardModel.h" #include "src/models/symbolic/Model.h" #include "src/models/symbolic/StandardRewardModel.h"