From f44f0ce4108c76c34a3cdafbb54d156b711da2db Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 5 Jun 2013 13:13:45 +0200
Subject: [PATCH] Cleaned interfaces of models from std::shared_ptr. Improved
 some code in graph utility.

---
 src/modelchecker/prctl/AbstractModelChecker.h |  30 ++-
 .../prctl/SparseDtmcPrctlModelChecker.h       | 233 ++++++++++--------
 .../prctl/SparseMdpPrctlModelChecker.h        |  36 +--
 src/models/AbstractModel.h                    |  22 +-
 src/models/AbstractNondeterministicModel.h    |   4 +-
 src/models/Ctmdp.h                            |   4 +-
 src/models/Dtmc.h                             |  10 +-
 src/models/Mdp.h                              |   4 +-
 src/storage/BitVector.h                       |  27 +-
 src/storage/SparseMatrix.h                    |   2 +-
 src/utility/graph.h                           | 158 ++++++------
 test/functional/parser/ParseMdpTest.cpp       |   6 +-
 12 files changed, 291 insertions(+), 245 deletions(-)

diff --git a/src/modelchecker/prctl/AbstractModelChecker.h b/src/modelchecker/prctl/AbstractModelChecker.h
index 2ac3fd241..b3ae46bd2 100644
--- a/src/modelchecker/prctl/AbstractModelChecker.h
+++ b/src/modelchecker/prctl/AbstractModelChecker.h
@@ -86,7 +86,8 @@ public:
 
 	/*!
 	 * Returns a pointer to the model checker object that is of the requested type as given by the template parameters.
-	 * @returns A pointer to the model checker object that is of the requested type as given by the template parameters.
+     *
+	 * @return A pointer to the model checker object that is of the requested type as given by the template parameters.
 	 * If the model checker is not of the requested type, type casting will fail and result in an exception.
 	 */
 	template <template <class T> class Target>
@@ -105,7 +106,7 @@ public:
 	 * Retrieves the model associated with this model checker as a constant reference to an object of the type given
 	 * by the template parameter.
 	 *
-	 * @returns A constant reference of the specified type to the model associated with this model checker. If the model
+	 * @return A constant reference of the specified type to the model associated with this model checker. If the model
 	 * is not of the requested type, type casting will fail and result in an exception.
 	 */
 	template <class Model>
@@ -118,6 +119,15 @@ public:
 			throw bc;
 		}
 	}
+        
+    /*!
+     * Retrieves the initial states of the model.
+     *
+     * @return A bit vector that represents the initial states of the model.
+     */
+    storm::storage::BitVector const& getInitialStates() const {
+        return model.getLabeledStates("init");
+    }
 
 	/*!
 	 * Checks the given abstract prctl formula on the model and prints the result (depending on the actual type of the formula)
@@ -148,7 +158,7 @@ public:
 			result = stateFormula.check(*this);
 			LOG4CPLUS_INFO(logger, "Result for initial states:");
 			std::cout << "Result for initial states:" << std::endl;
-			for (auto initialState : model.getLabeledStates("init")) {
+			for (auto initialState : this->getInitialStates()) {
 				LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result->get(initialState) ? "satisfied" : "not satisfied"));
 				std::cout << "\t" << initialState << ": " << result->get(initialState) << std::endl;
 			}
@@ -178,7 +188,7 @@ public:
 			result = this->checkNoBoundOperator(noBoundFormula);
 			LOG4CPLUS_INFO(logger, "Result for initial states:");
 			std::cout << "Result for initial states:" << std::endl;
-			for (auto initialState : model.getLabeledStates("init")) {
+			for (auto initialState : this->getInitialStates()) {
 				LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (*result)[initialState]);
 				std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl;
 			}
@@ -196,7 +206,7 @@ public:
 	 * Checks the given formula consisting of a single atomic proposition.
 	 *
 	 * @param formula The formula to be checked.
-	 * @returns The set of states satisfying the formula represented by a bit vector.
+	 * @return The set of states satisfying the formula represented by a bit vector.
 	 */
 	storm::storage::BitVector* checkAp(storm::property::prctl::Ap<Type> const& formula) const {
 		if (formula.getAp() == "true") {
@@ -217,7 +227,7 @@ public:
 	 * Checks the given formula that is a logical "and" of two formulae.
 	 *
 	 * @param formula The formula to be checked.
-	 * @returns The set of states satisfying the formula represented by a bit vector.
+	 * @return The set of states satisfying the formula represented by a bit vector.
 	 */
 	storm::storage::BitVector* checkAnd(storm::property::prctl::And<Type> const& formula) const {
 		storm::storage::BitVector* result = formula.getLeft().check(*this);
@@ -231,7 +241,7 @@ public:
 	 * Checks the given formula that is a logical "or" of two formulae.
 	 *
 	 * @param formula The formula to check.
-	 * @returns The set of states satisfying the formula represented by a bit vector.
+	 * @return The set of states satisfying the formula represented by a bit vector.
 	 */
 	virtual storm::storage::BitVector* checkOr(storm::property::prctl::Or<Type> const& formula) const {
 		storm::storage::BitVector* result = formula.getLeft().check(*this);
@@ -245,7 +255,7 @@ public:
 	 * Checks the given formula that is a logical "not" of a sub-formula.
 	 *
 	 * @param formula The formula to check.
-	 * @returns The set of states satisfying the formula represented by a bit vector.
+	 * @return The set of states satisfying the formula represented by a bit vector.
 	 */
 	storm::storage::BitVector* checkNot(const storm::property::prctl::Not<Type>& formula) const {
 		storm::storage::BitVector* result = formula.getChild().check(*this);
@@ -258,7 +268,7 @@ public:
 	 * Checks the given formula that is a P operator over a path formula featuring a value bound.
 	 *
 	 * @param formula The formula to check.
-	 * @returns The set of states satisfying the formula represented by a bit vector.
+	 * @return The set of states satisfying the formula represented by a bit vector.
 	 */
 	storm::storage::BitVector* checkProbabilisticBoundOperator(storm::property::prctl::ProbabilisticBoundOperator<Type> const& formula) const {
 		// First, we need to compute the probability for satisfying the path formula for each state.
@@ -284,7 +294,7 @@ public:
 	 * Checks the given formula that is an R operator over a reward formula featuring a value bound.
 	 *
 	 * @param formula The formula to check.
-	 * @returns The set of states satisfying the formula represented by a bit vector.
+	 * @return The set of states satisfying the formula represented by a bit vector.
 	 */
 	storm::storage::BitVector* checkRewardBoundOperator(const storm::property::prctl::RewardBoundOperator<Type>& formula) const {
 		// First, we need to compute the probability for satisfying the path formula for each state.
diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
index 36f2ff9ee..5ab063ef7 100644
--- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
+++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
@@ -88,31 +88,40 @@ public:
 		// First, we need to compute the states that satisfy the sub-formulas of the bounded until-formula.
 		storm::storage::BitVector* leftStates = formula.getLeft().check(*this);
 		storm::storage::BitVector* rightStates = formula.getRight().check(*this);
-
+        std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
+        
         // If we identify the states that have probability 0 of reaching the target states, we can exclude them in the
         // further analysis.
-        storm::storage::BitVector maybeStates = storm::utility::graph::performProbGreater0(this->getModel(), *leftStates, *rightStates, true, formula.getBound());
-        
-        // Now we can eliminate the rows and columns from the original transition probability matrix that have probability 0.
-        storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates);
-        
-        // Compute the new set of target states in the reduced system.
-        storm::storage::BitVector rightStatesInReducedSystem = maybeStates % *rightStates;
+        storm::storage::BitVector statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(this->getModel(), *leftStates, *rightStates, true, formula.getBound());
+        LOG4CPLUS_INFO(logger, "Found " << statesWithProbabilityGreater0.getNumberOfSetBits() << " 'maybe' states.");
         
-		// Make all rows absorbing that satisfy the second sub-formula.
-		submatrix.makeRowsAbsorbing(rightStatesInReducedSystem);
-
-		// Create the vector with which to multiply.
-        std::vector<Type> subresult(maybeStates.getNumberOfSetBits());
-		storm::utility::vector::setVectorValues(subresult, rightStatesInReducedSystem, storm::utility::constGetOne<Type>());
-
-		// Perform the matrix vector multiplication as often as required by the formula bound.
-		this->performMatrixVectorMultiplication(submatrix, subresult, nullptr, formula.getBound());
-
-        // Create result vector and set its values accordingly.
-		std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
-        storm::utility::vector::setVectorValues(*result, maybeStates, subresult);
-        storm::utility::vector::setVectorValues<Type>(*result, ~maybeStates, storm::utility::constGetZero<Type>());
+        // Check if we already know the result (i.e. probability 0) for all initial states and
+        // don't compute anything in this case.
+        if (this->getInitialStates().isSubsetOf(~statesWithProbabilityGreater0)) {
+            LOG4CPLUS_INFO(logger, "The probabilities for the initial states were determined in a preprocessing step."
+                           << " No exact probabilities were computed.");
+        } else { // Otherwise, we have have to compute the probabilities.
+            // Now we can eliminate the rows and columns from the original transition probability matrix that have probability 0.
+            storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix().getSubmatrix(statesWithProbabilityGreater0);
+            
+            // Compute the new set of target states in the reduced system.
+            storm::storage::BitVector rightStatesInReducedSystem = statesWithProbabilityGreater0 % *rightStates;
+            
+            // Make all rows absorbing that satisfy the second sub-formula.
+            submatrix.makeRowsAbsorbing(rightStatesInReducedSystem);
+            
+            // Create the vector with which to multiply.
+            std::vector<Type> subresult(statesWithProbabilityGreater0.getNumberOfSetBits());
+            storm::utility::vector::setVectorValues(subresult, rightStatesInReducedSystem, storm::utility::constGetOne<Type>());
+            
+            // Perform the matrix vector multiplication as often as required by the formula bound.
+            this->performMatrixVectorMultiplication(submatrix, subresult, nullptr, formula.getBound());
+            
+            // Create result vector and set its values accordingly.
+
+            storm::utility::vector::setVectorValues(*result, statesWithProbabilityGreater0, subresult);
+            storm::utility::vector::setVectorValues<Type>(*result, ~statesWithProbabilityGreater0, storm::utility::constGetZero<Type>());
+        }
         
 		// Delete obsolete intermediates and return result.
 		delete leftStates;
@@ -143,7 +152,7 @@ public:
 		delete nextStates;
 
 		// Perform one single matrix-vector multiplication.
-		this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result);
+		this->performMatrixVectorMultiplication(this->getModel().getTransitionMatrix(), *result);
 
 		// Return result.
 		return result;
@@ -231,42 +240,49 @@ public:
 		delete rightStates;
 
 		// Perform some logging.
+        storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1);
 		LOG4CPLUS_INFO(logger, "Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states.");
 		LOG4CPLUS_INFO(logger, "Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states.");
-		storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1);
 		LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
 
 		// Create resulting vector.
 		std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
 
-		// Only try to solve system if there are states for which the probability is unknown.
-		uint_fast64_t maybeStatesSetBitCount = maybeStates.getNumberOfSetBits();
-		if (maybeStatesSetBitCount > 0 && !qualitative) {
-			// Now we can eliminate the rows and columns from the original transition probability matrix.
-			storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates);
-			// 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.
-			submatrix.convertToEquationSystem();
-
-			// Initialize the x vector with 0.5 for each element. This is the initial guess for
-			// the iterative solvers. It should be safe as for all 'maybe' states we know that the
-			// probability is strictly larger than 0.
-			std::vector<Type> x(maybeStatesSetBitCount, Type(0.5));
-
-			// 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<Type> b = this->getModel().getTransitionMatrix()->getConstrainedRowSumVector(maybeStates, statesWithProbability1);
-
-			// Now solve the created system of linear equations.
-			this->solveEquationSystem(submatrix, x, b);
-
-			// Set values of resulting vector according to result.
-			storm::utility::vector::setVectorValues<Type>(*result, maybeStates, x);
-		} else if (qualitative) {
-			// If we only need a qualitative result, we can safely assume that the results will only be compared to
-			// bounds which are either 0 or 1. Setting the value to 0.5 is thus safe.
-			storm::utility::vector::setVectorValues<Type>(*result, maybeStates, Type(0.5));
-		}
+        // Check whether we need to compute exact probabilities for some states.
+        if (this->getInitialStates().isDisjointFrom(maybeStates) || qualitative) {
+            if (qualitative) {
+                LOG4CPLUS_INFO(logger, "The formula was checked qualitatively. No exact probabilities were computed.");
+            } else {
+                LOG4CPLUS_INFO(logger, "The probabilities for the initial states were determined in a preprocessing step."
+                               << " No exact probabilities were computed.");
+            }
+            // Set the values for all maybe-states to 0.5 to indicate that their probability values
+            // are neither 0 nor 1.
+            storm::utility::vector::setVectorValues<Type>(*result, maybeStates, Type(0.5));
+        } else {
+            // Otherwise, we have have to compute the probabilities.
+            
+            // First, we can eliminate the rows and columns from the original transition probability matrix.
+            storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix().getSubmatrix(maybeStates);
+            // 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.
+            submatrix.convertToEquationSystem();
+            
+            // Initialize the x vector with 0.5 for each element. This is the initial guess for
+            // the iterative solvers. It should be safe as for all 'maybe' states we know that the
+            // probability is strictly larger than 0.
+            std::vector<Type> x(maybeStates.getNumberOfSetBits(), Type(0.5));
+            
+            // 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<Type> b = this->getModel().getTransitionMatrix().getConstrainedRowSumVector(maybeStates, statesWithProbability1);
+            
+            // Now solve the created system of linear equations.
+            this->solveEquationSystem(submatrix, x, b);
+            
+            // Set values of resulting vector according to result.
+            storm::utility::vector::setVectorValues<Type>(*result, maybeStates, x);
+        }
 
 		// Set values of resulting vector that are known exactly.
 		storm::utility::vector::setVectorValues<Type>(*result, statesWithProbability0, storm::utility::constGetZero<Type>());
@@ -294,10 +310,10 @@ public:
 		}
 
 		// Initialize result to state rewards of the model.
-		std::vector<Type>* result = new std::vector<Type>(*this->getModel().getStateRewardVector());
+		std::vector<Type>* result = new std::vector<Type>(this->getModel().getStateRewardVector());
 
 		// Perform the actual matrix-vector multiplication as long as the bound of the formula is met.
-		this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, nullptr, formula.getBound());
+		this->performMatrixVectorMultiplication(this->getModel().getTransitionMatrix(), *result, nullptr, formula.getBound());
 
 		// Return result.
 		return result;
@@ -324,24 +340,24 @@ public:
 		// Compute the reward vector to add in each step based on the available reward models.
 		std::vector<Type> totalRewardVector;
 		if (this->getModel().hasTransitionRewards()) {
-			totalRewardVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix());
+			totalRewardVector = this->getModel().getTransitionMatrix().getPointwiseProductRowSumVector(this->getModel().getTransitionRewardMatrix());
 			if (this->getModel().hasStateRewards()) {
-				gmm::add(*this->getModel().getStateRewardVector(), totalRewardVector);
+                storm::utility::vector::addVectorsInPlace(totalRewardVector, this->getModel().getStateRewardVector());
 			}
 		} else {
-			totalRewardVector = std::vector<Type>(*this->getModel().getStateRewardVector());
+			totalRewardVector = std::vector<Type>(this->getModel().getStateRewardVector());
 		}
 
 		// Initialize result to either the state rewards of the model or the null vector.
 		std::vector<Type>* result = nullptr;
 		if (this->getModel().hasStateRewards()) {
-			result = new std::vector<Type>(*this->getModel().getStateRewardVector());
+			result = new std::vector<Type>(this->getModel().getStateRewardVector());
 		} else {
 			result = new std::vector<Type>(this->getModel().getNumberOfStates());
 		}
 
 		// Perform the actual matrix-vector multiplication as long as the bound of the formula is met.
-		this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, &totalRewardVector, formula.getBound());
+		this->performMatrixVectorMultiplication(this->getModel().getTransitionMatrix(), *result, &totalRewardVector, formula.getBound());
 
 		// Return result.
 		return result;
@@ -372,56 +388,67 @@ public:
 		storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true);
 		storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(this->getModel(), trueStates, *targetStates);
 		infinityStates.complement();
+        LOG4CPLUS_INFO(logger, "Found " << infinityStates.getNumberOfSetBits() << " 'infinity' states.");
 
 		// Create resulting vector.
 		std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
 
 		// Check whether there are states for which we have to compute the result.
 		storm::storage::BitVector maybeStates = ~(*targetStates) & ~infinityStates;
-		const int maybeStatesSetBitCount = maybeStates.getNumberOfSetBits();
-		if (maybeStatesSetBitCount > 0) {
-			// Now we can eliminate the rows and columns from the original transition probability matrix.
-			storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates);
-			// 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.
-			submatrix.convertToEquationSystem();
-
-			// Initialize the x vector with 1 for each element. This is the initial guess for
-			// the iterative solvers.
-			std::vector<Type> x(maybeStatesSetBitCount, storm::utility::constGetOne<Type>());
-
-			// Prepare the right-hand side of the equation system.
-			std::vector<Type> b(maybeStatesSetBitCount);
-			if (this->getModel().hasTransitionRewards()) {
-				// 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<Type> pointwiseProductRowSumVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix());
-				storm::utility::vector::selectVectorValues(b, maybeStates, pointwiseProductRowSumVector);
-
-				if (this->getModel().hasStateRewards()) {
-					// 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<Type> subStateRewards(maybeStatesSetBitCount);
-					storm::utility::vector::selectVectorValues(subStateRewards, maybeStates, *this->getModel().getStateRewardVector());
-					gmm::add(subStateRewards, b);
-				}
-			} else {
-				// If only a state-based reward model is  available, we take this vector as the
-				// 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());
-			}
-
-			// Now solve the resulting equation system.
-			this->solveEquationSystem(submatrix, x, b);
-
-			// Set values of resulting vector according to result.
-			storm::utility::vector::setVectorValues<Type>(*result, maybeStates, x);
-		}
+        
+        // Check whether we need to compute exact rewards for some states.
+        if (this->getInitialStates().isDisjointFrom(maybeStates)) {
+            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<Type>(*result, maybeStates, storm::utility::constGetOne<Type>());
+        } else {
+            // In this case we have to compute the reward values for the remaining states.
+            const int maybeStatesSetBitCount = maybeStates.getNumberOfSetBits();
+
+            // Now we can eliminate the rows and columns from the original transition probability matrix.
+            storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix().getSubmatrix(maybeStates);
+            // 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.
+            submatrix.convertToEquationSystem();
+            
+            // Initialize the x vector with 1 for each element. This is the initial guess for
+            // the iterative solvers.
+            std::vector<Type> x(maybeStatesSetBitCount, storm::utility::constGetOne<Type>());
+            
+            // Prepare the right-hand side of the equation system.
+            std::vector<Type> b(maybeStatesSetBitCount);
+            if (this->getModel().hasTransitionRewards()) {
+                // 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<Type> pointwiseProductRowSumVector = this->getModel().getTransitionMatrix().getPointwiseProductRowSumVector(this->getModel().getTransitionRewardMatrix());
+                storm::utility::vector::selectVectorValues(b, maybeStates, pointwiseProductRowSumVector);
+                
+                if (this->getModel().hasStateRewards()) {
+                    // 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<Type> subStateRewards(maybeStatesSetBitCount);
+                    storm::utility::vector::selectVectorValues(subStateRewards, maybeStates, this->getModel().getStateRewardVector());
+                    storm::utility::vector::addVectorsInPlace(b, subStateRewards);
+                }
+            } else {
+                // If only a state-based reward model is  available, we take this vector as the
+                // 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());
+            }
+            
+            // Now solve the resulting equation system.
+            this->solveEquationSystem(submatrix, x, b);
+            
+            // Set values of resulting vector according to result.
+            storm::utility::vector::setVectorValues<Type>(*result, maybeStates, x);
+        }
 
 		// Set values of resulting vector that are known exactly.
 		storm::utility::vector::setVectorValues(*result, *targetStates, storm::utility::constGetZero<Type>());
diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
index 81c9b45e1..3611a70a2 100644
--- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
+++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
@@ -104,7 +104,7 @@ public:
 		}
         
         // Now we can eliminate the rows and columns from the original transition probability matrix that have probability 0.
-        storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates, *this->getModel().getNondeterministicChoiceIndices());
+        storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix().getSubmatrix(maybeStates, this->getModel().getNondeterministicChoiceIndices());
 
         // Get the "new" nondeterministic choice indices for the submatrix.
         std::vector<uint_fast64_t> subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates);
@@ -154,7 +154,7 @@ public:
 		// Delete obsolete sub-result.
 		delete nextStates;
 
-		this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, *this->getModel().getNondeterministicChoiceIndices());
+		this->performMatrixVectorMultiplication(this->getModel().getTransitionMatrix(), *result, this->getModel().getNondeterministicChoiceIndices());
 
 		// Return result.
 		return result;
@@ -259,7 +259,7 @@ public:
 		if (maybeStatesSetBitCount > 0) {
 			// First, we can eliminate the rows and columns from the original transition probability matrix for states
 			// whose probabilities are already known.
-			storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates, *this->getModel().getNondeterministicChoiceIndices());
+			storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix().getSubmatrix(maybeStates, this->getModel().getNondeterministicChoiceIndices());
 
 			// Get the "new" nondeterministic choice indices for the submatrix.
 			std::vector<uint_fast64_t> subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates);
@@ -269,7 +269,7 @@ public:
 
 			// 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<Type> b = this->getModel().getTransitionMatrix()->getConstrainedRowSumVector(maybeStates, *this->getModel().getNondeterministicChoiceIndices(), statesWithProbability1, submatrix.getRowCount());
+			std::vector<Type> b = this->getModel().getTransitionMatrix().getConstrainedRowSumVector(maybeStates, this->getModel().getNondeterministicChoiceIndices(), statesWithProbability1, submatrix.getRowCount());
 
 			// Solve the corresponding system of equations.
 			this->solveEquationSystem(submatrix, x, b, subNondeterministicChoiceIndices);
@@ -304,9 +304,9 @@ public:
 		}
 
 		// Initialize result to state rewards of the model.
-		std::vector<Type>* result = new std::vector<Type>(*this->getModel().getStateRewardVector());
+		std::vector<Type>* result = new std::vector<Type>(this->getModel().getStateRewardVector());
 
-		this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, *this->getModel().getNondeterministicChoiceIndices(), nullptr, formula.getBound());
+		this->performMatrixVectorMultiplication(this->getModel().getTransitionMatrix(), *result, this->getModel().getNondeterministicChoiceIndices(), nullptr, formula.getBound());
 
 		// Return result.
 		return result;
@@ -333,23 +333,23 @@ public:
 		// Compute the reward vector to add in each step based on the available reward models.
 		std::vector<Type> totalRewardVector;
 		if (this->getModel().hasTransitionRewards()) {
-			totalRewardVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix());
+			totalRewardVector = this->getModel().getTransitionMatrix().getPointwiseProductRowSumVector(this->getModel().getTransitionRewardMatrix());
 			if (this->getModel().hasStateRewards()) {
-				gmm::add(*this->getModel().getStateRewardVector(), totalRewardVector);
+                storm::utility::vector::addVectorsInPlace(totalRewardVector, this->getModel().getStateRewardVector());
 			}
 		} else {
-			totalRewardVector = std::vector<Type>(*this->getModel().getStateRewardVector());
+			totalRewardVector = std::vector<Type>(this->getModel().getStateRewardVector());
 		}
 
 		// Initialize result to either the state rewards of the model or the null vector.
 		std::vector<Type>* result = nullptr;
 		if (this->getModel().hasStateRewards()) {
-			result = new std::vector<Type>(*this->getModel().getStateRewardVector());
+			result = new std::vector<Type>(this->getModel().getStateRewardVector());
 		} else {
 			result = new std::vector<Type>(this->getModel().getNumberOfStates());
 		}
 
-		this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, *this->getModel().getNondeterministicChoiceIndices(), &totalRewardVector, formula.getBound());
+		this->performMatrixVectorMultiplication(this->getModel().getTransitionMatrix(), *result, this->getModel().getNondeterministicChoiceIndices(), &totalRewardVector, formula.getBound());
 
 		// Delete temporary variables and return result.
 		return result;
@@ -399,7 +399,7 @@ public:
 		if (maybeStatesSetBitCount > 0) {
 			// First, we can eliminate the rows and columns from the original transition probability matrix for states
 			// whose probabilities are already known.
-			storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates, *this->getModel().getNondeterministicChoiceIndices());
+			storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix().getSubmatrix(maybeStates, this->getModel().getNondeterministicChoiceIndices());
 
 			// Get the "new" nondeterministic choice indices for the submatrix.
 			std::vector<uint_fast64_t> subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates);
@@ -415,8 +415,8 @@ public:
 				// 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<Type> pointwiseProductRowSumVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix());
-				storm::utility::vector::selectVectorValues(b, maybeStates, *this->getModel().getNondeterministicChoiceIndices(), pointwiseProductRowSumVector);
+				std::vector<Type> pointwiseProductRowSumVector = this->getModel().getTransitionMatrix().getPointwiseProductRowSumVector(this->getModel().getTransitionRewardMatrix());
+				storm::utility::vector::selectVectorValues(b, maybeStates, this->getModel().getNondeterministicChoiceIndices(), pointwiseProductRowSumVector);
 
 				if (this->getModel().hasStateRewards()) {
 					// If a state-based reward model is also available, we need to add this vector
@@ -424,15 +424,15 @@ public:
 					// that we still consider (i.e. maybeStates), we need to extract these values
 					// first.
 					std::vector<Type> subStateRewards(b.size());
-					storm::utility::vector::selectVectorValuesRepeatedly(subStateRewards, maybeStates, *this->getModel().getNondeterministicChoiceIndices(), *this->getModel().getStateRewardVector());
-					gmm::add(subStateRewards, b);
+					storm::utility::vector::selectVectorValuesRepeatedly(subStateRewards, maybeStates, this->getModel().getNondeterministicChoiceIndices(), this->getModel().getStateRewardVector());
+					storm::utility::vector::addVectorsInPlace(b, subStateRewards);
 				}
 			} else {
 				// If only a state-based reward model is  available, we take this vector as the
 				// 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().getNondeterministicChoiceIndices(), *this->getModel().getStateRewardVector());
+				storm::utility::vector::selectVectorValuesRepeatedly(b, maybeStates, this->getModel().getNondeterministicChoiceIndices(), this->getModel().getStateRewardVector());
 			}
 
 			// Solve the corresponding system of equations.
@@ -573,7 +573,7 @@ private:
 	 */
 	std::vector<uint_fast64_t> computeNondeterministicChoiceIndicesForConstraint(storm::storage::BitVector const& constraint) const {
 		// First, get a reference to the full nondeterministic choice indices.
-		std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = *this->getModel().getNondeterministicChoiceIndices();
+		std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices();
 
 		// Reserve the known amount of slots for the resulting vector.
 		std::vector<uint_fast64_t> subNondeterministicChoiceIndices(constraint.getNumberOfSetBits() + 1);
diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h
index 5d99b0f8f..e632e7879 100644
--- a/src/models/AbstractModel.h
+++ b/src/models/AbstractModel.h
@@ -208,7 +208,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
 		 * @return The size of the state space of the model.
 		 */
 		virtual uint_fast64_t getNumberOfStates() const {
-			return this->getTransitionMatrix()->getColumnCount();
+			return this->getTransitionMatrix().getColumnCount();
 		}
 
 		/*!
@@ -216,7 +216,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
 		 * @return The number of (non-zero) transitions of the model.
 		 */
 		virtual uint_fast64_t getNumberOfTransitions() const {
-			return this->getTransitionMatrix()->getNonZeroEntryCount();
+			return this->getTransitionMatrix().getNonZeroEntryCount();
 		}
 
 		/*!
@@ -245,24 +245,24 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
 		 * @return A pointer to the matrix representing the transition probability
 		 * function.
 		 */
-		std::shared_ptr<storm::storage::SparseMatrix<T>> getTransitionMatrix() const {
-			return transitionMatrix;
+		storm::storage::SparseMatrix<T> const& getTransitionMatrix() const {
+			return *transitionMatrix;
 		}
 
 		/*!
 		 * Returns a pointer to the matrix representing the transition rewards.
 		 * @return A pointer to the matrix representing the transition rewards.
 		 */
-		std::shared_ptr<storm::storage::SparseMatrix<T>> getTransitionRewardMatrix() const {
-			return transitionRewardMatrix;
+		storm::storage::SparseMatrix<T> const& getTransitionRewardMatrix() const {
+			return *transitionRewardMatrix;
 		}
 
 		/*!
 		 * Returns a pointer to the vector representing the state rewards.
 		 * @return A pointer to the vector representing the state rewards.
 		 */
-		std::shared_ptr<std::vector<T>> getStateRewardVector() const {
-			return stateRewardVector;
+		std::vector<T> const& getStateRewardVector() const {
+			return *stateRewardVector;
 		}
 
 		/*!
@@ -277,8 +277,8 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
 		 * Returns the state labeling associated with this model.
 		 * @return The state labeling associated with this model.
 		 */
-		std::shared_ptr<storm::models::AtomicPropositionsLabeling> getStateLabeling() const {
-			return stateLabeling;
+		storm::models::AtomicPropositionsLabeling const& getStateLabeling() const {
+			return *stateLabeling;
 		}
 
 		/*!
@@ -323,7 +323,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
 			out << "Model type: \t\t" << this->getType() << std::endl;
 			out << "States: \t\t" << this->getNumberOfStates() << std::endl;
 			out << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl;
-			this->getStateLabeling()->printAtomicPropositionsInformationToStream(out);
+			this->getStateLabeling().printAtomicPropositionsInformationToStream(out);
 			out << "Size in memory: \t"
 				<< (this->getSizeInMemory())/1024 << " kbytes" << std::endl;
 			out << "-------------------------------------------------------------- "
diff --git a/src/models/AbstractNondeterministicModel.h b/src/models/AbstractNondeterministicModel.h
index b64359d2f..0aacc698b 100644
--- a/src/models/AbstractNondeterministicModel.h
+++ b/src/models/AbstractNondeterministicModel.h
@@ -73,8 +73,8 @@ class AbstractNondeterministicModel: public AbstractModel<T> {
 		 * @param the vector indicating which matrix rows represent non-deterministic choices
 		 * of a certain state.
 		 */
-		std::shared_ptr<std::vector<uint_fast64_t>> getNondeterministicChoiceIndices() const {
-			return nondeterministicChoiceIndices;
+		std::vector<uint_fast64_t> const& getNondeterministicChoiceIndices() const {
+			return *nondeterministicChoiceIndices;
 		}
     
         /*!
diff --git a/src/models/Ctmdp.h b/src/models/Ctmdp.h
index e693c70a1..0d6095ea6 100644
--- a/src/models/Ctmdp.h
+++ b/src/models/Ctmdp.h
@@ -84,8 +84,8 @@ private:
 		// Get the settings object to customize linear solving.
 		storm::settings::Settings* s = storm::settings::instance();
 		double precision = s->get<double>("precision");
-		for (uint_fast64_t row = 0; row < this->getTransitionMatrix()->getRowCount(); row++) {
-			T sum = this->getTransitionMatrix()->getRowSum(row);
+		for (uint_fast64_t row = 0; row < this->getTransitionMatrix().getRowCount(); row++) {
+			T sum = this->getTransitionMatrix().getRowSum(row);
 			if (sum == 0) continue;
 			if (std::abs(sum - 1) > precision) return false;
 		}
diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h
index 41e6bae8a..97399115d 100644
--- a/src/models/Dtmc.h
+++ b/src/models/Dtmc.h
@@ -49,8 +49,8 @@ public:
 			LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
 			throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
 		}
-		if (this->getTransitionRewardMatrix() != nullptr) {
-			if (!this->getTransitionRewardMatrix()->containsAllPositionsOf(*this->getTransitionMatrix())) {
+		if (this->hasTransitionRewards()) {
+			if (!this->getTransitionRewardMatrix().containsAllPositionsOf(this->getTransitionMatrix())) {
 				LOG4CPLUS_ERROR(logger, "Transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist.");
 				throw storm::exceptions::InvalidArgumentException() << "There are transition rewards for nonexistent transitions.";
 			}
@@ -89,14 +89,14 @@ private:
 		storm::settings::Settings* s = storm::settings::instance();
 		double precision = s->get<double>("precision");
 
-		if (this->getTransitionMatrix()->getRowCount() != this->getTransitionMatrix()->getColumnCount()) {
+		if (this->getTransitionMatrix().getRowCount() != this->getTransitionMatrix().getColumnCount()) {
 			// not square
 			LOG4CPLUS_ERROR(logger, "Probability matrix is not square.");
 			return false;
 		}
 
-		for (uint_fast64_t row = 0; row < this->getTransitionMatrix()->getRowCount(); ++row) {
-			T sum = this->getTransitionMatrix()->getRowSum(row);
+		for (uint_fast64_t row = 0; row < this->getTransitionMatrix().getRowCount(); ++row) {
+			T sum = this->getTransitionMatrix().getRowSum(row);
 			if (sum == 0) {
 				LOG4CPLUS_ERROR(logger, "Row " << row << " has sum 0");
 				return false;
diff --git a/src/models/Mdp.h b/src/models/Mdp.h
index 586de6e5e..b2a8d285f 100644
--- a/src/models/Mdp.h
+++ b/src/models/Mdp.h
@@ -86,8 +86,8 @@ private:
 		// Get the settings object to customize linear solving.
 		storm::settings::Settings* s = storm::settings::instance();
 		double precision = s->get<double>("precision");
-		for (uint_fast64_t row = 0; row < this->getTransitionMatrix()->getRowCount(); row++) {
-			T sum = this->getTransitionMatrix()->getRowSum(row);
+		for (uint_fast64_t row = 0; row < this->getTransitionMatrix().getRowCount(); row++) {
+			T sum = this->getTransitionMatrix().getRowSum(row);
 			if (sum == 0) continue;
 			if (std::abs(sum - 1) > precision)  {
 				return false;
diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h
index d412b2eb7..376555e3e 100644
--- a/src/storage/BitVector.h
+++ b/src/storage/BitVector.h
@@ -420,6 +420,7 @@ public:
 	 * Performs a logical "implies" with the given bit vector. In case the sizes of the bit vectors
 	 * do not match, only the matching portion is considered and the overlapping bits
 	 * are set to 0.
+     *
 	 * @param bv A reference to the bit vector to use for the operation.
 	 * @return A bit vector corresponding to the logical "implies" of the two bit vectors.
 	 */
@@ -439,14 +440,15 @@ public:
 	/*!
 	 * Checks whether all bits that are set in the current bit vector are also set in the given bit
 	 * vector.
+     *
 	 * @param bv A reference to the bit vector whose bits are (possibly) a superset of the bits of
 	 * the current bit vector.
-	 * @returns True iff all bits that are set in the current bit vector are also set in the given bit
+	 * @return True iff all bits that are set in the current bit vector are also set in the given bit
 	 * vector.
 	 */
-	bool isContainedIn(BitVector const& bv) const {
+	bool isSubsetOf(BitVector const& bv) const {
 		for (uint_fast64_t i = 0; i < this->bucketCount; ++i) {
-			if ((this->bucketArray[i] & bv.bucketArray[i]) != bv.bucketArray[i]) {
+			if ((this->bucketArray[i] & bv.bucketArray[i]) != this->bucketArray[i]) {
 				return false;
 			}
 		}
@@ -456,6 +458,7 @@ public:
 	/*!
 	 * Checks whether none of the bits that are set in the current bit vector are also set in the
 	 * given bit vector.
+     *
 	 * @param bv A reference to the bit vector whose bits are (possibly) disjoint from the bits in
 	 * the current bit vector.
 	 * @returns True iff none of the bits that are set in the current bit vector are also set in the
@@ -504,9 +507,25 @@ public:
         
 		return result;
 	}
+    
+    /*!
+     * Returns a list containing all indices such that the bits at these indices are set to true
+     * in the bit vector.
+     *
+     * @return A vector of indices of set bits in the bit vector.
+     */
+    std::vector<uint_fast64_t> getSetIndicesList() const {
+        std::vector<uint_fast64_t> result;
+        result.reserve(this->getNumberOfSetBits());
+        for (auto index : *this) {
+			result.push_back(index);
+		}
+        return result;
+    }
 
 	/*!
-	 * Adds all indices of bits set to one to the provided list.
+	 * Adds all indices of bits set to one to the given list.
+     *
 	 * @param list The list to which to append the indices.
 	 */
 	void addSetIndicesToVector(std::vector<uint_fast64_t>& vector) const {
diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h
index 4ee005881..96d56424e 100644
--- a/src/storage/SparseMatrix.h
+++ b/src/storage/SparseMatrix.h
@@ -920,7 +920,7 @@ public:
 	 * @returns A vector containing the sum of the elements in each row of the matrix resulting from
 	 * pointwise multiplication of the current matrix with the given matrix.
 	 */
-	std::vector<T> getPointwiseProductRowSumVector(storm::storage::SparseMatrix<T> const& otherMatrix) {
+	std::vector<T> getPointwiseProductRowSumVector(storm::storage::SparseMatrix<T> const& otherMatrix) const {
 		// Prepare result.
 		std::vector<T> result(rowCount, storm::utility::constGetZero<T>());
 
diff --git a/src/utility/graph.h b/src/utility/graph.h
index 8d9f0f024..4d67f35ac 100644
--- a/src/utility/graph.h
+++ b/src/utility/graph.h
@@ -46,10 +46,8 @@ namespace graph {
 		// Add all psi states as the already satisfy the condition.
 		statesWithProbabilityGreater0 |= psiStates;
 
-		// Initialize the stack used for the BFS with the states.
-		std::vector<uint_fast64_t> stack;
-		stack.reserve(model.getNumberOfStates());
-		psiStates.addSetIndicesToVector(stack);
+		// Initialize the stack used for the DFS with the states.
+		std::vector<uint_fast64_t> stack = psiStates.getSetIndicesList();
         
         // Initialize the stack for the step bound, if the number of steps is bounded.
         std::vector<uint_fast64_t> stepStack;
@@ -63,7 +61,7 @@ namespace graph {
             }
         }
 
-		// Perform the actual BFS.
+		// Perform the actual DFS.
         uint_fast64_t currentState, currentStepBound;
 		while (!stack.empty()) {
             currentState = stack.back();
@@ -74,17 +72,17 @@ namespace graph {
                 stepStack.pop_back();
             }
 
-			for (auto it = backwardTransitions.constColumnIteratorBegin(currentState); it != backwardTransitions.constColumnIteratorEnd(currentState); ++it) {
-				if (phiStates.get(*it) && (!statesWithProbabilityGreater0.get(*it) || (useStepBound && remainingSteps[*it] < currentStepBound - 1))) {
-                    // If we don't have a number of maximal steps to take, just add the state to the stack.
+			for (auto predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) {
+				if (phiStates.get(*predecessorIt) && (!statesWithProbabilityGreater0.get(*predecessorIt) || (useStepBound && remainingSteps[*predecessorIt] < currentStepBound - 1))) {
+                    // If we don't have a bound on the number of steps to take, just add the state to the stack.
                     if (!useStepBound) {
-                        statesWithProbabilityGreater0.set(*it, true);
-                        stack.push_back(*it);
+                        statesWithProbabilityGreater0.set(*predecessorIt, true);
+                        stack.push_back(*predecessorIt);
                     } else if (currentStepBound > 0) {
                         // If there is at least one more step to go, we need to push the state and the new number of steps.
-                        remainingSteps[*it] = currentStepBound - 1;
-                        statesWithProbabilityGreater0.set(*it, true);
-                        stack.push_back(*it);
+                        remainingSteps[*predecessorIt] = currentStepBound - 1;
+                        statesWithProbabilityGreater0.set(*predecessorIt, true);
+                        stack.push_back(*predecessorIt);
                         stepStack.push_back(currentStepBound - 1);
                     }
 				}
@@ -174,17 +172,11 @@ namespace graph {
         // Prepare resulting bit vector.
         storm::storage::BitVector statesWithProbabilityGreater0(model.getNumberOfStates());
         
-		// Get some temporaries for convenience.
-		std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix = model.getTransitionMatrix();
-		std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices();
-        
 		// Add all psi states as the already satisfy the condition.
 		statesWithProbabilityGreater0 |= psiStates;
         
-		// Initialize the stack used for the BFS with the states
-		std::vector<uint_fast64_t> stack;
-		stack.reserve(model.getNumberOfStates());
-		psiStates.addSetIndicesToVector(stack);
+		// Initialize the stack used for the DFS with the states
+		std::vector<uint_fast64_t> stack = psiStates.getSetIndicesList();
         
         // Initialize the stack for the step bound, if the number of steps is bounded.
         std::vector<uint_fast64_t> stepStack;
@@ -198,7 +190,7 @@ namespace graph {
             }
         }
         
-		// Perform the actual BFS.
+		// Perform the actual DFS.
         uint_fast64_t currentState, currentStepBound;
 		while (!stack.empty()) {
 			currentState = stack.back();
@@ -209,17 +201,17 @@ namespace graph {
                 stepStack.pop_back();
             }
             
-			for (auto it = backwardTransitions.constColumnIteratorBegin(currentState), ite = backwardTransitions.constColumnIteratorEnd(currentState); it != ite; ++it) {
-                if (phiStates.get(*it) && (!statesWithProbabilityGreater0.get(*it) || (useStepBound && remainingSteps[*it] < currentStepBound - 1))) {
+			for (auto predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) {
+                if (phiStates.get(*predecessorIt) && (!statesWithProbabilityGreater0.get(*predecessorIt) || (useStepBound && remainingSteps[*predecessorIt] < currentStepBound - 1))) {
                     // If we don't have a bound on the number of steps to take, just add the state to the stack.
                     if (!useStepBound) {
-                        statesWithProbabilityGreater0.set(*it, true);
-                        stack.push_back(*it);
+                        statesWithProbabilityGreater0.set(*predecessorIt, true);
+                        stack.push_back(*predecessorIt);
                     } else if (currentStepBound > 0) {
                         // If there is at least one more step to go, we need to push the state and the new number of steps.
-                        remainingSteps[*it] = currentStepBound - 1;
-                        statesWithProbabilityGreater0.set(*it, true);
-                        stack.push_back(*it);
+                        remainingSteps[*predecessorIt] = currentStepBound - 1;
+                        statesWithProbabilityGreater0.set(*predecessorIt, true);
+                        stack.push_back(*predecessorIt);
                         stepStack.push_back(currentStepBound - 1);
                     }
                 }
@@ -265,11 +257,11 @@ namespace graph {
 	template <typename T>
 	storm::storage::BitVector performProb1E(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::SparseMatrix<bool> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
         // Get some temporaries for convenience.
-		std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix = model.getTransitionMatrix();
-		std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices();
+        storm::storage::SparseMatrix<T> const& transitionMatrix = model.getTransitionMatrix();
+		std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices();
 
+        // Initialize the environment for the iterative algorithm.
 		storm::storage::BitVector currentStates(model.getNumberOfStates(), true);
-
 		std::vector<uint_fast64_t> stack;
 		stack.reserve(model.getNumberOfStates());
 
@@ -285,14 +277,14 @@ namespace graph {
 				currentState = stack.back();
 				stack.pop_back();
 
-				for(auto it = backwardTransitions.constColumnIteratorBegin(currentState), ite = backwardTransitions.constColumnIteratorEnd(currentState); it != ite; ++it) {
-					if (phiStates.get(*it) && !nextStates.get(*it)) {
+				for(auto predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) {
+					if (phiStates.get(*predecessorIt) && !nextStates.get(*predecessorIt)) {
 						// Check whether the predecessor has only successors in the current state set for one of the
 						// nondeterminstic choices.
-						for (uint_fast64_t row = (*nondeterministicChoiceIndices)[*it]; row < (*nondeterministicChoiceIndices)[*it + 1]; ++row) {
+						for (auto row = nondeterministicChoiceIndices[*predecessorIt]; row < nondeterministicChoiceIndices[*predecessorIt + 1]; ++row) {
 							bool allSuccessorsInCurrentStates = true;
-							for (auto colIt = transitionMatrix->constColumnIteratorBegin(row); colIt != transitionMatrix->constColumnIteratorEnd(row); ++colIt) {
-								if (!currentStates.get(*colIt)) {
+							for (auto targetIt = transitionMatrix.constColumnIteratorBegin(row), targetIte = transitionMatrix.constColumnIteratorEnd(row); targetIt != targetIte; ++targetIt) {
+								if (!currentStates.get(*targetIt)) {
 									allSuccessorsInCurrentStates = false;
 									break;
 								}
@@ -302,8 +294,8 @@ namespace graph {
 							// add it to the set of states for the next iteration and perform a backward search from
 							// that state.
 							if (allSuccessorsInCurrentStates) {
-								nextStates.set(*it, true);
-								stack.push_back(*it);
+								nextStates.set(*predecessorIt, true);
+								stack.push_back(*predecessorIt);
 								break;
 							}
 						}
@@ -364,16 +356,14 @@ namespace graph {
         storm::storage::BitVector statesWithProbabilityGreater0(model.getNumberOfStates());
         
 		// Get some temporaries for convenience.
-		std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix = model.getTransitionMatrix();
-		std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices();
+        storm::storage::SparseMatrix<T> const& transitionMatrix = model.getTransitionMatrix();
+		std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices();
         
 		// Add all psi states as the already satisfy the condition.
 		statesWithProbabilityGreater0 |= psiStates;
         
-		// Initialize the stack used for the BFS with the states
-		std::vector<uint_fast64_t> stack;
-		stack.reserve(model.getNumberOfStates());
-		psiStates.addSetIndicesToVector(stack);
+		// Initialize the stack used for the DFS with the states
+		std::vector<uint_fast64_t> stack = psiStates.getSetIndicesList();
         
         // Initialize the stack for the step bound, if the number of steps is bounded.
         std::vector<uint_fast64_t> stepStack;
@@ -387,7 +377,7 @@ namespace graph {
             }
         }
         
-		// Perform the actual BFS.
+		// Perform the actual DFS.
         uint_fast64_t currentState, currentStepBound;
 		while(!stack.empty()) {
 			currentState = stack.back();
@@ -398,15 +388,15 @@ namespace graph {
                 stepStack.pop_back();
             }
             
-			for(auto it = backwardTransitions.constColumnIteratorBegin(currentState), ite = backwardTransitions.constColumnIteratorEnd(currentState); it != ite; ++it) {
-                if (phiStates.get(*it) && (!statesWithProbabilityGreater0.get(*it) || (useStepBound && remainingSteps[*it] < currentStepBound - 1))) {
+			for(auto predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) {
+                if (phiStates.get(*predecessorIt) && (!statesWithProbabilityGreater0.get(*predecessorIt) || (useStepBound && remainingSteps[*predecessorIt] < currentStepBound - 1))) {
                     // Check whether the predecessor has at least one successor in the current state set for every
                     // nondeterministic choice.
                     bool addToStatesWithProbabilityGreater0 = true;
-                    for (auto rowIt = nondeterministicChoiceIndices->begin() + *it; rowIt != nondeterministicChoiceIndices->begin() + *it + 1; ++rowIt) {
+                    for (auto row = nondeterministicChoiceIndices[*predecessorIt]; row < nondeterministicChoiceIndices[*predecessorIt + 1]; ++row) {
                         bool hasAtLeastOneSuccessorWithProbabilityGreater0 = false;
-                        for (auto colIt = transitionMatrix->constColumnIteratorBegin(*rowIt); colIt != transitionMatrix->constColumnIteratorEnd(*rowIt); ++colIt) {
-                            if (statesWithProbabilityGreater0.get(*colIt)) {
+                        for (auto successorIt = transitionMatrix.constColumnIteratorBegin(row), successorIte = transitionMatrix.constColumnIteratorEnd(row); successorIt != successorIte; ++successorIt) {
+                            if (statesWithProbabilityGreater0.get(*successorIt)) {
                                 hasAtLeastOneSuccessorWithProbabilityGreater0 = true;
                                 break;
                             }
@@ -422,13 +412,13 @@ namespace graph {
                     if (addToStatesWithProbabilityGreater0) {
                         // If we don't have a bound on the number of steps to take, just add the state to the stack.
                         if (!useStepBound) {
-                            statesWithProbabilityGreater0.set(*it, true);
-                            stack.push_back(*it);
+                            statesWithProbabilityGreater0.set(*predecessorIt, true);
+                            stack.push_back(*predecessorIt);
                         } else if (currentStepBound > 0) {
                             // If there is at least one more step to go, we need to push the state and the new number of steps.
-                            remainingSteps[*it] = currentStepBound - 1;
-                            statesWithProbabilityGreater0.set(*it, true);
-                            stack.push_back(*it);
+                            remainingSteps[*predecessorIt] = currentStepBound - 1;
+                            statesWithProbabilityGreater0.set(*predecessorIt, true);
+                            stack.push_back(*predecessorIt);
                             stepStack.push_back(currentStepBound - 1);
                         }
                     }
@@ -473,8 +463,8 @@ namespace graph {
 	template <typename T>
 	storm::storage::BitVector performProb1A(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::SparseMatrix<bool> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
 		// Get some temporaries for convenience.
-		std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix = model.getTransitionMatrix();
-		std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices();
+        storm::storage::SparseMatrix<T> const& transitionMatrix = model.getTransitionMatrix();
+		std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices();
 
         // Initialize the environment for the iterative algorithm.
 		storm::storage::BitVector currentStates(model.getNumberOfStates(), true);
@@ -493,14 +483,14 @@ namespace graph {
 				currentState = stack.back();
 				stack.pop_back();
 
-				for(auto it = backwardTransitions.constColumnIteratorBegin(currentState), ite = backwardTransitions.constColumnIteratorEnd(currentState); it != ite; ++it) {
-					if (phiStates.get(*it) && !nextStates.get(*it)) {
+				for(auto predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) {
+					if (phiStates.get(*predecessorIt) && !nextStates.get(*predecessorIt)) {
 						// Check whether the predecessor has only successors in the current state set for all of the
 						// nondeterminstic choices.
 						bool allSuccessorsInCurrentStatesForAllChoices = true;
-						for (uint_fast64_t row = (*nondeterministicChoiceIndices)[*it]; row < (*nondeterministicChoiceIndices)[*it + 1]; ++row) {
-							for (auto colIt = transitionMatrix->constColumnIteratorBegin(row); colIt != transitionMatrix->constColumnIteratorEnd(row); ++colIt) {
-								if (!currentStates.get(*colIt)) {
+						for (auto row = nondeterministicChoiceIndices[*predecessorIt]; row < nondeterministicChoiceIndices[*predecessorIt + 1]; ++row) {
+							for (auto successorIt = transitionMatrix.constColumnIteratorBegin(row), successorIte = transitionMatrix.constColumnIteratorEnd(row); successorIt != successorIte; ++successorIt) {
+								if (!currentStates.get(*successorIt)) {
 									allSuccessorsInCurrentStatesForAllChoices = false;
 									goto afterCheckLoop;
 								}
@@ -512,8 +502,8 @@ namespace graph {
 						// add it to the set of states for the next iteration and perform a backward search from
 						// that state.
 						if (allSuccessorsInCurrentStatesForAllChoices) {
-							nextStates.set(*it, true);
-							stack.push_back(*it);
+							nextStates.set(*predecessorIt, true);
+							stack.push_back(*predecessorIt);
 						}
 					}
 				}
@@ -584,7 +574,7 @@ namespace graph {
     recursionStepForward:
 		while (!recursionStateStack.empty()) {
 			uint_fast64_t currentState = recursionStateStack.back();
-			typename storm::storage::SparseMatrix<T>::ConstIndexIterator currentIt = recursionIteratorStack.back();
+			typename storm::storage::SparseMatrix<T>::ConstIndexIterator successorIt = recursionIteratorStack.back();
             
 			// Perform the treatment of newly discovered state as defined by Tarjan's algorithm
 			visitedStates.set(currentState, true);
@@ -595,29 +585,29 @@ namespace graph {
 			tarjanStackStates.set(currentState, true);
             
 			// Now, traverse all successors of the current state.
-			for(; currentIt != matrix.constColumnIteratorEnd(currentState); ++currentIt) {
+			for(; successorIt != matrix.constColumnIteratorEnd(currentState); ++successorIt) {
 				// If we have not visited the successor already, we need to perform the procedure
 				// recursively on the newly found state.
-				if (!visitedStates.get(*currentIt)) {
+				if (!visitedStates.get(*successorIt)) {
 					// Save current iterator position so we can continue where we left off later.
 					recursionIteratorStack.pop_back();
-					recursionIteratorStack.push_back(currentIt);
+					recursionIteratorStack.push_back(successorIt);
                     
 					// Put unvisited successor on top of our recursion stack and remember that.
-					recursionStateStack.push_back(*currentIt);
-					statesInStack[*currentIt] = true;
+					recursionStateStack.push_back(*successorIt);
+					statesInStack[*successorIt] = true;
                     
 					// Also, put initial value for iterator on corresponding recursion stack.
-					recursionIteratorStack.push_back(matrix.constColumnIteratorBegin(*currentIt));
+					recursionIteratorStack.push_back(matrix.constColumnIteratorBegin(*successorIt));
                     
 					// Perform the actual recursion step in an iterative way.
 					goto recursionStepForward;
                     
                 recursionStepBackward:
-					lowlinks[currentState] = std::min(lowlinks[currentState], lowlinks[*currentIt]);
-				} else if (tarjanStackStates.get(*currentIt)) {
+					lowlinks[currentState] = std::min(lowlinks[currentState], lowlinks[*successorIt]);
+				} else if (tarjanStackStates.get(*successorIt)) {
 					// Update the lowlink of the current state.
-					lowlinks[currentState] = std::min(lowlinks[currentState], stateIndices[*currentIt]);
+					lowlinks[currentState] = std::min(lowlinks[currentState], stateIndices[*successorIt]);
 				}
 			}
             
@@ -648,7 +638,7 @@ namespace graph {
 			// original recursive call.
 			if (recursionStateStack.size() > 0) {
 				currentState = recursionStateStack.back();
-				currentIt = recursionIteratorStack.back();
+				successorIt = recursionIteratorStack.back();
                 
 				goto recursionStepBackward;
 			}
@@ -680,7 +670,7 @@ namespace graph {
         uint_fast64_t currentIndex = 0;
         for (uint_fast64_t state = 0; state < numberOfStates; ++state) {
             if (!visitedStates.get(state)) {
-                performSccDecompositionHelper(state, currentIndex, stateIndices, lowlinks, tarjanStack, tarjanStackStates, visitedStates, *model.getTransitionMatrix(), scc);
+                performSccDecompositionHelper(state, currentIndex, stateIndices, lowlinks, tarjanStack, tarjanStackStates, visitedStates, model.getTransitionMatrix(), scc);
             }
         }
 
@@ -723,22 +713,22 @@ namespace graph {
 				recursionStepForward:
 				while (!recursionStack.empty()) {
 					uint_fast64_t currentState = recursionStack.back();
-					typename storm::storage::SparseMatrix<T>::ConstIndexIterator currentIt = iteratorRecursionStack.back();
+					typename storm::storage::SparseMatrix<T>::ConstIndexIterator successorIt = iteratorRecursionStack.back();
 
 					visitedStates.set(currentState, true);
 
 					recursionStepBackward:
-					for (; currentIt != matrix.constColumnIteratorEnd(currentState); ++currentIt) {
-						if (!visitedStates.get(*currentIt)) {
+					for (; successorIt != matrix.constColumnIteratorEnd(currentState); ++successorIt) {
+						if (!visitedStates.get(*successorIt)) {
 							// Put unvisited successor on top of our recursion stack and remember that.
-							recursionStack.push_back(*currentIt);
+							recursionStack.push_back(*successorIt);
 
 							// Save current iterator position so we can continue where we left off later.
 							iteratorRecursionStack.pop_back();
-							iteratorRecursionStack.push_back(currentIt + 1);
+							iteratorRecursionStack.push_back(successorIt + 1);
 
 							// Also, put initial value for iterator on corresponding recursion stack.
-							iteratorRecursionStack.push_back(matrix.constColumnIteratorBegin(*currentIt));
+							iteratorRecursionStack.push_back(matrix.constColumnIteratorBegin(*successorIt));
 
 							goto recursionStepForward;
 						}
@@ -756,7 +746,7 @@ namespace graph {
 					// original recursive call.
 					if (recursionStack.size() > 0) {
 						currentState = recursionStack.back();
-						currentIt = iteratorRecursionStack.back();
+						successorIt = iteratorRecursionStack.back();
 
 						goto recursionStepBackward;
 					}
diff --git a/test/functional/parser/ParseMdpTest.cpp b/test/functional/parser/ParseMdpTest.cpp
index dfaa0ac15..a379e82c2 100644
--- a/test/functional/parser/ParseMdpTest.cpp
+++ b/test/functional/parser/ParseMdpTest.cpp
@@ -17,12 +17,12 @@ TEST(ParseMdpTest, parseAndOutput) {
 			STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/pctl_general_input_01.lab"));
 
 	std::shared_ptr<storm::models::Mdp<double>> mdp = mdpParser->getMdp();
-	std::shared_ptr<storm::storage::SparseMatrix<double>> matrix = mdp->getTransitionMatrix();
+	storm::storage::SparseMatrix<double> const& matrix = mdp->getTransitionMatrix();
 
 	ASSERT_EQ(mdp->getNumberOfStates(), (uint_fast64_t)3);
 	ASSERT_EQ(mdp->getNumberOfTransitions(), (uint_fast64_t)11);
-	ASSERT_EQ(matrix->getRowCount(), (uint_fast64_t)(2 * 3));
-	ASSERT_EQ(matrix->getColumnCount(), (uint_fast64_t)3);
+	ASSERT_EQ(matrix.getRowCount(), (uint_fast64_t)(2 * 3));
+	ASSERT_EQ(matrix.getColumnCount(), (uint_fast64_t)3);
 	
 
 	delete mdpParser;