From 5b77d827dc193993a6084e1e775cc7c443ec8664 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 19 Aug 2015 23:58:32 +0200
Subject: [PATCH] fixed a bug
Former-commit-id: 2a19ecc4f7f4e2bf2808d5d84e8269666ae397fc
---
src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp | 2 +-
src/models/sparse/Model.cpp | 2 +-
src/models/symbolic/Model.cpp | 2 +-
3 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
index 2e93246b3..1f9a9552f 100644
--- a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
+++ b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
@@ -160,7 +160,7 @@ namespace storm {
template<typename ValueType, typename RewardModelType>
std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::function<std::vector<ValueType> const&(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
-
+
// Determine which states have a reward of infinity by definition.
storm::storage::BitVector trueStates(transitionMatrix.getRowCount(), true);
storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(backwardTransitions, trueStates, targetStates);
diff --git a/src/models/sparse/Model.cpp b/src/models/sparse/Model.cpp
index 7a1d8beba..f438f7420 100644
--- a/src/models/sparse/Model.cpp
+++ b/src/models/sparse/Model.cpp
@@ -90,7 +90,7 @@ namespace storm {
template<typename ValueType, typename RewardModelType>
RewardModelType const& Model<ValueType, RewardModelType>::getRewardModel(std::string const& rewardModelName) const {
auto it = this->rewardModels.find(rewardModelName);
- STORM_LOG_THROW(it != this->rewardModels.end(), storm::exceptions::IllegalArgumentException, "The requested reward model does not exist.");
+ STORM_LOG_THROW(it != this->rewardModels.end(), storm::exceptions::IllegalArgumentException, "The requested reward model '" << rewardModelName << "' does not exist.");
return it->second;
}
diff --git a/src/models/symbolic/Model.cpp b/src/models/symbolic/Model.cpp
index 13950e681..48384395d 100644
--- a/src/models/symbolic/Model.cpp
+++ b/src/models/symbolic/Model.cpp
@@ -132,7 +132,7 @@ namespace storm {
template<storm::dd::DdType Type>
typename Model<Type>::RewardModelType const& Model<Type>::getRewardModel(std::string const& rewardModelName) const {
auto it = this->rewardModels.find(rewardModelName);
- STORM_LOG_THROW(it != this->rewardModels.end(), storm::exceptions::InvalidArgumentException, "Unknown reward model '" << rewardModelName << "'.");
+ STORM_LOG_THROW(it != this->rewardModels.end(), storm::exceptions::InvalidArgumentException, "The requested reward model '" << rewardModelName << "' does not exist.");
return it->second;
}