From 9cf488b249a99d6935cc9470ed132e2fd7435744 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 24 Aug 2015 23:21:45 +0200
Subject: [PATCH] moved to checking the validity of transition matrices by
 calling the matrix function

Former-commit-id: 720ec563802cff997fc033179bc23eb51e67f2bd
---
 src/models/sparse/Dtmc.cpp | 28 ++--------------------------
 src/models/sparse/Dtmc.h   |  8 --------
 src/models/sparse/Mdp.cpp  | 24 ++----------------------
 src/models/sparse/Mdp.h    |  8 --------
 4 files changed, 4 insertions(+), 64 deletions(-)

diff --git a/src/models/sparse/Dtmc.cpp b/src/models/sparse/Dtmc.cpp
index 733c8497c..c4853496a 100644
--- a/src/models/sparse/Dtmc.cpp
+++ b/src/models/sparse/Dtmc.cpp
@@ -3,8 +3,6 @@
 #include "src/adapters/CarlAdapter.h"
 #include "src/exceptions/NotImplementedException.h"
 #include "src/exceptions/InvalidArgumentException.h"
-#include "src/utility/constants.h"
-#include "src/utility/ConstantsComparator.h"
 
 namespace storm {
     namespace models {
@@ -16,14 +14,14 @@ namespace storm {
                  std::unordered_map<std::string, RewardModelType> const& rewardModels,
                  boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling)
             : DeterministicModel<ValueType>(storm::models::ModelType::Dtmc, probabilityMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) {
-                STORM_LOG_THROW(this->checkValidityOfProbabilityMatrix(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid.");
+                STORM_LOG_THROW(probabilityMatrix.isProbabilistic(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid.");
             }
             
             template <typename ValueType, typename RewardModelType>
             Dtmc<ValueType, RewardModelType>::Dtmc(storm::storage::SparseMatrix<ValueType>&& probabilityMatrix, storm::models::sparse::StateLabeling&& stateLabeling,
                 std::unordered_map<std::string, RewardModelType>&& rewardModels, boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling)
             : DeterministicModel<ValueType>(storm::models::ModelType::Dtmc, std::move(probabilityMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) {
-                STORM_LOG_THROW(this->checkValidityOfProbabilityMatrix(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid.");
+                STORM_LOG_THROW(probabilityMatrix.isProbabilistic(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid.");
             }
             
             template <typename ValueType, typename RewardModelType>
@@ -223,28 +221,6 @@ namespace storm {
             }
 #endif
             
-            template <typename ValueType, typename RewardModelType>
-            bool Dtmc<ValueType, RewardModelType>::checkValidityOfProbabilityMatrix() const {
-                if (this->getTransitionMatrix().getRowCount() != this->getTransitionMatrix().getColumnCount()) {
-                    return false;
-                }
-                
-                storm::utility::ConstantsComparator<ValueType> comparator;
-                for (uint_fast64_t row = 0; row < this->getTransitionMatrix().getRowCount(); ++row) {
-                    ValueType sum = this->getTransitionMatrix().getRowSum(row);
-                    
-                    // If the sum is not a constant, for example for parametric models, we cannot check whether the sum is one or not.
-                    if (!comparator.isConstant(sum)) {
-                        continue;
-                    }
-                    
-                    if (!comparator.isOne(sum)) {
-                        return false;
-                    }
-                }
-                return true;
-            }
-            
             template class Dtmc<double>;
             template class Dtmc<float>;
 
diff --git a/src/models/sparse/Dtmc.h b/src/models/sparse/Dtmc.h
index f5537a561..334422dba 100644
--- a/src/models/sparse/Dtmc.h
+++ b/src/models/sparse/Dtmc.h
@@ -107,14 +107,6 @@ namespace storm {
                     
                 };
 #endif
-
-            private:
-                /*!
-                 * Checks the probability matrix for validity.
-                 *
-                 * @return True iff the probability matrix is valid.
-                 */
-                bool checkValidityOfProbabilityMatrix() const;
             };
             
         } // namespace sparse
diff --git a/src/models/sparse/Mdp.cpp b/src/models/sparse/Mdp.cpp
index 7d26280df..0ba1e7c28 100644
--- a/src/models/sparse/Mdp.cpp
+++ b/src/models/sparse/Mdp.cpp
@@ -5,7 +5,6 @@
 #include "src/adapters/CarlAdapter.h"
 
 #include "src/models/sparse/StandardRewardModel.h"
-#include "src/utility/ConstantsComparator.h"
 
 namespace storm {
     namespace models {
@@ -17,7 +16,7 @@ namespace storm {
                                 std::unordered_map<std::string, RewardModelType> const& rewardModels,
                                 boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling)
             : NondeterministicModel<ValueType>(storm::models::ModelType::Mdp, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) {
-                STORM_LOG_THROW(this->checkValidityOfProbabilityMatrix(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid.");
+                STORM_LOG_THROW(transitionMatrix.isProbabilistic(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid.");
             }
             
             
@@ -27,7 +26,7 @@ namespace storm {
                                 std::unordered_map<std::string, RewardModelType>&& rewardModels,
                                 boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling)
             : NondeterministicModel<ValueType>(storm::models::ModelType::Mdp, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) {
-                STORM_LOG_THROW(this->checkValidityOfProbabilityMatrix(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid.");
+                STORM_LOG_THROW(transitionMatrix.isProbabilistic(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid.");
             }
             
             template <typename ValueType, typename RewardModelType>
@@ -85,25 +84,6 @@ namespace storm {
                 return Mdp<ValueType>(restrictedTransitions, this->getStateLabeling(), newRewardModels, this->getOptionalChoiceLabeling());
             }
             
-            template <typename ValueType, typename RewardModelType>
-            bool Mdp<ValueType, RewardModelType>::checkValidityOfProbabilityMatrix() const {
-                storm::utility::ConstantsComparator<ValueType> comparator;
-                // Get the settings object to customize linear solving.
-                for (uint_fast64_t row = 0; row < this->getTransitionMatrix().getRowCount(); row++) {
-                    ValueType sum = this->getTransitionMatrix().getRowSum(row);
-                    
-                    // If the sum is not a constant, for example for parametric models, we cannot check whether the sum is one or not.
-                    if (!comparator.isConstant(sum)) {
-                        continue;
-                    }
-                    
-                    if (!comparator.isOne(sum))  {
-                        return false;
-                    }
-                }
-                return true;
-            }
-            
             template class Mdp<double>;
             template class Mdp<float>;
 
diff --git a/src/models/sparse/Mdp.h b/src/models/sparse/Mdp.h
index 6cd6a3ec3..6354551f9 100644
--- a/src/models/sparse/Mdp.h
+++ b/src/models/sparse/Mdp.h
@@ -66,14 +66,6 @@ namespace storm {
                  * @return A subMDP.
                  */
                 Mdp<ValueType> restrictActions(storm::storage::BitVector const& enabledActions) const;
-                
-            private:
-                /*!
-                 * Checks the probability matrix for validity.
-                 *
-                 * @return True iff the probability matrix is valid.
-                 */
-                bool checkValidityOfProbabilityMatrix() const;
             };
             
         } // namespace sparse