diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 94de9020b..64f52bcb1 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -264,7 +264,8 @@ namespace storm { } else { if (computeCumulativeReward) { result = std::vector(values.size()); - storm::utility::vector::applyPointwiseInPlace(result, [&uniformizationRate] (ValueType const& a) { return a / uniformizationRate; }); + std::function scaleWithUniformizationRate = [&uniformizationRate] (ValueType const& a) -> ValueType { return a / uniformizationRate; }; + storm::utility::vector::applyPointwiseInPlace(result, scaleWithUniformizationRate); } else { result = std::vector(values.size()); } @@ -369,6 +370,24 @@ namespace storm { return result; } + template + std::unique_ptr SparseCtmcCslModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + storm::storage::SparseMatrix probabilityMatrix = computeProbabilityMatrix(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector()); + + boost::optional> modifiedStateRewardVector; + if (this->getModel().hasStateRewards()) { + modifiedStateRewardVector = std::vector(this->getModel().getStateRewardVector()); + typename std::vector::const_iterator it2 = this->getModel().getExitRateVector().begin(); + for (typename std::vector::iterator it1 = modifiedStateRewardVector.get().begin(), ite1 = modifiedStateRewardVector.get().end(); it1 != ite1; ++it1, ++it2) { + *it1 /= *it2; + } + } + + return std::unique_ptr(new ExplicitQuantitativeCheckResult(SparseDtmcPrctlModelChecker::computeReachabilityRewardsHelper(probabilityMatrix, modifiedStateRewardVector, this->getModel().getOptionalTransitionRewardMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), *linearEquationSolver, qualitative))); + } + // Explicitly instantiate the model checker. template class SparseCtmcCslModelChecker; diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.h b/src/modelchecker/csl/SparseCtmcCslModelChecker.h index 7b3c35e64..2257075e7 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.h +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.h @@ -21,6 +21,7 @@ namespace storm { virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; protected: storm::models::sparse::Ctmc const& getModel() const override; @@ -31,6 +32,7 @@ namespace storm { static std::vector computeUntilProbabilitiesHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolver const& linearEquationSolver); std::vector computeInstantaneousRewardsHelper(double timeBound) const; std::vector computeCumulativeRewardsHelper(double timeBound) const; + std::vector computeReachabilityRewardsHelper(storm::storage::BitVector const& targetStates, bool qualitative) const; /*! * Computes the matrix representing the transitions of the uniformized CTMC. diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 2e5e928ac..cdde1e716 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -217,13 +217,13 @@ namespace storm { } template - std::vector SparseDtmcPrctlModelChecker::computeReachabilityRewardsHelper(storm::storage::BitVector const& targetStates, bool qualitative) const { + std::vector SparseDtmcPrctlModelChecker::computeReachabilityRewardsHelper(storm::storage::SparseMatrix const& transitionMatrix, boost::optional> const& stateRewardVector, boost::optional> const& transitionRewardMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::solver::LinearEquationSolver const& linearEquationSolver, bool qualitative) { // Only compute the result if the model has at least one reward this->getModel(). - STORM_LOG_THROW(this->getModel().hasStateRewards() || this->getModel().hasTransitionRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); + STORM_LOG_THROW(stateRewardVector || transitionRewardMatrix, storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); // Determine which states have a reward of infinity by definition. - storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true); - storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(this->getModel().getBackwardTransitions(), trueStates, targetStates); + storm::storage::BitVector trueStates(transitionMatrix.getRowCount(), true); + storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(backwardTransitions, trueStates, targetStates); infinityStates.complement(); storm::storage::BitVector maybeStates = ~targetStates & ~infinityStates; STORM_LOG_INFO("Found " << infinityStates.getNumberOfSetBits() << " 'infinity' states."); @@ -231,7 +231,7 @@ namespace storm { STORM_LOG_INFO("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); // Create resulting vector. - std::vector result(this->getModel().getNumberOfStates()); + std::vector result(transitionMatrix.getRowCount()); // Check whether we need to compute exact rewards for some states. if (qualitative) { @@ -241,7 +241,7 @@ namespace storm { } else { // In this case we have to compute the reward values for the remaining states. // We can eliminate the rows and columns from the original transition probability matrix. - storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(true, maybeStates, maybeStates, true); + storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, true); // Converting the matrix from the fixpoint notation to the form needed for the equation // system. That is, we go from x = A*x + b to (I-A)x = b. @@ -253,20 +253,20 @@ namespace storm { // Prepare the right-hand side of the equation system. std::vector b(submatrix.getRowCount()); - if (this->getModel().hasTransitionRewards()) { + if (transitionRewardMatrix) { // If a transition-based reward model is available, we initialize the right-hand // side to the vector resulting from summing the rows of the pointwise product // of the transition probability matrix and the transition reward matrix. - std::vector pointwiseProductRowSumVector = this->getModel().getTransitionMatrix().getPointwiseProductRowSumVector(this->getModel().getTransitionRewardMatrix()); + std::vector pointwiseProductRowSumVector = transitionMatrix.getPointwiseProductRowSumVector(transitionRewardMatrix.get()); storm::utility::vector::selectVectorValues(b, maybeStates, pointwiseProductRowSumVector); - if (this->getModel().hasStateRewards()) { + if (stateRewardVector) { // If a state-based reward model is also available, we need to add this vector // as well. As the state reward vector contains entries not just for the states // that we still consider (i.e. maybeStates), we need to extract these values // first. std::vector subStateRewards(b.size()); - storm::utility::vector::selectVectorValues(subStateRewards, maybeStates, this->getModel().getStateRewardVector()); + storm::utility::vector::selectVectorValues(subStateRewards, maybeStates, stateRewardVector.get()); storm::utility::vector::addVectorsInPlace(b, subStateRewards); } } else { @@ -274,12 +274,11 @@ namespace storm { // right-hand side. As the state reward vector contains entries not just for the // states that we still consider (i.e. maybeStates), we need to extract these values // first. - storm::utility::vector::selectVectorValues(b, maybeStates, this->getModel().getStateRewardVector()); + storm::utility::vector::selectVectorValues(b, maybeStates, stateRewardVector.get()); } // Now solve the resulting equation system. - STORM_LOG_THROW(linearEquationSolver != nullptr, storm::exceptions::InvalidStateException, "No valid linear equation solver available."); - this->linearEquationSolver->solveEquationSystem(submatrix, x, b); + linearEquationSolver.solveEquationSystem(submatrix, x, b); // Set values of resulting vector according to result. storm::utility::vector::setVectorValues(result, maybeStates, x); @@ -296,7 +295,7 @@ namespace storm { std::unique_ptr SparseDtmcPrctlModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeReachabilityRewardsHelper(subResult.getTruthValuesVector(), qualitative))); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeReachabilityRewardsHelper(this->getModel().getTransitionMatrix(), this->getModel().getOptionalStateRewardVector(), this->getModel().getOptionalTransitionRewardMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), *this->linearEquationSolver, qualitative))); } template diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index 5913b373c..b5e73436b 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -38,7 +38,7 @@ namespace storm { static std::vector computeUntilProbabilitiesHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolver const& linearEquationSolver); std::vector computeInstantaneousRewardsHelper(uint_fast64_t stepCount) const; std::vector computeCumulativeRewardsHelper(uint_fast64_t stepBound) const; - std::vector computeReachabilityRewardsHelper(storm::storage::BitVector const& targetStates, bool qualitative) const; + static std::vector computeReachabilityRewardsHelper(storm::storage::SparseMatrix const& transitionMatrix, boost::optional> const& stateRewardVector, boost::optional> const& transitionRewardMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::solver::LinearEquationSolver const& linearEquationSolver, bool qualitative); // An object that is used for solving linear equations and performing matrix-vector multiplication. std::unique_ptr> linearEquationSolver; diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 973a7731a..fdf85d1b6 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -228,17 +228,17 @@ namespace storm { } template - std::vector SparseMdpPrctlModelChecker::computeReachabilityRewardsHelper(bool minimize, storm::storage::BitVector const& targetStates, bool qualitative) const { + std::vector SparseMdpPrctlModelChecker::computeReachabilityRewardsHelper(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, boost::optional> const& stateRewardVector, boost::optional> const& transitionRewardMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::solver::NondeterministicLinearEquationSolver const& nondeterministicLinearEquationSolver, bool qualitative) const { // Only compute the result if the model has at least one reward this->getModel(). - STORM_LOG_THROW(this->getModel().hasStateRewards() || this->getModel().hasTransitionRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); + STORM_LOG_THROW(stateRewardVector || transitionRewardMatrix, storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); // Determine which states have a reward of infinity by definition. storm::storage::BitVector infinityStates; - storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true); + storm::storage::BitVector trueStates(transitionMatrix.getRowCount(), true); if (minimize) { - infinityStates = std::move(storm::utility::graph::performProb1A(this->getModel().getTransitionMatrix(), this->getModel().getTransitionMatrix().getRowGroupIndices(), this->getModel().getBackwardTransitions(), trueStates, targetStates)); + infinityStates = std::move(storm::utility::graph::performProb1A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, trueStates, targetStates)); } else { - infinityStates = std::move(storm::utility::graph::performProb1E(this->getModel().getTransitionMatrix(), this->getModel().getTransitionMatrix().getRowGroupIndices(), this->getModel().getBackwardTransitions(), trueStates, targetStates)); + infinityStates = std::move(storm::utility::graph::performProb1E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, trueStates, targetStates)); } infinityStates.complement(); storm::storage::BitVector maybeStates = ~targetStates & ~infinityStates; @@ -247,12 +247,11 @@ namespace storm { LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); // Create resulting vector. - std::vector result(this->getModel().getNumberOfStates()); + std::vector result(transitionMatrix.getRowCount()); // Check whether we need to compute exact rewards for some states. - if (this->getModel().getInitialStates().isDisjointFrom(maybeStates)) { - LOG4CPLUS_INFO(logger, "The rewards for the initial states were determined in a preprocessing step." - << " No exact rewards were computed."); + if (qualitative) { + LOG4CPLUS_INFO(logger, "The rewards for the initial states were determined in a preprocessing step. No exact rewards were computed."); // Set the values for all maybe-states to 1 to indicate that their reward values // are neither 0 nor infinity. storm::utility::vector::setVectorValues(result, maybeStates, storm::utility::one()); @@ -261,26 +260,26 @@ namespace storm { // We can eliminate the rows and columns from the original transition probability matrix for states // whose reward values are already known. - storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(true, maybeStates, maybeStates, false); + storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, false); // Prepare the right-hand side of the equation system. For entry i this corresponds to // the accumulated probability of going from state i to some 'yes' state. std::vector b(submatrix.getRowCount()); - if (this->getModel().hasTransitionRewards()) { + if (transitionRewardMatrix) { // If a transition-based reward model is available, we initialize the right-hand // side to the vector resulting from summing the rows of the pointwise product // of the transition probability matrix and the transition reward matrix. - std::vector pointwiseProductRowSumVector = this->getModel().getTransitionMatrix().getPointwiseProductRowSumVector(this->getModel().getTransitionRewardMatrix()); - storm::utility::vector::selectVectorValues(b, maybeStates, this->getModel().getTransitionMatrix().getRowGroupIndices(), pointwiseProductRowSumVector); + std::vector pointwiseProductRowSumVector = transitionMatrix.getPointwiseProductRowSumVector(transitionRewardMatrix.get()); + storm::utility::vector::selectVectorValues(b, maybeStates, transitionMatrix.getRowGroupIndices(), pointwiseProductRowSumVector); - if (this->getModel().hasStateRewards()) { + if (stateRewardVector) { // If a state-based reward model is also available, we need to add this vector // as well. As the state reward vector contains entries not just for the states // that we still consider (i.e. maybeStates), we need to extract these values // first. std::vector subStateRewards(b.size()); - storm::utility::vector::selectVectorValuesRepeatedly(subStateRewards, maybeStates, this->getModel().getTransitionMatrix().getRowGroupIndices(), this->getModel().getStateRewardVector()); + storm::utility::vector::selectVectorValuesRepeatedly(subStateRewards, maybeStates, transitionMatrix.getRowGroupIndices(), stateRewardVector.get()); storm::utility::vector::addVectorsInPlace(b, subStateRewards); } } else { @@ -288,7 +287,7 @@ namespace storm { // right-hand side. As the state reward vector contains entries not just for the // states that we still consider (i.e. maybeStates), we need to extract these values // first. - storm::utility::vector::selectVectorValuesRepeatedly(b, maybeStates, this->getModel().getTransitionMatrix().getRowGroupIndices(), this->getModel().getStateRewardVector()); + storm::utility::vector::selectVectorValuesRepeatedly(b, maybeStates, transitionMatrix.getRowGroupIndices(), stateRewardVector.get()); } // Create vector for results for maybe states. @@ -313,7 +312,7 @@ namespace storm { STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic."); std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeReachabilityRewardsHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, subResult.getTruthValuesVector(), qualitative))); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeReachabilityRewardsHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel().getTransitionMatrix(), this->getModel().getOptionalStateRewardVector(), this->getModel().getOptionalTransitionRewardMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), *this->nondeterministicLinearEquationSolver, qualitative))); } template diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index cfe6188e2..153b5168a 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -51,7 +51,7 @@ namespace storm { static std::vector computeUntilProbabilitiesHelper(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::shared_ptr> nondeterministicLinearEquationSolver, bool qualitative); std::vector computeInstantaneousRewardsHelper(bool minimize, uint_fast64_t stepCount) const; std::vector computeCumulativeRewardsHelper(bool minimize, uint_fast64_t stepBound) const; - std::vector computeReachabilityRewardsHelper(bool minimize, storm::storage::BitVector const& targetStates, bool qualitative) const; + std::vector computeReachabilityRewardsHelper(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, boost::optional> const& stateRewardVector, boost::optional> const& transitionRewardMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::solver::NondeterministicLinearEquationSolver const& nondeterministicLinearEquationSolver, bool qualitative) const; // A solver that is used for solving systems of linear equations that are the result of nondeterministic choices. std::shared_ptr> nondeterministicLinearEquationSolver; diff --git a/src/models/sparse/Model.cpp b/src/models/sparse/Model.cpp index cc0f088a6..6541d517f 100644 --- a/src/models/sparse/Model.cpp +++ b/src/models/sparse/Model.cpp @@ -93,11 +93,21 @@ namespace storm { return transitionRewardMatrix.get(); } + template + boost::optional> const& Model::getOptionalTransitionRewardMatrix() const { + return transitionRewardMatrix; + } + template std::vector const& Model::getStateRewardVector() const { return stateRewardVector.get(); } + template + boost::optional> const& Model::getOptionalStateRewardVector() const { + return stateRewardVector; + } + template std::vector> const& Model::getChoiceLabeling() const { return choiceLabeling.get(); diff --git a/src/models/sparse/Model.h b/src/models/sparse/Model.h index 787822e2d..103da9fba 100644 --- a/src/models/sparse/Model.h +++ b/src/models/sparse/Model.h @@ -139,6 +139,13 @@ namespace storm { */ storm::storage::SparseMatrix const& getTransitionRewardMatrix() const; + /*! + * Retrieves an optional value that contains the transition reward matrix if there is one. + * + * @return The transition reward matrix if there is one. + */ + boost::optional> const& getOptionalTransitionRewardMatrix() const; + /*! * Retrieves the matrix representing the transition rewards of the model. Note that calling this method * is only valid if the model has transition rewards. @@ -155,6 +162,13 @@ namespace storm { */ std::vector const& getStateRewardVector() const; + /*! + * Retrieves an optional value that contains the state reward vector if there is one. + * + * @return The state reward vector if there is one. + */ + boost::optional> const& getOptionalStateRewardVector() const; + /*! * Retrieves the labels for the choices of the model. Note that calling this method is only valud if the * model has a choice labling. diff --git a/src/utility/vector.h b/src/utility/vector.h index 7c9ac7216..09ee43579 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -160,7 +160,7 @@ namespace storm { * @param function The function to apply. */ template - void applyPointwiseInPlace(std::vector& target, std::function function) { + void applyPointwiseInPlace(std::vector& target, std::function const& function) { #ifdef STORM_HAVE_INTELTBB tbb::parallel_for(tbb::blocked_range(0, target.size()), [&](tbb::blocked_range const& range) {