diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 4bbc92e73..a76916519 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -190,8 +190,12 @@ namespace storm { template template std::vector SparseMarkovAutomatonCslHelper::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { - std::vector totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix.getRowCount(), transitionMatrix, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true)); - return computeExpectedRewards(dir, transitionMatrix, backwardTransitions, exitRateVector, markovianStates, psiStates, totalRewardVector, minMaxLinearEquationSolverFactory); + std::vector stateRewardWeights(transitionMatrix.getRowGroupCount()); + for (auto const markovianState : markovianStates) { + stateRewardWeights[markovianState] = storm::utility::one() / exitRateVector[markovianState]; + } + std::vector totalRewardVector = rewardModel.getTotalActionRewardVector(transitionMatrix, stateRewardWeights); + return computeExpectedRewards(dir, transitionMatrix, backwardTransitions, psiStates, totalRewardVector, minMaxLinearEquationSolverFactory); } template @@ -351,58 +355,77 @@ namespace storm { template std::vector SparseMarkovAutomatonCslHelper::computeTimes(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { - uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); - std::vector rewardValues(numberOfStates, storm::utility::zero()); - storm::utility::vector::setVectorValues(rewardValues, markovianStates, storm::utility::one()); - return computeExpectedRewards(dir, transitionMatrix, backwardTransitions, exitRateVector, markovianStates, psiStates, rewardValues, minMaxLinearEquationSolverFactory); + std::vector rewardValues(transitionMatrix.getRowCount(), storm::utility::zero()); + for (auto const markovianState : markovianStates) { + rewardValues[transitionMatrix.getRowGroupIndices()[markovianState]] = storm::utility::one() / exitRateVector[markovianState]; + } + return computeExpectedRewards(dir, transitionMatrix, backwardTransitions, psiStates, rewardValues, minMaxLinearEquationSolverFactory); } - - template - std::vector SparseMarkovAutomatonCslHelper::computeExpectedRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, std::vector const& stateRewards, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + + template + std::vector + SparseMarkovAutomatonCslHelper::computeExpectedRewards(OptimizationDirection dir, + storm::storage::SparseMatrix const &transitionMatrix, + storm::storage::SparseMatrix const &backwardTransitions, + storm::storage::BitVector const &goalStates, + std::vector const &stateActionRewardVector, + storm::solver::MinMaxLinearEquationSolverFactory const &minMaxLinearEquationSolverFactory) { uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); - + // First, we need to check which states have infinite expected time (by definition). storm::storage::BitVector infinityStates; - if (dir ==OptimizationDirection::Minimize) { + if (dir == OptimizationDirection::Minimize) { // If we need to compute the minimum expected times, we have to set the values of those states to infinity that, under all schedulers, // reach a bottom SCC without a goal state. - + // So we start by computing all bottom SCCs without goal states. - storm::storage::StronglyConnectedComponentDecomposition sccDecomposition(transitionMatrix, ~goalStates, true, true); - + storm::storage::StronglyConnectedComponentDecomposition sccDecomposition(transitionMatrix, + ~goalStates, true, + true); + // Now form the union of all these SCCs. storm::storage::BitVector unionOfNonGoalBSccs(numberOfStates); - for (auto const& scc : sccDecomposition) { + for (auto const &scc : sccDecomposition) { for (auto state : scc) { unionOfNonGoalBSccs.set(state); } } - + // Finally, if this union is non-empty, compute the states such that all schedulers reach some state of the union. if (!unionOfNonGoalBSccs.empty()) { - infinityStates = storm::utility::graph::performProbGreater0A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, storm::storage::BitVector(numberOfStates, true), unionOfNonGoalBSccs); + infinityStates = storm::utility::graph::performProbGreater0A(transitionMatrix, + transitionMatrix.getRowGroupIndices(), + backwardTransitions, + storm::storage::BitVector( + numberOfStates, true), + unionOfNonGoalBSccs); } else { // Otherwise, we have no infinity states. infinityStates = storm::storage::BitVector(numberOfStates); } } else { // If we maximize the property, the expected time of a state is infinite, if an end-component without any goal state is reachable. - + // So we start by computing all MECs that have no goal state. - storm::storage::MaximalEndComponentDecomposition mecDecomposition(transitionMatrix, backwardTransitions, ~goalStates); - + storm::storage::MaximalEndComponentDecomposition mecDecomposition(transitionMatrix, + backwardTransitions, + ~goalStates); + // Now we form the union of all states in these end components. storm::storage::BitVector unionOfNonGoalMaximalEndComponents(numberOfStates); - for (auto const& mec : mecDecomposition) { - for (auto const& stateActionPair : mec) { + for (auto const &mec : mecDecomposition) { + for (auto const &stateActionPair : mec) { unionOfNonGoalMaximalEndComponents.set(stateActionPair.first); } } - + if (!unionOfNonGoalMaximalEndComponents.empty()) { // Now we need to check for which states there exists a scheduler that reaches one of the previously computed states. - infinityStates = storm::utility::graph::performProbGreater0E(backwardTransitions, storm::storage::BitVector(numberOfStates, true), unionOfNonGoalMaximalEndComponents); + infinityStates = storm::utility::graph::performProbGreater0E(backwardTransitions, + storm::storage::BitVector( + numberOfStates, true), + unionOfNonGoalMaximalEndComponents); } else { // Otherwise, we have no infinity states. infinityStates = storm::storage::BitVector(numberOfStates); @@ -413,33 +436,31 @@ namespace storm { // Create resulting vector. std::vector result(numberOfStates); - + if (!maybeStates.empty()) { // Then, we can eliminate the rows and columns for all states whose values are already known. std::vector x(maybeStates.getNumberOfSetBits()); - storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates); - - // Now prepare the expected reward values for all states so they can be used as the right-hand side of the equation system. - std::vector rewardValues(stateRewards); - for (auto state : markovianStates) { - rewardValues[state] = rewardValues[state] / exitRateVector[state]; - } - + storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, maybeStates, + maybeStates); + // Finally, prepare the actual right-hand side. std::vector b(submatrix.getRowCount()); - storm::utility::vector::selectVectorValuesRepeatedly(b, maybeStates, transitionMatrix.getRowGroupIndices(), rewardValues); - + storm::utility::vector::selectVectorValues(b, maybeStates, + transitionMatrix.getRowGroupIndices(), + stateActionRewardVector); + // Solve the corresponding system of equations. - std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(submatrix); + std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create( + submatrix); solver->solveEquations(dir, x, b); - + // Set values of resulting vector according to previous result and return the result. storm::utility::vector::setVectorValues(result, maybeStates, x); } storm::utility::vector::setVectorValues(result, goalStates, storm::utility::zero()); storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::infinity()); - + return result; } diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h index ba8223b60..f0ab29ebc 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h @@ -32,7 +32,7 @@ namespace storm { /*! * Computes the long-run average value for the given maximal end component of a Markov automaton. * - * @param minimize Sets whether the long-run average is to be minimized or maximized. + * @param dir Sets whether the long-run average is to be minimized or maximized. * @param transitionMatrix The transition matrix of the underlying Markov automaton. * @param markovianStates A bit vector storing all markovian states. * @param exitRateVector A vector with exit rates for all states. Exit rates of probabilistic states are @@ -46,12 +46,9 @@ namespace storm { /*! * Computes the expected reward that is gained from each state before entering any of the goal states. * - * @param minimize Indicates whether minimal or maximal rewards are to be computed. + * @param dir Indicates whether minimal or maximal rewards are to be computed. * @param transitionMatrix The transition matrix of the underlying Markov automaton. * @param backwardTransitions The reversed transition relation of the underlying Markov automaton. - * @param exitRateVector A vector with exit rates for all states. Exit rates of probabilistic states are - * assumed to be zero. - * @param markovianStates A bit vector storing all markovian states. * @param goalStates The goal states that define until which point rewards are gained. * @param stateRewards A vector that defines the reward gained in each state. For probabilistic states, * this is an instantaneous reward that is fully gained and for Markovian states the actually gained @@ -59,7 +56,7 @@ namespace storm { * of the state. * @return A vector that contains the expected reward for each state of the model. */ - static std::vector computeExpectedRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, std::vector const& stateRewards, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeExpectedRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& goalStates, std::vector const& stateRewards, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); }; } diff --git a/src/storm/models/sparse/StandardRewardModel.cpp b/src/storm/models/sparse/StandardRewardModel.cpp index fa2b63900..4f43c62fb 100644 --- a/src/storm/models/sparse/StandardRewardModel.cpp +++ b/src/storm/models/sparse/StandardRewardModel.cpp @@ -161,7 +161,7 @@ namespace storm { this->optionalStateActionRewardVector = boost::none; } } - + template template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix) const { @@ -211,24 +211,23 @@ namespace storm { } return result; } - - template - std::vector StandardRewardModel::getTotalStateActionRewardVector(uint_fast64_t numberOfRows, std::vector const& rowGroupIndices) const { - std::vector result = this->hasStateActionRewards() ? this->getStateActionRewardVector() : std::vector(numberOfRows); - if (this->hasStateRewards()) { - storm::utility::vector::addVectorToGroupedVector(result, this->getStateRewardVector(), rowGroupIndices); - } - return result; - } - + template - std::vector StandardRewardModel::getTotalStateActionRewardVector(uint_fast64_t numberOfRows, std::vector const& rowGroupIndices, storm::storage::BitVector const& filter) const { - std::vector result(numberOfRows); - if (this->hasStateRewards()) { - storm::utility::vector::selectVectorValuesRepeatedly(result, filter, rowGroupIndices, this->getStateRewardVector()); + template + std::vector StandardRewardModel::getTotalActionRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& stateRewardWeights) const { + std::vector result; + if (this->hasTransitionRewards()) { + result = transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()); + } else { + result = std::vector(transitionMatrix.getRowCount()); } if (this->hasStateActionRewards()) { - storm::utility::vector::addFilteredVectorGroupsToGroupedVector(result, this->getStateActionRewardVector(), filter, rowGroupIndices); + storm::utility::vector::addVectors(result, this->getStateActionRewardVector(), result); + } + if (this->hasStateRewards()) { + std::vector scaledStateRewardVector(transitionMatrix.getRowGroupCount()); + storm::utility::vector::multiplyVectorsPointwise(this->getStateRewardVector(), stateRewardWeights, scaledStateRewardVector); + storm::utility::vector::addVectorToGroupedVector(result, scaledStateRewardVector, transitionMatrix.getRowGroupIndices()); } return result; } @@ -304,6 +303,7 @@ namespace storm { template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix) const; template std::vector StandardRewardModel::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& filter) const; template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights, bool scaleTransAndActions) const; + template std::vector StandardRewardModel::getTotalActionRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& stateRewardWeights) const; template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards); template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, double const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, double const & newValue); @@ -313,6 +313,7 @@ namespace storm { template std::vector StandardRewardModel::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& filter) const; template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix) const; template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights, bool scaleTransAndActions) const; + template std::vector StandardRewardModel::getTotalActionRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& stateRewardWeights) const; template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards); template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, float const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, float const & newValue); @@ -323,24 +324,27 @@ namespace storm { template std::vector StandardRewardModel::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& filter) const; template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix) const; template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights, bool scaleTransAndActions) const; + template std::vector StandardRewardModel::getTotalActionRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& stateRewardWeights) const; template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards); template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, storm::RationalNumber const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, storm::RationalNumber const & newValue); template class StandardRewardModel; template std::ostream& operator<<(std::ostream& out, StandardRewardModel const& rewardModel); - + template std::vector StandardRewardModel::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& filter) const; template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix) const; template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights, bool scaleTransAndActions) const; + template std::vector StandardRewardModel::getTotalActionRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& stateRewardWeights) const; template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards); template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, storm::RationalFunction const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, storm::RationalFunction const & newValue); template class StandardRewardModel; template std::ostream& operator<<(std::ostream& out, StandardRewardModel const& rewardModel); - + template std::vector StandardRewardModel::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& filter) const; template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix) const; template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights, bool scaleTransAndActions) const; + template std::vector StandardRewardModel::getTotalActionRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& stateRewardWeights) const; template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, double const & newValue); template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, storm::Interval const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, double const & newValue); diff --git a/src/storm/models/sparse/StandardRewardModel.h b/src/storm/models/sparse/StandardRewardModel.h index dbf484c40..7251ac656 100644 --- a/src/storm/models/sparse/StandardRewardModel.h +++ b/src/storm/models/sparse/StandardRewardModel.h @@ -217,28 +217,19 @@ namespace storm { */ template std::vector getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& filter) const; - - /*! - * Creates a vector representing the complete state action reward vector based on the state-, state-action- - * and transition-based rewards in the reward model. - * - * @param numberOfRows The total number of rows of the resulting vector. - * @param rowGroupIndices The starting indices of the row groups. - * @return The full state-action reward vector. - */ - std::vector getTotalStateActionRewardVector(uint_fast64_t numberOfRows, std::vector const& rowGroupIndices) const; - + /*! - * Creates a vector representing the complete state action reward vector based on the state- and - * state-action rewards in the reward model. + * Creates a vector representing the complete action-based rewards, i.e., state-action- and + * transition-based rewards * * @param numberOfRows The total number of rows of the resulting vector. - * @param rowGroupIndices The starting indices of the row groups. - * @param filter A bit vector indicating which row groups to select. - * @return The full state-action reward vector. + * @param transitionMatrix The matrix that is used to weight the values of the transition reward matrix. + * @return The state-action reward vector that considers state-action rewards and transition rewards of this reward model. */ - std::vector getTotalStateActionRewardVector(uint_fast64_t numberOfRows, std::vector const& rowGroupIndices, storm::storage::BitVector const& filter) const; - + + template + std::vector getTotalActionRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& stateRewardWeights) const; + /*! * Sets the given value in the state-action reward vector at the given row. This assumes that the reward * model has state-action rewards.