Merge remote-tracking branch 'upstream/master'

src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp

@@ -200,12 +200,16 @@ namespace storm {
             
             template <typename ValueType, typename RewardModelType>
             std::vector<ValueType> SparseMarkovAutomatonCslHelper::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
-                std::vector<ValueType> stateRewardWeights(transitionMatrix.getRowGroupCount());
+                
+                // Get a reward model where the state rewards are scaled accordingly
+                std::vector<ValueType> stateRewardWeights(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
                 for (auto const markovianState : markovianStates) {
                     stateRewardWeights[markovianState] = storm::utility::one<ValueType>() / exitRateVector[markovianState];
                 }
                 std::vector<ValueType> totalRewardVector = rewardModel.getTotalActionRewardVector(transitionMatrix, stateRewardWeights);
-                return computeExpectedRewards(dir, transitionMatrix, backwardTransitions, psiStates, totalRewardVector, minMaxLinearEquationSolverFactory);
+                RewardModelType scaledRewardModel(boost::none, std::move(totalRewardVector));
+                
+                return SparseMdpPrctlHelper<ValueType>::computeReachabilityRewards(dir, transitionMatrix, backwardTransitions, scaledRewardModel, psiStates, false, false, minMaxLinearEquationSolverFactory).values;
             }
             
             template<typename ValueType>
@@ -365,112 +369,15 @@ namespace storm {
             
             template <typename ValueType>
             std::vector<ValueType> SparseMarkovAutomatonCslHelper::computeReachabilityTimes(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
+                
+                // Get a reward model representing expected sojourn times
                 std::vector<ValueType> rewardValues(transitionMatrix.getRowCount(), storm::utility::zero<ValueType>());
                 for (auto const markovianState : markovianStates) {
                     rewardValues[transitionMatrix.getRowGroupIndices()[markovianState]] = storm::utility::one<ValueType>() / exitRateVector[markovianState];
                 }
-                return computeExpectedRewards(dir, transitionMatrix, backwardTransitions, psiStates, rewardValues, minMaxLinearEquationSolverFactory);
-            }
-
-            template<typename ValueType>
-            std::vector<ValueType> SparseMarkovAutomatonCslHelper::computeExpectedRewards(OptimizationDirection dir,
-                                                                              storm::storage::SparseMatrix<ValueType> const &transitionMatrix,
-                                                                              storm::storage::SparseMatrix<ValueType> const &backwardTransitions,
-                                                                              storm::storage::BitVector const &goalStates,
-                                                                              std::vector<ValueType> const &stateActionRewardVector,
-                                                                              storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const &minMaxLinearEquationSolverFactory) {
-
-                uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount();
+                storm::models::sparse::StandardRewardModel<ValueType> rewardModel(boost::none, std::move(rewardValues));
                 
-                // First, we need to check which states have infinite expected time (by definition).
-                storm::storage::BitVector infinityStates;
-                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<ValueType> 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 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);
-                    } 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<ValueType> 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) {
-                            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);
-                    } else {
-                        // Otherwise, we have no infinity states.
-                        infinityStates = storm::storage::BitVector(numberOfStates);
-                    }
-                }
-                // Now we identify the states for which values need to be computed.
-                storm::storage::BitVector maybeStates = ~(goalStates | infinityStates);
-
-                // Create resulting vector.
-                std::vector<ValueType> result(numberOfStates);
-
-                if (!maybeStates.empty()) {
-                    // Then, we can eliminate the rows and columns for all states whose values are already known.
-                    std::vector<ValueType> x(maybeStates.getNumberOfSetBits());
-                    storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, maybeStates,
-                                                                                                      maybeStates);
-
-                    // Finally, prepare the actual right-hand side.
-                    std::vector<ValueType> b(submatrix.getRowCount());
-                    storm::utility::vector::selectVectorValues(b, maybeStates,
-                                                               transitionMatrix.getRowGroupIndices(),
-                                                               stateActionRewardVector);
-
-                    // Solve the corresponding system of equations.
-                    std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> 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<ValueType>(result, maybeStates, x);
-                }
-
-                storm::utility::vector::setVectorValues(result, goalStates, storm::utility::zero<ValueType>());
-                storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::infinity<ValueType>());
-
-                return result;
+                return SparseMdpPrctlHelper<ValueType>::computeReachabilityRewards(dir, transitionMatrix, backwardTransitions, rewardModel, psiStates, false, false, minMaxLinearEquationSolverFactory).values;
             }
 
             template<typename ValueType>
@@ -550,8 +457,6 @@ namespace storm {
                 
             template double SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<double> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::MaximalEndComponent const& mec);
                 
-            template std::vector<double> SparseMarkovAutomatonCslHelper::computeExpectedRewards(OptimizationDirection dir, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& goalStates, std::vector<double> const& stateRewards, storm::solver::MinMaxLinearEquationSolverFactory<double> const& minMaxLinearEquationSolverFactory);
-
             template std::vector<storm::RationalNumber> SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::vector<storm::RationalNumber> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::pair<double, double> const& boundsPair, storm::solver::MinMaxLinearEquationSolverFactory<storm::RationalNumber> const& minMaxLinearEquationSolverFactory);
                 
             template std::vector<storm::RationalNumber> SparseMarkovAutomatonCslHelper::computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory<storm::RationalNumber> const& minMaxLinearEquationSolverFactory);
@@ -566,8 +471,6 @@ namespace storm {
                 
             template storm::RationalNumber SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::vector<storm::RationalNumber> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::MaximalEndComponent const& mec);
                 
-            template std::vector<storm::RationalNumber> SparseMarkovAutomatonCslHelper::computeExpectedRewards(OptimizationDirection dir, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& goalStates, std::vector<storm::RationalNumber> const& stateRewards, storm::solver::MinMaxLinearEquationSolverFactory<storm::RationalNumber> const& minMaxLinearEquationSolverFactory);
-
         }
     }
 }

src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h

@@ -55,22 +55,6 @@ namespace storm {
                  */
                 template <typename ValueType>
                 static ValueType computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::MaximalEndComponent const& mec);
-                
-                /*!
-                 * Computes the expected reward that is gained from each state before entering any of the goal states.
-                 *
-                 * @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 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
-                 * reward is dependent on the expected time to stay in the state, i.e. it is gouverned by the exit rate
-                 * of the state.
-                 * @return A vector that contains the expected reward for each state of the model.
-                 */
-                template <typename ValueType>
-                static std::vector<ValueType> computeExpectedRewards(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& goalStates, std::vector<ValueType> const& stateRewards, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
             };
             
         }