From dbd6c02f6a77169f8462e5a07ecd865d494183f9 Mon Sep 17 00:00:00 2001
From: PBerger <philipp.berger@rwth-aachen.de>
Date: Sat, 9 Feb 2013 18:34:53 +0100
Subject: [PATCH 1/8] Updated CMakeLists.txt, Cotire Usage is now restricted to
 Linux/Windows and deactivated on APPLE systems.

---
 CMakeLists.txt | 48 ++++++++++++++++++++++++++++++++----------------
 1 file changed, 32 insertions(+), 16 deletions(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index b19636778..0ffe20f22 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -152,14 +152,24 @@ add_executable(storm-tests ${STORM_TEST_SOURCES} ${STORM_TEST_HEADERS})
 target_link_libraries(storm ${Boost_LIBRARIES})   
 target_link_libraries(storm-tests ${Boost_LIBRARIES})
 
-# Include Cotire for PCH Generation
-set (CMAKE_MODULE_PATH "${CMAKE_SOURCE_DIR}/resources/cmake")
-include(cotire)
-
-cotire(storm)
-target_link_libraries(storm_unity ${Boost_LIBRARIES})
-#cotire(storm-tests)
-
+set (STORM_USE_COTIRE ON)
+if (APPLE)
+	set(STORM_USE_COTIRE OFF)
+endif(APPLE)
+
+# Print Cotire Usage Status
+message (STATUS "Using Cotire: ${STORM_USE_COTIRE}")
+
+if (STORM_USE_COTIRE)
+	# Include Cotire for PCH Generation
+	set (CMAKE_MODULE_PATH "${CMAKE_SOURCE_DIR}/resources/cmake")
+	include(cotire)
+
+	cotire(storm)
+	target_link_libraries(storm_unity ${Boost_LIBRARIES})
+	#cotire(storm-tests)
+endif()
+	
 # Add a target to generate API documentation with Doxygen
 if(DOXYGEN_FOUND)
     set(CMAKE_DOXYGEN_OUTPUT_DIR "${CMAKE_CURRENT_BINARY_DIR}/doc")
@@ -187,27 +197,33 @@ endif(GTEST_INCLUDE_DIR)
 if (LOG4CPLUS_INCLUDE_DIR)
     include_directories(${LOG4CPLUS_INCLUDE_DIR})
     target_link_libraries(storm ${LOG4CPLUS_LIBRARIES}) 
-	target_link_libraries(storm_unity ${LOG4CPLUS_LIBRARIES})
+	if (STORM_USE_COTIRE)
+		target_link_libraries(storm_unity ${LOG4CPLUS_LIBRARIES})
+	endif(STORM_USE_COTIRE)
     target_link_libraries(storm-tests ${LOG4CPLUS_LIBRARIES})
     # On Linux, we have to link against librt
     if (UNIX AND NOT APPLE)
-	   target_link_libraries(storm rt)
-	   target_link_libraries(storm_unity rt)
-	   target_link_libraries(storm-tests rt)
+		target_link_libraries(storm rt)
+		if (STORM_USE_COTIRE)
+			target_link_libraries(storm_unity rt)
+		endif(STORM_USE_COTIRE)
+		target_link_libraries(storm-tests rt)
     endif(UNIX AND NOT APPLE)
 endif(LOG4CPLUS_INCLUDE_DIR)
 
 if (THREADS_FOUND)
 	include_directories(${THREADS_INCLUDE_DIRS})
-    target_link_libraries(storm ${CMAKE_THREAD_LIBS_INIT})
-	target_link_libraries(storm_unity ${CMAKE_THREAD_LIBS_INIT})
+	target_link_libraries(storm ${CMAKE_THREAD_LIBS_INIT})
+	if (STORM_USE_COTIRE)
+		target_link_libraries(storm_unity ${CMAKE_THREAD_LIBS_INIT})
+	endif(STORM_USE_COTIRE)
 	target_link_libraries(storm-tests ${CMAKE_THREAD_LIBS_INIT})
 endif(THREADS_FOUND)
 
 # Configure a header file to pass some of the CMake settings to the source code
 configure_file (
-  "${PROJECT_SOURCE_DIR}/storm-config.h.in"
-  "${PROJECT_BINARY_DIR}/storm-config.h"
+	"${PROJECT_SOURCE_DIR}/storm-config.h.in"
+	"${PROJECT_BINARY_DIR}/storm-config.h"
 )
 
 add_custom_target(memcheck valgrind --leak-check=full --show-reachable=yes ${PROJECT_BINARY_DIR}/storm -v --fix-deadlocks ${PROJECT_SOURCE_DIR}/examples/dtmc/crowds/crowds5_5.tra examples/dtmc/crowds/crowds5_5.lab

From c02271a36ae43873a6c200962f5bb2b00348ad26 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Sun, 10 Feb 2013 13:55:37 +0100
Subject: [PATCH 2/8] Fixed typo in CTMC class. Moved GraphAnalyzer to utility.

---
 src/modelchecker/EigenDtmcPrctlModelChecker.h |  4 ++--
 src/modelchecker/GmmxxDtmcPrctlModelChecker.h |  6 +++---
 src/models/Ctmc.h                             |  2 +-
 src/storm.cpp                                 |  1 -
 src/{solver => utility}/GraphAnalyzer.h       | 10 +++++-----
 5 files changed, 11 insertions(+), 12 deletions(-)
 rename src/{solver => utility}/GraphAnalyzer.h (97%)

diff --git a/src/modelchecker/EigenDtmcPrctlModelChecker.h b/src/modelchecker/EigenDtmcPrctlModelChecker.h
index a7b749129..61867620d 100644
--- a/src/modelchecker/EigenDtmcPrctlModelChecker.h
+++ b/src/modelchecker/EigenDtmcPrctlModelChecker.h
@@ -12,7 +12,7 @@
 
 #include "src/models/Dtmc.h"
 #include "src/modelchecker/DtmcPrctlModelChecker.h"
-#include "src/solver/GraphAnalyzer.h"
+#include "src/utility/GraphAnalyzer.h"
 #include "src/utility/ConstTemplates.h"
 #include "src/exceptions/NoConvergenceException.h"
 
@@ -128,7 +128,7 @@ public:
 		// all states that have probability 0 and 1 of satisfying the until-formula.
 		storm::storage::BitVector notExistsPhiUntilPsiStates(this->getModel().getNumberOfStates());
 		storm::storage::BitVector alwaysPhiUntilPsiStates(this->getModel().getNumberOfStates());
-		storm::solver::GraphAnalyzer::getPhiUntilPsiStates<double>(this->getModel(), *leftStates, *rightStates, &notExistsPhiUntilPsiStates, &alwaysPhiUntilPsiStates);
+		storm::utility::GraphAnalyzer::getPhiUntilPsiStates<double>(this->getModel(), *leftStates, *rightStates, &notExistsPhiUntilPsiStates, &alwaysPhiUntilPsiStates);
 		notExistsPhiUntilPsiStates.complement();
 
 		delete leftStates;
diff --git a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h
index 009ecd678..a1b11af0a 100644
--- a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h
+++ b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h
@@ -12,7 +12,7 @@
 
 #include "src/models/Dtmc.h"
 #include "src/modelchecker/DtmcPrctlModelChecker.h"
-#include "src/solver/GraphAnalyzer.h"
+#include "src/utility/GraphAnalyzer.h"
 #include "src/utility/Vector.h"
 #include "src/utility/ConstTemplates.h"
 #include "src/utility/Settings.h"
@@ -113,7 +113,7 @@ public:
 		// all states that have probability 0 and 1 of satisfying the until-formula.
 		storm::storage::BitVector notExistsPhiUntilPsiStates(this->getModel().getNumberOfStates());
 		storm::storage::BitVector alwaysPhiUntilPsiStates(this->getModel().getNumberOfStates());
-		storm::solver::GraphAnalyzer::getPhiUntilPsiStates(this->getModel(), *leftStates, *rightStates, &notExistsPhiUntilPsiStates, &alwaysPhiUntilPsiStates);
+		storm::utility::GraphAnalyzer::getPhiUntilPsiStates(this->getModel(), *leftStates, *rightStates, &notExistsPhiUntilPsiStates, &alwaysPhiUntilPsiStates);
 		notExistsPhiUntilPsiStates.complement();
 
 		// Delete sub-results that are obsolete now.
@@ -253,7 +253,7 @@ public:
 		// Determine which states have a reward of infinity by definition.
 		storm::storage::BitVector infinityStates(this->getModel().getNumberOfStates());
 		storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true);
-		storm::solver::GraphAnalyzer::getAlwaysPhiUntilPsiStates(this->getModel(), trueStates, *targetStates, &infinityStates);
+		storm::utility::GraphAnalyzer::getAlwaysPhiUntilPsiStates(this->getModel(), trueStates, *targetStates, &infinityStates);
 		infinityStates.complement();
 
 		// Create resulting vector.
diff --git a/src/models/Ctmc.h b/src/models/Ctmc.h
index 263a62fe9..ef6cd4658 100644
--- a/src/models/Ctmc.h
+++ b/src/models/Ctmc.h
@@ -139,7 +139,7 @@ public:
 	 */
 	storm::models::GraphTransitions<T>& getBackwardTransitions() {
 		if (this->backwardTransitions == nullptr) {
-			this->backwardTransitions = new storm::models::GraphTransitions<T>(this->probabilityMatrix, false);
+			this->backwardTransitions = new storm::models::GraphTransitions<T>(this->rateMatrix, false);
 		}
 		return *this->backwardTransitions;
 	}
diff --git a/src/storm.cpp b/src/storm.cpp
index 2015e85e4..f0b528f99 100644
--- a/src/storm.cpp
+++ b/src/storm.cpp
@@ -26,7 +26,6 @@
 #include "src/modelchecker/GmmxxDtmcPrctlModelChecker.h"
 #include "src/parser/AutoParser.h"
 #include "src/parser/PrctlParser.h"
-#include "src/solver/GraphAnalyzer.h"
 #include "src/utility/Settings.h"
 #include "src/formula/Formulas.h"
 
diff --git a/src/solver/GraphAnalyzer.h b/src/utility/GraphAnalyzer.h
similarity index 97%
rename from src/solver/GraphAnalyzer.h
rename to src/utility/GraphAnalyzer.h
index 70b6b10f5..0e3479338 100644
--- a/src/solver/GraphAnalyzer.h
+++ b/src/utility/GraphAnalyzer.h
@@ -5,8 +5,8 @@
  *      Author: Christian Dehnert
  */
 
-#ifndef STORM_SOLVER_GRAPHANALYZER_H_
-#define STORM_SOLVER_GRAPHANALYZER_H_
+#ifndef STORM_UTILITY_GRAPHANALYZER_H_
+#define STORM_UTILITY_GRAPHANALYZER_H_
 
 #include "src/models/Dtmc.h"
 #include "src/exceptions/InvalidArgumentException.h"
@@ -18,7 +18,7 @@ extern log4cplus::Logger logger;
 
 namespace storm {
 
-namespace solver {
+namespace utility {
 
 class GraphAnalyzer {
 public:
@@ -148,8 +148,8 @@ public:
 
 };
 
-} // namespace solver
+} // namespace utility
 
 } // namespace storm
 
-#endif /* STORM_SOLVER_GRAPHANALYZER_H_ */
+#endif /* STORM_UTILITY_GRAPHANALYZER_H_ */

From 7d95a45633fc8ec43388727484ac9ecc628cedd4 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Sun, 10 Feb 2013 23:52:27 +0100
Subject: [PATCH 3/8] Fixed bug in AbstractModelChecker: it does now correctly
 inherit from a lot more interface classes. NOTE: checking a formula on a
 model checker that does not support it failed silently. This should NOT be
 the case. Re-enabled DEBUG option for cmake. NOTE: why was this disabled
 anyway? Introduced another layer AbstractDeterministicModel and
 AbstractNonDeterministicModel in model hierarchy to allow for easily
 distinguishing these classes. Made necessary adaptions in (hopefully) all
 classes. Move the graph analyzer to utility folder.

---
 CMakeLists.txt                                |  14 +-
 src/formula/ReachabilityReward.h              |   1 -
 src/modelchecker/AbstractModelChecker.h       |  13 +-
 src/modelchecker/DtmcPrctlModelChecker.h      |   5 +-
 src/modelchecker/GmmxxDtmcPrctlModelChecker.h |  28 ++--
 src/models/AbstractDeterministicModel.h       |  61 +++++++
 src/models/AbstractModel.h                    | 140 +++++++++++++++-
 src/models/AbstractNonDeterministicModel.h    |  49 ++++++
 src/models/Ctmc.h                             | 127 ++------------
 src/models/Ctmdp.h                            | 152 ++---------------
 src/models/Dtmc.h                             | 156 ++----------------
 src/models/GraphTransitions.h                 |   6 +-
 src/models/Mdp.h                              | 152 ++---------------
 src/parser/AutoParser.cpp                     |  79 ---------
 src/parser/AutoParser.h                       |  76 ++++++++-
 src/storm.cpp                                 |   2 +-
 src/utility/GraphAnalyzer.h                   |  10 +-
 src/utility/IoUtility.cpp                     |   2 +-
 test/parser/ParseMdpTest.cpp                  |   2 +-
 19 files changed, 414 insertions(+), 661 deletions(-)
 create mode 100644 src/models/AbstractDeterministicModel.h
 create mode 100644 src/models/AbstractNonDeterministicModel.h
 delete mode 100644 src/parser/AutoParser.cpp

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 0ffe20f22..8cf280117 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -50,13 +50,13 @@ option(USE_POPCNT "Sets whether the popcnt instruction is going to be used." ON)
 option(USE_BOOST_STATIC_LIBRARIES "Sets whether the Boost libraries should be linked statically." ON)
 
 # If the DEBUG option was turned on, we will target a debug version and a release version otherwise
-#if (DEBUG)
-#    set (CMAKE_BUILD_TYPE "DEBUG")
-#    message(STATUS "Building DEBUG version.")
-#else()
-#    set (CMAKE_BUILD_TYPE "RELEASE")
-#    message(STATUS "Building RELEASE version.")
-#endif()
+if (DEBUG)
+    set (CMAKE_BUILD_TYPE "DEBUG")
+    message(STATUS "Building DEBUG version.")
+else()
+    set (CMAKE_BUILD_TYPE "RELEASE")
+    message(STATUS "Building RELEASE version.")
+endif()
 
 message(STATUS "CMAKE_BUILD_TYPE: ${CMAKE_BUILD_TYPE}")
 message(STATUS "CMAKE_BUILD_TYPE (ENV): $ENV{CMAKE_BUILD_TYPE}")
diff --git a/src/formula/ReachabilityReward.h b/src/formula/ReachabilityReward.h
index ad8171642..a725e202a 100644
--- a/src/formula/ReachabilityReward.h
+++ b/src/formula/ReachabilityReward.h
@@ -11,7 +11,6 @@
 #include "src/formula/AbstractPathFormula.h"
 #include "src/formula/AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
-#include "src/modelchecker/AbstractModelChecker.h"
 
 namespace storm {
 namespace formula {
diff --git a/src/modelchecker/AbstractModelChecker.h b/src/modelchecker/AbstractModelChecker.h
index 5e0920231..69bbeb9da 100644
--- a/src/modelchecker/AbstractModelChecker.h
+++ b/src/modelchecker/AbstractModelChecker.h
@@ -33,12 +33,19 @@ template<class Type>
 class AbstractModelChecker :
 	public virtual storm::formula::IApModelChecker<Type>,
 	public virtual storm::formula::IAndModelChecker<Type>,
+	public virtual storm::formula::IOrModelChecker<Type>,
+	public virtual storm::formula::INotModelChecker<Type>,
+	public virtual storm::formula::IUntilModelChecker<Type>,
 	public virtual storm::formula::IEventuallyModelChecker<Type>,
 	public virtual storm::formula::IGloballyModelChecker<Type>,
 	public virtual storm::formula::INextModelChecker<Type>,
-	public virtual storm::formula::INotModelChecker<Type>,
-	public virtual storm::formula::IOrModelChecker<Type>
-	{
+	public virtual storm::formula::IBoundedUntilModelChecker<Type>,
+	public virtual storm::formula::IBoundedEventuallyModelChecker<Type>,
+	public virtual storm::formula::INoBoundOperatorModelChecker<Type>,
+	public virtual storm::formula::IPathBoundOperatorModelChecker<Type>,
+	public virtual storm::formula::IReachabilityRewardModelChecker<Type>,
+	public virtual storm::formula::ICumulativeRewardModelChecker<Type>,
+	public virtual storm::formula::IInstantaneousRewardModelChecker<Type> {
 	
 public:
 	template <template <class T> class Target>
diff --git a/src/modelchecker/DtmcPrctlModelChecker.h b/src/modelchecker/DtmcPrctlModelChecker.h
index 90f1672e0..48b10d54b 100644
--- a/src/modelchecker/DtmcPrctlModelChecker.h
+++ b/src/modelchecker/DtmcPrctlModelChecker.h
@@ -39,10 +39,7 @@ namespace modelChecker {
  */
 template<class Type>
 class DtmcPrctlModelChecker : 
-	public virtual AbstractModelChecker<Type>, 
-	public virtual storm::formula::INoBoundOperatorModelChecker<Type>,
-	public virtual storm::formula::IReachabilityRewardModelChecker<Type>
-	{
+	public virtual AbstractModelChecker<Type> {
 public:
 	/*!
 	 * Constructor
diff --git a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h
index a1b11af0a..6d11358b9 100644
--- a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h
+++ b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h
@@ -49,7 +49,7 @@ public:
 		storm::storage::BitVector* rightStates = this->checkStateFormula(formula.getRight());
 
 		// Copy the matrix before we make any changes.
-		storm::storage::SparseMatrix<Type> tmpMatrix(*this->getModel().getTransitionProbabilityMatrix());
+		storm::storage::SparseMatrix<Type> tmpMatrix(*this->getModel().getTransitionMatrix());
 
 		// Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula.
 		tmpMatrix.makeRowsAbsorbing(~(*leftStates | *rightStates) | *rightStates);
@@ -84,7 +84,7 @@ public:
 		storm::storage::BitVector* nextStates = this->checkStateFormula(formula.getChild());
 
 		// Transform the transition probability matrix to the gmm++ format to use its arithmetic.
-		gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*this->getModel().getTransitionProbabilityMatrix());
+		gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*this->getModel().getTransitionMatrix());
 
 		// Create the vector with which to multiply and initialize it correctly.
 		std::vector<Type> x(this->getModel().getNumberOfStates());
@@ -132,7 +132,7 @@ public:
 		uint_fast64_t 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().getTransitionProbabilityMatrix()->getSubmatrix(maybeStates);
+			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();
@@ -149,7 +149,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(mayBeStatesSetBitCount);
-			this->getModel().getTransitionProbabilityMatrix()->getConstrainedRowCountVector(maybeStates, alwaysPhiUntilPsiStates, &b);
+			this->getModel().getTransitionMatrix()->getConstrainedRowCountVector(maybeStates, alwaysPhiUntilPsiStates, &b);
 
 			// Solve the corresponding system of linear equations.
 			this->solveLinearEquationSystem(*gmmxxMatrix, x, b);
@@ -176,10 +176,10 @@ public:
 		}
 
 		// Transform the transition probability matrix to the gmm++ format to use its arithmetic.
-		gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*this->getModel().getTransitionProbabilityMatrix());
+		gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*this->getModel().getTransitionMatrix());
 
 		// Initialize result to state rewards of the model.
-		std::vector<Type>* result = new std::vector<Type>(*this->getModel().getStateRewards());
+		std::vector<Type>* result = new std::vector<Type>(*this->getModel().getStateRewardVector());
 
 		// Now perform matrix-vector multiplication as long as we meet the bound of the formula.
 		std::vector<Type>* swap = nullptr;
@@ -205,17 +205,17 @@ public:
 		}
 
 		// Transform the transition probability matrix to the gmm++ format to use its arithmetic.
-		gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*this->getModel().getTransitionProbabilityMatrix());
+		gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*this->getModel().getTransitionMatrix());
 
 		// Compute the reward vector to add in each step based on the available reward models.
 		std::vector<Type>* totalRewardVector = nullptr;
 		if (this->getModel().hasTransitionRewards()) {
-			totalRewardVector = this->getModel().getTransitionProbabilityMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix());
+			totalRewardVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix());
 			if (this->getModel().hasStateRewards()) {
-				gmm::add(*this->getModel().getStateRewards(), *totalRewardVector);
+				gmm::add(*this->getModel().getStateRewardVector(), *totalRewardVector);
 			}
 		} else {
-			totalRewardVector = new std::vector<Type>(*this->getModel().getStateRewards());
+			totalRewardVector = new std::vector<Type>(*this->getModel().getStateRewardVector());
 		}
 
 		std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
@@ -264,7 +264,7 @@ public:
 		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().getTransitionProbabilityMatrix()->getSubmatrix(maybeStates);
+			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();
@@ -283,7 +283,7 @@ 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().getTransitionProbabilityMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix());
+				std::vector<Type>* pointwiseProductRowSumVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix());
 				storm::utility::selectVectorValues(b, maybeStates, *pointwiseProductRowSumVector);
 				delete pointwiseProductRowSumVector;
 
@@ -293,7 +293,7 @@ public:
 					// that we still consider (i.e. maybeStates), we need to extract these values
 					// first.
 					std::vector<Type>* subStateRewards = new std::vector<Type>(maybeStatesSetBitCount);
-					storm::utility::setVectorValues(subStateRewards, maybeStates, *this->getModel().getStateRewards());
+					storm::utility::setVectorValues(subStateRewards, maybeStates, *this->getModel().getStateRewardVector());
 					gmm::add(*subStateRewards, *b);
 					delete subStateRewards;
 				}
@@ -302,7 +302,7 @@ public:
 				// 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::setVectorValues(b, maybeStates, *this->getModel().getStateRewards());
+				storm::utility::setVectorValues(b, maybeStates, *this->getModel().getStateRewardVector());
 			}
 
 			// Solve the corresponding system of linear equations.
diff --git a/src/models/AbstractDeterministicModel.h b/src/models/AbstractDeterministicModel.h
new file mode 100644
index 000000000..b7dc1a380
--- /dev/null
+++ b/src/models/AbstractDeterministicModel.h
@@ -0,0 +1,61 @@
+#ifndef STORM_MODELS_ABSTRACTDETERMINISTICMODEL_H_
+#define STORM_MODELS_ABSTRACTDETERMINISTICMODEL_H_
+
+#include "AbstractModel.h"
+#include "GraphTransitions.h"
+
+#include <memory>
+
+namespace storm {
+
+namespace models {
+
+/*!
+ *	@brief	Base class for all deterministic model classes.
+ *
+ *	This is base class defines a common interface for all deterministic models.
+ */
+template<class T>
+class AbstractDeterministicModel: public AbstractModel<T> {
+
+	public:
+		AbstractDeterministicModel(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix,
+			std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling,
+			std::shared_ptr<std::vector<T>> stateRewardVector, std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix)
+			: AbstractModel<T>(transitionMatrix, stateLabeling, stateRewardVector, transitionRewardMatrix), backwardTransitions(nullptr) {
+		}
+
+		virtual ~AbstractDeterministicModel() {
+			// Intentionally left empty.
+		}
+
+		AbstractDeterministicModel(AbstractDeterministicModel const& other) : AbstractModel<T>(other), backwardTransitions(nullptr) {
+			if (other.backwardTransitions != nullptr) {
+				backwardTransitions = new storm::models::GraphTransitions<T>(*other.backwardTransitions);
+			}
+		}
+
+		/*!
+		 * Retrieves a reference to the backwards transition relation.
+		 * @return A reference to the backwards transition relation.
+		 */
+		storm::models::GraphTransitions<T>& getBackwardTransitions() {
+			if (this->backwardTransitions == nullptr) {
+				this->backwardTransitions = std::shared_ptr<storm::models::GraphTransitions<T>>(new storm::models::GraphTransitions<T>(this->getTransitionMatrix(), this->getNumberOfStates(), false));
+			}
+			return *this->backwardTransitions;
+		}
+
+	private:
+		/*!
+		 * A data structure that stores the predecessors for all states. This is
+		 * needed for backwards directed searches.
+		 */
+		std::shared_ptr<storm::models::GraphTransitions<T>> backwardTransitions;
+};
+
+} // namespace models
+
+} // namespace storm
+
+#endif /* STORM_MODELS_ABSTRACTDETERMINISTICMODEL_H_ */
diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h
index c35ecd3cc..42aa13eb8 100644
--- a/src/models/AbstractModel.h
+++ b/src/models/AbstractModel.h
@@ -1,7 +1,12 @@
 #ifndef STORM_MODELS_ABSTRACTMODEL_H_
 #define STORM_MODELS_ABSTRACTMODEL_H_
 
+#include "src/models/AtomicPropositionsLabeling.h"
+#include "src/storage/BitVector.h"
+#include "src/storage/SparseMatrix.h"
+
 #include <memory>
+#include <vector>
 
 namespace storm {
 namespace models {
@@ -24,9 +29,32 @@ std::ostream& operator<<(std::ostream& os, ModelType const type);
  *	This is base class defines a common interface for all models to identify
  *	their type and obtain the special model.
  */
-class AbstractModel: public std::enable_shared_from_this<AbstractModel> {
+template<class T>
+class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
 
 	public:
+		/*! Constructs an abstract model from the given transition matrix and
+		 * the given labeling of the states.
+		 * @param transitionMatrix The matrix representing the transitions in the model.
+		 * @param stateLabeling The labeling that assigns a set of atomic
+		 * propositions to each state.
+		 * @param stateRewardVector The reward values associated with the states.
+		 * @param transitionRewardMatrix The reward values associated with the transitions of the model.
+		 */
+		AbstractModel(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix,
+				std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling,
+				std::shared_ptr<std::vector<T>> stateRewardVector, std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix)
+				: transitionMatrix(transitionMatrix), stateLabeling(stateLabeling), stateRewardVector(stateRewardVector), transitionRewardMatrix(transitionRewardMatrix) {
+			// Intentionally left empty.
+		}
+
+		/*!
+		 * Destructors.
+		 */
+		virtual ~AbstractModel() {
+			// Intentionally left empty.
+		}
+
 		/*!
 		 *	@brief Casts the model to the model type that was actually
 		 *	created.
@@ -44,7 +72,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel> {
 		 */
 		template <typename Model>
 		std::shared_ptr<Model> as() {
-			return std::dynamic_pointer_cast<Model>(shared_from_this());
+			return std::dynamic_pointer_cast<Model>(this->shared_from_this());
 		}
 		
 		/*!
@@ -55,7 +83,113 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel> {
 		 *	@return	Type of the model.
 		 */
 		virtual ModelType getType() = 0;
-		
+
+		/*!
+		 * Returns the state space size of the model.
+		 * @return The size of the state space of the model.
+		 */
+		virtual uint_fast64_t getNumberOfStates() const {
+			return this->getTransitionMatrix()->getColumnCount();
+		}
+
+		/*!
+		 * Returns the number of (non-zero) transitions of the model.
+		 * @return The number of (non-zero) transitions of the model.
+		 */
+		virtual uint_fast64_t getNumberOfTransitions() const {
+			return this->getTransitionMatrix()->getNonZeroEntryCount();
+		}
+
+		/*!
+		 * Returns a bit vector in which exactly those bits are set to true that
+		 * correspond to a state labeled with the given atomic proposition.
+		 * @param ap The atomic proposition for which to get the bit vector.
+		 * @return A bit vector in which exactly those bits are set to true that
+		 * correspond to a state labeled with the given atomic proposition.
+		 */
+		storm::storage::BitVector* getLabeledStates(std::string ap) const {
+			return stateLabeling->getAtomicProposition(ap);
+		}
+
+		/*!
+		 * Retrieves whether the given atomic proposition is a valid atomic proposition in this model.
+		 * @param atomicProposition The atomic proposition to be checked for validity.
+		 * @return True if the given atomic proposition is valid in this model.
+		 */
+		bool hasAtomicProposition(std::string const& atomicProposition) const {
+			return stateLabeling->containsAtomicProposition(atomicProposition);
+		}
+
+		/*!
+		 * Returns a pointer to the matrix representing the transition probability
+		 * function.
+		 * @return A pointer to the matrix representing the transition probability
+		 * function.
+		 */
+		std::shared_ptr<storm::storage::SparseMatrix<T>> 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;
+		}
+
+		/*!
+		 * 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;
+		}
+
+		/*!
+		 * Returns the set of states with which the given state is labeled.
+		 * @return The set of states with which the given state is labeled.
+		 */
+		std::set<std::string> const getPropositionsForState(uint_fast64_t const &state) const {
+			return stateLabeling->getPropositionsForState(state);
+		}
+
+		/*!
+		 * 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;
+		}
+
+		/*!
+		 * Retrieves whether this model has a state reward model.
+		 * @return True if this model has a state reward model.
+		 */
+		bool hasStateRewards() const {
+			return stateRewardVector != nullptr;
+		}
+
+		/*!
+		 * Retrieves whether this model has a transition reward model.
+		 * @return True if this model has a transition reward model.
+		 */
+		bool hasTransitionRewards() const {
+			return transitionRewardMatrix != nullptr;
+		}
+
+	private:
+		/*! A matrix representing the likelihoods of moving between states. */
+		std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix;
+
+		/*! The labeling of the states of the model. */
+		std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling;
+
+		/*! The state-based rewards of the model. */
+		std::shared_ptr<std::vector<T>> stateRewardVector;
+
+		/*! The transition-based rewards of the model. */
+		std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix;
 };
 
 } // namespace models
diff --git a/src/models/AbstractNonDeterministicModel.h b/src/models/AbstractNonDeterministicModel.h
new file mode 100644
index 000000000..153ca059c
--- /dev/null
+++ b/src/models/AbstractNonDeterministicModel.h
@@ -0,0 +1,49 @@
+#ifndef STORM_MODELS_ABSTRACTNONDETERMINISTICMODEL_H_
+#define STORM_MODELS_ABSTRACTNONDETERMINISTICMODEL_H_
+
+#include "AbstractModel.h"
+#include "GraphTransitions.h"
+
+#include <memory>
+
+namespace storm {
+
+namespace models {
+
+/*!
+ *	@brief	Base class for all non-deterministic model classes.
+ *
+ *	This is base class defines a common interface for all non-deterministic models.
+ */
+template<class T>
+class AbstractNonDeterministicModel: public AbstractModel<T> {
+
+	public:
+	AbstractNonDeterministicModel(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix,
+			std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling,
+			std::shared_ptr<std::vector<uint_fast64_t>> choiceIndices,
+			std::shared_ptr<std::vector<T>> stateRewardVector,
+			std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix)
+			: AbstractModel<T>(transitionMatrix, stateLabeling, stateRewardVector, transitionRewardMatrix),
+			  choiceIndices(choiceIndices) {
+		}
+
+		virtual ~AbstractNonDeterministicModel() {
+			// Intentionally left empty.
+		}
+
+		AbstractNonDeterministicModel(AbstractNonDeterministicModel const& other) : AbstractModel<T>(other),
+				choiceIndices(other.choiceIndices) {
+
+		}
+
+	private:
+		/*! A vector of indices mapping states to the choices (rows) in the transition matrix. */
+		std::shared_ptr<std::vector<uint_fast64_t>> choiceIndices;
+};
+
+} // namespace models
+
+} // namespace storm
+
+#endif /* STORM_MODELS_ABSTRACTDETERMINISTICMODEL_H_ */
diff --git a/src/models/Ctmc.h b/src/models/Ctmc.h
index ef6cd4658..3c4a36a75 100644
--- a/src/models/Ctmc.h
+++ b/src/models/Ctmc.h
@@ -18,18 +18,18 @@
 #include "src/storage/SparseMatrix.h"
 #include "src/exceptions/InvalidArgumentException.h"
 
-#include "src/models/AbstractModel.h"
+#include "AbstractDeterministicModel.h"
 
 namespace storm {
 
 namespace models {
 
 /*!
- * This class represents a discrete-time Markov chain (DTMC) whose states are
+ * This class represents a continuous-time Markov chain (CTMC) whose states are
  * labeled with atomic propositions.
  */
 template <class T>
-class Ctmc : public storm::models::AbstractModel {
+class Ctmc : public storm::models::AbstractDeterministicModel<T> {
 
 public:
 	//! Constructor
@@ -43,11 +43,9 @@ public:
 	 */
 	Ctmc(std::shared_ptr<storm::storage::SparseMatrix<T>> rateMatrix,
 			std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling,
-			std::shared_ptr<std::vector<T>> stateRewards = nullptr,
+			std::shared_ptr<std::vector<T>> stateRewardVector = nullptr,
 			std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix = nullptr)
-			: rateMatrix(rateMatrix), stateLabeling(stateLabeling),
-			  stateRewards(stateRewards), transitionRewardMatrix(transitionRewardMatrix),
-			  backwardTransitions(nullptr) {
+			: AbstractDeterministicModel<T>(rateMatrix, stateLabeling, stateRewardVector, transitionRewardMatrix) {
 	}
 
 	//! Copy Constructor
@@ -55,93 +53,8 @@ public:
 	 * Copy Constructor. Performs a deep copy of the given CTMC.
 	 * @param ctmc A reference to the CTMC that is to be copied.
 	 */
-	Ctmc(const Ctmc<T> &ctmc) : rateMatrix(ctmc.rateMatrix),
-			stateLabeling(ctmc.stateLabeling), stateRewards(ctmc.stateRewards),
-			transitionRewardMatrix(ctmc.transitionRewardMatrix) {
-		if (ctmc.backwardTransitions != nullptr) {
-			this->backwardTransitions = new storm::models::GraphTransitions<T>(*ctmc.backwardTransitions);
-		}
-	}
-
-	//! Destructor
-	/*!
-	 * Destructor. Frees the matrix and labeling associated with this CTMC.
-	 */
-	~Ctmc() {
-		if (this->backwardTransitions != nullptr) {
-			delete this->backwardTransitions;
-		}
-	}
-	
-	/*!
-	 * Returns the state space size of the CTMC.
-	 * @return The size of the state space of the CTMC.
-	 */
-	uint_fast64_t getNumberOfStates() const {
-		return this->rateMatrix->getRowCount();
-	}
-
-	/*!
-	 * Returns the number of (non-zero) transitions of the CTMC.
-	 * @return The number of (non-zero) transitions of the CTMC.
-	 */
-	uint_fast64_t getNumberOfTransitions() const {
-		return this->rateMatrix->getNonZeroEntryCount();
-	}
-
-	/*!
-	 * Returns a bit vector in which exactly those bits are set to true that
-	 * correspond to a state labeled with the given atomic proposition.
-	 * @param ap The atomic proposition for which to get the bit vector.
-	 * @return A bit vector in which exactly those bits are set to true that
-	 * correspond to a state labeled with the given atomic proposition.
-	 */
-	storm::storage::BitVector* getLabeledStates(std::string ap) const {
-		return this->stateLabeling->getAtomicProposition(ap);
-	}
-
-	/*!
-	 * Returns a pointer to the matrix representing the transition probability
-	 * function.
-	 * @return A pointer to the matrix representing the transition probability
-	 * function.
-	 */
-	std::shared_ptr<storm::storage::SparseMatrix<T>> getTransitionRateMatrix() const {
-		return this->rateMatrix;
-	}
-
-	/*!
-	 * 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 this->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>> getStateRewards() const {
-		return this->stateRewards;
-	}
-
-	/*!
-	 *
-	 */
-	std::set<std::string> const getPropositionsForState(uint_fast64_t const &state) const {
-		return stateLabeling->getPropositionsForState(state);
-	}
-
-	/*!
-	 * Retrieves a reference to the backwards transition relation.
-	 * @return A reference to the backwards transition relation.
-	 */
-	storm::models::GraphTransitions<T>& getBackwardTransitions() {
-		if (this->backwardTransitions == nullptr) {
-			this->backwardTransitions = new storm::models::GraphTransitions<T>(this->rateMatrix, false);
-		}
-		return *this->backwardTransitions;
+	Ctmc(const Ctmc<T> &ctmc) : AbstractDeterministicModel<T>(ctmc) {
+		// Intentionally left empty.
 	}
 
 	/*!
@@ -154,10 +67,10 @@ public:
 		out << "Model type: \t\tCTMC" << std::endl;
 		out << "States: \t\t" << this->getNumberOfStates() << std::endl;
 		out << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl;
-		this->stateLabeling->printAtomicPropositionsInformationToStream(out);
+		this->getStateLabeling()->printAtomicPropositionsInformationToStream(out);
 		out << "Size in memory: \t"
-			<< (this->rateMatrix->getSizeInMemory() +
-				this->stateLabeling->getSizeInMemory() +
+			<< (this->getTransitionMatrix()->getSizeInMemory() +
+				this->stateLabeling()->getSizeInMemory() +
 				sizeof(*this))/1024 << " kbytes" << std::endl;
 		out << "-------------------------------------------------------------- "
 			<< std::endl;
@@ -166,26 +79,6 @@ public:
 	storm::models::ModelType getType() {
 		return CTMC;
 	}
-
-private:
-
-	/*! A matrix representing the transition rate function of the CTMC. */
-	std::shared_ptr<storm::storage::SparseMatrix<T>> rateMatrix;
-
-	/*! The labeling of the states of the CTMC. */
-	std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling;
-
-	/*! The state-based rewards of the CTMC. */
-	std::shared_ptr<std::vector<T>> stateRewards;
-
-	/*! The transition-based rewards of the CTMC. */
-	std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix;
-
-	/*!
-	 * A data structure that stores the predecessors for all states. This is
-	 * needed for backwards directed searches.
-	 */
-	storm::models::GraphTransitions<T>* backwardTransitions;
 };
 
 } // namespace models
diff --git a/src/models/Ctmdp.h b/src/models/Ctmdp.h
index 137095e9f..37b73d748 100644
--- a/src/models/Ctmdp.h
+++ b/src/models/Ctmdp.h
@@ -19,7 +19,7 @@
 #include "src/exceptions/InvalidArgumentException.h"
 #include "src/utility/CommandLine.h"
 #include "src/utility/Settings.h"
-#include "src/models/AbstractModel.h"
+#include "src/models/AbstractNonDeterministicModel.h"
 #include "src/parser/NonDeterministicSparseTransitionParser.h"
 
 namespace storm {
@@ -31,7 +31,7 @@ namespace models {
  * labeled with atomic propositions.
  */
 template <class T>
-class Ctmdp : public storm::models::AbstractModel {
+class Ctmdp : public storm::models::AbstractNonDeterministicModel<T> {
 
 public:
 	//! Constructor
@@ -45,12 +45,10 @@ public:
 	 */
 	Ctmdp(std::shared_ptr<storm::storage::SparseMatrix<T>> probabilityMatrix,
 			std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling,
-			std::shared_ptr<std::vector<uint_fast64_t>> rowMapping,
-			std::shared_ptr<std::vector<T>> stateRewards = nullptr,
+			std::shared_ptr<std::vector<uint_fast64_t>> choiceIndices,
+			std::shared_ptr<std::vector<T>> stateRewardVector = nullptr,
 			std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix = nullptr)
-			: probabilityMatrix(probabilityMatrix), stateLabeling(stateLabeling), rowMapping(rowMapping),
-			  stateRewards(stateRewards), transitionRewardMatrix(transitionRewardMatrix),
-			  backwardTransitions(nullptr) {
+			: AbstractNonDeterministicModel<T>(probabilityMatrix, stateLabeling, choiceIndices, stateRewardVector, transitionRewardMatrix) {
 		if (!this->checkValidityOfProbabilityMatrix()) {
 			LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
 			throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
@@ -62,12 +60,7 @@ public:
 	 * Copy Constructor. Performs a deep copy of the given CTMDP.
 	 * @param ctmdp A reference to the CTMDP that is to be copied.
 	 */
-	Ctmdp(const Ctmdp<T> &ctmdp) : probabilityMatrix(ctmdp.probabilityMatrix),
-			stateLabeling(ctmdp.stateLabeling), rowMapping(ctmdp.rowMapping), stateRewards(ctmdp.stateRewards),
-			transitionRewardMatrix(ctmdp.transitionRewardMatrix) {
-		if (ctmdp.backwardTransitions != nullptr) {
-			this->backwardTransitions = new storm::models::GraphTransitions<T>(*ctmdp.backwardTransitions);
-		}
+	Ctmdp(const Ctmdp<T> &ctmdp) : AbstractNonDeterministicModel<T>(ctmdp) {
 		if (!this->checkValidityOfProbabilityMatrix()) {
 			LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
 			throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
@@ -76,110 +69,12 @@ public:
 
 	//! Destructor
 	/*!
-	 * Destructor. Frees the matrix and labeling associated with this CTMDP.
+	 * Destructor.
 	 */
 	~Ctmdp() {
-		if (this->backwardTransitions != nullptr) {
-			delete this->backwardTransitions;
-		}
+		// Intentionally left empty.
 	}
 	
-	/*!
-	 * Returns the state space size of the CTMDP.
-	 * @return The size of the state space of the CTMDP.
-	 */
-	uint_fast64_t getNumberOfStates() const {
-		return this->probabilityMatrix->getColumnCount();
-	}
-
-	/*!
-	 * Returns the number of (non-zero) transitions of the CTMDP.
-	 * @return The number of (non-zero) transitions of the CTMDP.
-	 */
-	uint_fast64_t getNumberOfTransitions() const {
-		return this->probabilityMatrix->getNonZeroEntryCount();
-	}
-
-	/*!
-	 * Returns a bit vector in which exactly those bits are set to true that
-	 * correspond to a state labeled with the given atomic proposition.
-	 * @param ap The atomic proposition for which to get the bit vector.
-	 * @return A bit vector in which exactly those bits are set to true that
-	 * correspond to a state labeled with the given atomic proposition.
-	 */
-	storm::storage::BitVector* getLabeledStates(std::string ap) const {
-		return this->stateLabeling->getAtomicProposition(ap);
-	}
-
-	/*!
-	 * Returns a pointer to the matrix representing the transition probability
-	 * function.
-	 * @return A pointer to the matrix representing the transition probability
-	 * function.
-	 */
-	std::shared_ptr<storm::storage::SparseMatrix<T>> getTransitionProbabilityMatrix() const {
-		return this->probabilityMatrix;
-	}
-
-	/*!
-	 * 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 this->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>> getStateRewards() const {
-		return this->stateRewards;
-	}
-
-	/*!
-	 *
-	 */
-	std::set<std::string> const getPropositionsForState(uint_fast64_t const &state) const {
-		return stateLabeling->getPropositionsForState(state);
-	}
-
-	/*!
-	 * Retrieves a reference to the backwards transition relation.
-	 * @return A reference to the backwards transition relation.
-	 */
-	storm::models::GraphTransitions<T>& getBackwardTransitions() {
-		if (this->backwardTransitions == nullptr) {
-			this->backwardTransitions = new storm::models::GraphTransitions<T>(this->probabilityMatrix, false);
-		}
-		return *this->backwardTransitions;
-	}
-
-	/*!
-	 * Retrieves whether this CTMDP has a state reward model.
-	 * @return True if this CTMDP has a state reward model.
-	 */
-	bool hasStateRewards() {
-		return this->stateRewards != nullptr;
-	}
-
-	/*!
-	 * Retrieves whether this CTMDP has a transition reward model.
-	 * @return True if this CTMDP has a transition reward model.
-	 */
-	bool hasTransitionRewards() {
-		return this->transitionRewardMatrix != nullptr;
-	}
-
-	/*!
-	 * Retrieves whether the given atomic proposition is a valid atomic proposition in this model.
-	 * @param atomicProposition The atomic proposition to be checked for validity.
-	 * @return True if the given atomic proposition is valid in this model.
-	 */
-	bool hasAtomicProposition(std::string const& atomicProposition) {
-		return this->stateLabeling->containsAtomicProposition(atomicProposition);
-	}
-
 	/*!
 	 * Prints information about the model to the specified stream.
 	 * @param out The stream the information is to be printed to.
@@ -190,10 +85,10 @@ public:
 		out << "Model type: \t\tCTMDP" << std::endl;
 		out << "States: \t\t" << this->getNumberOfStates() << std::endl;
 		out << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl;
-		this->stateLabeling->printAtomicPropositionsInformationToStream(out);
+		this->getStateLabeling()->printAtomicPropositionsInformationToStream(out);
 		out << "Size in memory: \t"
-			<< (this->probabilityMatrix->getSizeInMemory() +
-				this->stateLabeling->getSizeInMemory() +
+			<< (this->getTransitionMatrix()->getSizeInMemory() +
+				this->getStateLabeling()->getSizeInMemory() +
 				sizeof(*this))/1024 << " kbytes" << std::endl;
 		out << std::endl;
 		storm::utility::printSeparationLine(out);
@@ -214,34 +109,13 @@ 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->probabilityMatrix->getRowCount(); row++) {
-			T sum = this->probabilityMatrix->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;
 		}
 		return true;
 	}
-
-	/*! A matrix representing the transition probability function of the CTMDP. */
-	std::shared_ptr<storm::storage::SparseMatrix<T>> probabilityMatrix;
-
-	/*! The labeling of the states of the CTMDP. */
-	std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling;
-	
-	/*! The mapping from states to rows. */
-	std::shared_ptr<std::vector<uint_fast64_t>> rowMapping;
-
-	/*! The state-based rewards of the CTMDP. */
-	std::shared_ptr<std::vector<T>> stateRewards;
-
-	/*! The transition-based rewards of the CTMDP. */
-	std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix;
-
-	/*!
-	 * A data structure that stores the predecessors for all states. This is
-	 * needed for backwards directed searches.
-	 */
-	storm::models::GraphTransitions<T>* backwardTransitions;
 };
 
 } // namespace models
diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h
index c19208543..42e6279d3 100644
--- a/src/models/Dtmc.h
+++ b/src/models/Dtmc.h
@@ -19,7 +19,7 @@
 #include "src/exceptions/InvalidArgumentException.h"
 #include "src/utility/CommandLine.h"
 #include "src/utility/Settings.h"
-#include "src/models/AbstractModel.h"
+#include "src/models/AbstractDeterministicModel.h"
 
 namespace storm {
 
@@ -30,7 +30,7 @@ namespace models {
  * labeled with atomic propositions.
  */
 template <class T>
-class Dtmc : public storm::models::AbstractModel {
+class Dtmc : public storm::models::AbstractDeterministicModel<T> {
 
 public:
 	//! Constructor
@@ -44,17 +44,15 @@ public:
 	 */
 	Dtmc(std::shared_ptr<storm::storage::SparseMatrix<T>> probabilityMatrix,
 			std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling,
-			std::shared_ptr<std::vector<T>> stateRewards = nullptr,
+			std::shared_ptr<std::vector<T>> stateRewardVector = nullptr,
 			std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix = nullptr)
-			: probabilityMatrix(probabilityMatrix), stateLabeling(stateLabeling),
-			  stateRewards(stateRewards), transitionRewardMatrix(transitionRewardMatrix),
-			  backwardTransitions(nullptr) {
+			: AbstractDeterministicModel<T>(probabilityMatrix, stateLabeling, stateRewardVector, transitionRewardMatrix) {
 		if (!this->checkValidityOfProbabilityMatrix()) {
 			LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
 			throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
 		}
-		if (this->transitionRewardMatrix != nullptr) {
-			if (!this->transitionRewardMatrix->isSubmatrixOf(*(this->probabilityMatrix))) {
+		if (this->getTransitionRewardMatrix() != nullptr) {
+			if (!this->getTransitionRewardMatrix()->isSubmatrixOf(*(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.";
 			}
@@ -66,119 +64,16 @@ public:
 	 * Copy Constructor. Performs a deep copy of the given DTMC.
 	 * @param dtmc A reference to the DTMC that is to be copied.
 	 */
-	Dtmc(const Dtmc<T> &dtmc) : probabilityMatrix(dtmc.probabilityMatrix),
-			stateLabeling(dtmc.stateLabeling), stateRewards(dtmc.stateRewards),
-			transitionRewardMatrix(dtmc.transitionRewardMatrix) {
-		if (dtmc.backwardTransitions != nullptr) {
-			this->backwardTransitions = new storm::models::GraphTransitions<T>(*dtmc.backwardTransitions);
-		}
-		// no checks here, as they have already been performed for dtmc.
+	Dtmc(const Dtmc<T> &dtmc) : AbstractDeterministicModel<T>(dtmc) {
+		// Intentionally left empty.
 	}
 
 	//! Destructor
 	/*!
-	 * Destructor. Frees the matrix and labeling associated with this DTMC.
+	 * Destructor.
 	 */
 	~Dtmc() {
-		if (this->backwardTransitions != nullptr) {
-			delete this->backwardTransitions;
-		}
-	}
-	
-	/*!
-	 * Returns the state space size of the DTMC.
-	 * @return The size of the state space of the DTMC.
-	 */
-	uint_fast64_t getNumberOfStates() const {
-		return this->probabilityMatrix->getRowCount();
-	}
-
-	/*!
-	 * Returns the number of (non-zero) transitions of the DTMC.
-	 * @return The number of (non-zero) transitions of the DTMC.
-	 */
-	uint_fast64_t getNumberOfTransitions() const {
-		return this->probabilityMatrix->getNonZeroEntryCount();
-	}
-
-	/*!
-	 * Returns a bit vector in which exactly those bits are set to true that
-	 * correspond to a state labeled with the given atomic proposition.
-	 * @param ap The atomic proposition for which to get the bit vector.
-	 * @return A bit vector in which exactly those bits are set to true that
-	 * correspond to a state labeled with the given atomic proposition.
-	 */
-	storm::storage::BitVector* getLabeledStates(std::string ap) const {
-		return this->stateLabeling->getAtomicProposition(ap);
-	}
-
-	/*!
-	 * Returns a pointer to the matrix representing the transition probability
-	 * function.
-	 * @return A pointer to the matrix representing the transition probability
-	 * function.
-	 */
-	std::shared_ptr<storm::storage::SparseMatrix<T>> getTransitionProbabilityMatrix() const {
-		return this->probabilityMatrix;
-	}
-
-	/*!
-	 * 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 this->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>> getStateRewards() const {
-		return this->stateRewards;
-	}
-
-	/*!
-	 *
-	 */
-	std::set<std::string> const getPropositionsForState(uint_fast64_t const &state) const {
-		return stateLabeling->getPropositionsForState(state);
-	}
-
-	/*!
-	 * Retrieves a reference to the backwards transition relation.
-	 * @return A reference to the backwards transition relation.
-	 */
-	storm::models::GraphTransitions<T>& getBackwardTransitions() {
-		if (this->backwardTransitions == nullptr) {
-			this->backwardTransitions = new storm::models::GraphTransitions<T>(this->probabilityMatrix, false);
-		}
-		return *this->backwardTransitions;
-	}
-
-	/*!
-	 * Retrieves whether this DTMC has a state reward model.
-	 * @return True if this DTMC has a state reward model.
-	 */
-	bool hasStateRewards() {
-		return this->stateRewards != nullptr;
-	}
-
-	/*!
-	 * Retrieves whether this DTMC has a transition reward model.
-	 * @return True if this DTMC has a transition reward model.
-	 */
-	bool hasTransitionRewards() {
-		return this->transitionRewardMatrix != nullptr;
-	}
-
-	/*!
-	 * Retrieves whether the given atomic proposition is a valid atomic proposition in this model.
-	 * @param atomicProposition The atomic proposition to be checked for validity.
-	 * @return True if the given atomic proposition is valid in this model.
-	 */
-	bool hasAtomicProposition(std::string const& atomicProposition) {
-		return this->stateLabeling->containsAtomicProposition(atomicProposition);
+		// Intentionally left empty.
 	}
 
 	/*!
@@ -191,10 +86,10 @@ public:
 		out << "Model type: \t\tDTMC" << std::endl;
 		out << "States: \t\t" << this->getNumberOfStates() << std::endl;
 		out << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl;
-		this->stateLabeling->printAtomicPropositionsInformationToStream(out);
+		this->getStateLabeling()->printAtomicPropositionsInformationToStream(out);
 		out << "Size in memory: \t"
-			<< (this->probabilityMatrix->getSizeInMemory() +
-				this->stateLabeling->getSizeInMemory() +
+			<< (this->getTransitionMatrix()->getSizeInMemory() +
+				this->getStateLabeling()->getSizeInMemory() +
 				sizeof(*this))/1024 << " kbytes" << std::endl;
 		out << std::endl;
 		storm::utility::printSeparationLine(out);
@@ -205,7 +100,6 @@ public:
 	}
 
 private:
-
 	/*!
 	 *	@brief Perform some sanity checks.
 	 *
@@ -216,14 +110,14 @@ private:
 		storm::settings::Settings* s = storm::settings::instance();
 		double precision = s->get<double>("precision");
 
-		if (this->probabilityMatrix->getRowCount() != this->probabilityMatrix->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->probabilityMatrix->getRowCount(); row++) {
-			T sum = this->probabilityMatrix->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;
@@ -235,24 +129,6 @@ private:
 		}
 		return true;
 	}
-
-	/*! A matrix representing the transition probability function of the DTMC. */
-	std::shared_ptr<storm::storage::SparseMatrix<T>> probabilityMatrix;
-
-	/*! The labeling of the states of the DTMC. */
-	std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling;
-
-	/*! The state-based rewards of the DTMC. */
-	std::shared_ptr<std::vector<T>> stateRewards;
-
-	/*! The transition-based rewards of the DTMC. */
-	std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix;
-
-	/*!
-	 * A data structure that stores the predecessors for all states. This is
-	 * needed for backwards directed searches.
-	 */
-	storm::models::GraphTransitions<T>* backwardTransitions;
 };
 
 } // namespace models
diff --git a/src/models/GraphTransitions.h b/src/models/GraphTransitions.h
index 579bf7832..1cf152666 100644
--- a/src/models/GraphTransitions.h
+++ b/src/models/GraphTransitions.h
@@ -39,8 +39,8 @@ public:
 	 * @param forward If set to true, this objects will store the graph structure
 	 * of the backwards transition relation.
 	 */
-	GraphTransitions(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix, bool forward)
-			: successorList(nullptr), stateIndications(nullptr), numberOfStates(transitionMatrix->getRowCount()), numberOfNonZeroTransitions(transitionMatrix->getNonZeroEntryCount()) {
+	GraphTransitions(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix, uint_fast64_t numberOfStates, bool forward)
+			: successorList(nullptr), stateIndications(nullptr), numberOfStates(numberOfStates), numberOfNonZeroTransitions(transitionMatrix->getNonZeroEntryCount()) {
 		if (forward) {
 			this->initializeForward(transitionMatrix);
 		} else {
@@ -111,7 +111,7 @@ private:
 	 */
 	void initializeBackward(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix) {
 		this->successorList = new uint_fast64_t[numberOfNonZeroTransitions];
-		this->stateIndications = new uint_fast64_t[numberOfStates + 1];
+		this->stateIndications = new uint_fast64_t[numberOfStates + 1]();
 
 		// First, we need to count how many backward transitions each state has.
 		// NOTE: We disregard the diagonal here, as we only consider "true"
diff --git a/src/models/Mdp.h b/src/models/Mdp.h
index 5b9d0157f..357fa1433 100644
--- a/src/models/Mdp.h
+++ b/src/models/Mdp.h
@@ -19,7 +19,7 @@
 #include "src/exceptions/InvalidArgumentException.h"
 #include "src/utility/CommandLine.h"
 #include "src/utility/Settings.h"
-#include "src/models/AbstractModel.h"
+#include "src/models/AbstractNonDeterministicModel.h"
 #include "src/parser/NonDeterministicSparseTransitionParser.h"
 
 namespace storm {
@@ -31,7 +31,7 @@ namespace models {
  * labeled with atomic propositions.
  */
 template <class T>
-class Mdp : public storm::models::AbstractModel {
+class Mdp : public storm::models::AbstractNonDeterministicModel<T> {
 
 public:
 	//! Constructor
@@ -45,12 +45,10 @@ public:
 	 */
 	Mdp(std::shared_ptr<storm::storage::SparseMatrix<T>> probabilityMatrix,
 			std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling,
-			std::shared_ptr<std::vector<uint_fast64_t>> rowMapping,
-			std::shared_ptr<std::vector<T>> stateRewards = nullptr,
+			std::shared_ptr<std::vector<uint_fast64_t>> choiceIndices,
+			std::shared_ptr<std::vector<T>> stateRewardVector = nullptr,
 			std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix = nullptr)
-			: probabilityMatrix(probabilityMatrix), stateLabeling(stateLabeling), rowMapping(rowMapping),
-			  stateRewards(stateRewards), transitionRewardMatrix(transitionRewardMatrix),
-			  backwardTransitions(nullptr) {
+			: AbstractNonDeterministicModel<T>(probabilityMatrix, stateLabeling, choiceIndices, stateRewardVector, transitionRewardMatrix) {
 		if (!this->checkValidityOfProbabilityMatrix()) {
 			LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
 			throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
@@ -62,12 +60,7 @@ public:
 	 * Copy Constructor. Performs a deep copy of the given MDP.
 	 * @param mdp A reference to the MDP that is to be copied.
 	 */
-	Mdp(const Mdp<T> &mdp) : probabilityMatrix(mdp.probabilityMatrix),
-			stateLabeling(mdp.stateLabeling), rowMapping(mdp.rowMapping), stateRewards(mdp.stateRewards),
-			transitionRewardMatrix(mdp.transitionRewardMatrix) {
-		if (mdp.backwardTransitions != nullptr) {
-			this->backwardTransitions = new storm::models::GraphTransitions<T>(*mdp.backwardTransitions);
-		}
+	Mdp(const Mdp<T> &mdp) : AbstractNonDeterministicModel<T>(mdp) {
 		if (!this->checkValidityOfProbabilityMatrix()) {
 			LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
 			throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
@@ -76,108 +69,10 @@ public:
 
 	//! Destructor
 	/*!
-	 * Destructor. Frees the matrix and labeling associated with this MDP.
+	 * Destructor.
 	 */
 	~Mdp() {
-		if (this->backwardTransitions != nullptr) {
-			delete this->backwardTransitions;
-		}
-	}
-	
-	/*!
-	 * Returns the state space size of the MDP.
-	 * @return The size of the state space of the MDP.
-	 */
-	uint_fast64_t getNumberOfStates() const {
-		return this->probabilityMatrix->getColumnCount();
-	}
-
-	/*!
-	 * Returns the number of (non-zero) transitions of the MDP.
-	 * @return The number of (non-zero) transitions of the MDP.
-	 */
-	uint_fast64_t getNumberOfTransitions() const {
-		return this->probabilityMatrix->getNonZeroEntryCount();
-	}
-
-	/*!
-	 * Returns a bit vector in which exactly those bits are set to true that
-	 * correspond to a state labeled with the given atomic proposition.
-	 * @param ap The atomic proposition for which to get the bit vector.
-	 * @return A bit vector in which exactly those bits are set to true that
-	 * correspond to a state labeled with the given atomic proposition.
-	 */
-	storm::storage::BitVector* getLabeledStates(std::string ap) const {
-		return this->stateLabeling->getAtomicProposition(ap);
-	}
-
-	/*!
-	 * Returns a pointer to the matrix representing the transition probability
-	 * function.
-	 * @return A pointer to the matrix representing the transition probability
-	 * function.
-	 */
-	std::shared_ptr<storm::storage::SparseMatrix<T>> getTransitionProbabilityMatrix() const {
-		return this->probabilityMatrix;
-	}
-
-	/*!
-	 * 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 this->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>> getStateRewards() const {
-		return this->stateRewards;
-	}
-
-	/*!
-	 *
-	 */
-	std::set<std::string> const getPropositionsForState(uint_fast64_t const &state) const {
-		return stateLabeling->getPropositionsForState(state);
-	}
-
-	/*!
-	 * Retrieves a reference to the backwards transition relation.
-	 * @return A reference to the backwards transition relation.
-	 */
-	storm::models::GraphTransitions<T>& getBackwardTransitions() {
-		if (this->backwardTransitions == nullptr) {
-			this->backwardTransitions = new storm::models::GraphTransitions<T>(this->probabilityMatrix, false);
-		}
-		return *this->backwardTransitions;
-	}
-
-	/*!
-	 * Retrieves whether this MDP has a state reward model.
-	 * @return True if this MDP has a state reward model.
-	 */
-	bool hasStateRewards() {
-		return this->stateRewards != nullptr;
-	}
-
-	/*!
-	 * Retrieves whether this MDP has a transition reward model.
-	 * @return True if this MDP has a transition reward model.
-	 */
-	bool hasTransitionRewards() {
-		return this->transitionRewardMatrix != nullptr;
-	}
-
-	/*!
-	 * Retrieves whether the given atomic proposition is a valid atomic proposition in this model.
-	 * @param atomicProposition The atomic proposition to be checked for validity.
-	 * @return True if the given atomic proposition is valid in this model.
-	 */
-	bool hasAtomicProposition(std::string const& atomicProposition) {
-		return this->stateLabeling->containsAtomicProposition(atomicProposition);
+		// Intentionally left empty.
 	}
 
 	/*!
@@ -190,10 +85,10 @@ public:
 		out << "Model type: \t\tMDP" << std::endl;
 		out << "States: \t\t" << this->getNumberOfStates() << std::endl;
 		out << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl;
-		this->stateLabeling->printAtomicPropositionsInformationToStream(out);
+		this->getStateLabeling()->printAtomicPropositionsInformationToStream(out);
 		out << "Size in memory: \t"
-			<< (this->probabilityMatrix->getSizeInMemory() +
-				this->stateLabeling->getSizeInMemory() +
+			<< (this->getTransitionMatrix()->getSizeInMemory() +
+				this->getStateLabeling()->getSizeInMemory() +
 				sizeof(*this))/1024 << " kbytes" << std::endl;
 		out << std::endl;
 		storm::utility::printSeparationLine(out);
@@ -214,34 +109,13 @@ 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->probabilityMatrix->getRowCount(); row++) {
-			T sum = this->probabilityMatrix->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;
 		}
 		return true;
 	}
-
-	/*! A matrix representing the transition probability function of the MDP. */
-	std::shared_ptr<storm::storage::SparseMatrix<T>> probabilityMatrix;
-
-	/*! The labeling of the states of the MDP. */
-	std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling;
-	
-	/*! The mapping from states to rows. */
-	std::shared_ptr<std::vector<uint_fast64_t>> rowMapping;
-
-	/*! The state-based rewards of the MDP. */
-	std::shared_ptr<std::vector<T>> stateRewards;
-
-	/*! The transition-based rewards of the MDP. */
-	std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix;
-
-	/*!
-	 * A data structure that stores the predecessors for all states. This is
-	 * needed for backwards directed searches.
-	 */
-	storm::models::GraphTransitions<T>* backwardTransitions;
 };
 
 } // namespace models
diff --git a/src/parser/AutoParser.cpp b/src/parser/AutoParser.cpp
deleted file mode 100644
index 6c0d5cc40..000000000
--- a/src/parser/AutoParser.cpp
+++ /dev/null
@@ -1,79 +0,0 @@
-#include "src/parser/AutoParser.h"
-
-#include <string>
-#include <cctype>
-
-#include "src/exceptions/WrongFileFormatException.h"
-#include "src/models/AbstractModel.h"
-#include "src/parser/DeterministicModelParser.h"
-#include "src/parser/NonDeterministicModelParser.h"
-
-namespace storm {
-namespace parser {
-
-AutoParser::AutoParser(std::string const & transitionSystemFile, std::string const & labelingFile,
-	std::string const & stateRewardFile, std::string const & transitionRewardFile)
-	: model(nullptr) {
-	storm::models::ModelType type = this->analyzeHint(transitionSystemFile);
-
-	if (type == storm::models::Unknown) {
-		LOG4CPLUS_ERROR(logger, "Could not determine file type of " << transitionSystemFile << ".");
-		LOG4CPLUS_ERROR(logger, "The first line of the file should contain a format hint. Please fix your file and try again.");
-		throw storm::exceptions::WrongFileFormatException() << "Could not determine type of file " << transitionSystemFile;
-	} else {
-		LOG4CPLUS_INFO(logger, "Model type seems to be " << type);
-	}
-
-	// Do actual parsing
-	switch (type) {
-		case storm::models::DTMC: {
-			DeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
-			this->model = parser.getDtmc();
-			break;
-		}
-		case storm::models::CTMC: {
-			DeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
-			this->model = parser.getCtmc();
-			break;
-		}
-		case storm::models::MDP: {
-			NonDeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
-			this->model = parser.getMdp();
-			break;
-		}
-		case storm::models::CTMDP: {
-			NonDeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
-			this->model = parser.getCtmdp();
-			break;
-		}
-		default: ;  // Unknown
-	}
-
-	
-	if (!this->model) {
-		LOG4CPLUS_WARN(logger, "Model is still null.");
-	}
-}
-
-storm::models::ModelType AutoParser::analyzeHint(const std::string& filename) {
-	storm::models::ModelType hintType = storm::models::Unknown;
-	// Open file
-	MappedFile file(filename.c_str());
-	char* buf = file.data;
-
-	// parse hint
-	char hint[128];
-	sscanf(buf, "%s\n", hint);
-	for (char* c = hint; *c != '\0'; c++) *c = toupper(*c);
-
-	// check hint
-	if (strncmp(hint, "DTMC", sizeof(hint)) == 0) hintType = storm::models::DTMC;
-	else if (strncmp(hint, "CTMC", sizeof(hint)) == 0) hintType = storm::models::CTMC;
-	else if (strncmp(hint, "MDP", sizeof(hint)) == 0) hintType = storm::models::MDP;
-	else if (strncmp(hint, "CTMDP", sizeof(hint)) == 0) hintType = storm::models::CTMDP;
-
-	return hintType;
-}
-
-}  // namespace parser
-}  // namespace storm
diff --git a/src/parser/AutoParser.h b/src/parser/AutoParser.h
index 1424cb9b7..d7337ae54 100644
--- a/src/parser/AutoParser.h
+++ b/src/parser/AutoParser.h
@@ -4,11 +4,19 @@
 #include "src/parser/Parser.h"
 #include "src/models/AbstractModel.h"
 
+#include "src/exceptions/WrongFileFormatException.h"
+#include "src/models/AbstractModel.h"
+#include "src/parser/DeterministicModelParser.h"
+#include "src/parser/NonDeterministicModelParser.h"
+
 #include <memory>
 #include <iostream>
 #include <utility>
+#include <string>
+#include <cctype>
 
 namespace storm {
+
 namespace parser {
 
 /*!
@@ -21,10 +29,51 @@ namespace parser {
  *	When the files are parsed successfully, the parsed ModelType and Model
  *	can be obtained via getType() and getModel<ModelClass>().
  */
+template<class T>
 class AutoParser : Parser {
 	public:
 		AutoParser(std::string const & transitionSystemFile, std::string const & labelingFile,
-				std::string const & stateRewardFile = "", std::string const & transitionRewardFile = "");
+				std::string const & stateRewardFile = "", std::string const & transitionRewardFile = "") : model(nullptr) {
+			storm::models::ModelType type = this->analyzeHint(transitionSystemFile);
+
+			if (type == storm::models::Unknown) {
+				LOG4CPLUS_ERROR(logger, "Could not determine file type of " << transitionSystemFile << ".");
+				LOG4CPLUS_ERROR(logger, "The first line of the file should contain a format hint. Please fix your file and try again.");
+				throw storm::exceptions::WrongFileFormatException() << "Could not determine type of file " << transitionSystemFile;
+			} else {
+				LOG4CPLUS_INFO(logger, "Model type seems to be " << type);
+			}
+
+			// Do actual parsing
+			switch (type) {
+				case storm::models::DTMC: {
+					DeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
+					this->model = parser.getDtmc();
+					break;
+				}
+				case storm::models::CTMC: {
+					DeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
+					this->model = parser.getCtmc();
+					break;
+				}
+				case storm::models::MDP: {
+					NonDeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
+					this->model = parser.getMdp();
+					break;
+				}
+				case storm::models::CTMDP: {
+					NonDeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
+					this->model = parser.getCtmdp();
+					break;
+				}
+				default: ;  // Unknown
+			}
+
+
+			if (!this->model) {
+				LOG4CPLUS_WARN(logger, "Model is still null.");
+			}
+		}
 		
 		/*!
 		 *	@brief 	Returns the type of model that was parsed.
@@ -39,7 +88,7 @@ class AutoParser : Parser {
 		 */
 		template <typename Model>
 		std::shared_ptr<Model> getModel() {
-			return this->model->as<Model>();
+			return this->model->template as<Model>();
 		}
 		
 	private:
@@ -47,15 +96,34 @@ class AutoParser : Parser {
 		/*!
 		 *	@brief	Open file and read file format hint.
 		 */
-		storm::models::ModelType analyzeHint(const std::string& filename);
+		storm::models::ModelType analyzeHint(const std::string& filename) {
+			storm::models::ModelType hintType = storm::models::Unknown;
+			// Open file
+			MappedFile file(filename.c_str());
+			char* buf = file.data;
+
+			// parse hint
+			char hint[128];
+			sscanf(buf, "%s\n", hint);
+			for (char* c = hint; *c != '\0'; c++) *c = toupper(*c);
+
+			// check hint
+			if (strncmp(hint, "DTMC", sizeof(hint)) == 0) hintType = storm::models::DTMC;
+			else if (strncmp(hint, "CTMC", sizeof(hint)) == 0) hintType = storm::models::CTMC;
+			else if (strncmp(hint, "MDP", sizeof(hint)) == 0) hintType = storm::models::MDP;
+			else if (strncmp(hint, "CTMDP", sizeof(hint)) == 0) hintType = storm::models::CTMDP;
+
+			return hintType;
+		}
 		
 		/*!
 		 *	@brief	Pointer to a parser that has parsed the given transition system.
 		 */
-		std::shared_ptr<storm::models::AbstractModel> model;
+		std::shared_ptr<storm::models::AbstractModel<T>> model;
 };
 
 } // namespace parser
+
 } // namespace storm
 
 #endif /* STORM_PARSER_AUTOPARSER_H_ */
diff --git a/src/storm.cpp b/src/storm.cpp
index f0b528f99..26fe8d15a 100644
--- a/src/storm.cpp
+++ b/src/storm.cpp
@@ -210,7 +210,7 @@ void testCheckingSynchronousLeader(storm::models::Dtmc<double>& dtmc, uint_fast6
  */
 void testChecking() {
 	storm::settings::Settings* s = storm::settings::instance();
-	storm::parser::AutoParser parser(s->getString("trafile"), s->getString("labfile"), s->getString("staterew"), s->getString("transrew"));
+	storm::parser::AutoParser<double> parser(s->getString("trafile"), s->getString("labfile"), s->getString("staterew"), s->getString("transrew"));
 
 	if (parser.getType() == storm::models::DTMC) {
 		std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
diff --git a/src/utility/GraphAnalyzer.h b/src/utility/GraphAnalyzer.h
index 0e3479338..02c122d89 100644
--- a/src/utility/GraphAnalyzer.h
+++ b/src/utility/GraphAnalyzer.h
@@ -8,7 +8,7 @@
 #ifndef STORM_UTILITY_GRAPHANALYZER_H_
 #define STORM_UTILITY_GRAPHANALYZER_H_
 
-#include "src/models/Dtmc.h"
+#include "src/models/AbstractDeterministicModel.h"
 #include "src/exceptions/InvalidArgumentException.h"
 
 #include "log4cplus/logger.h"
@@ -34,7 +34,7 @@ public:
 	 * a paths satisfying phi until psi.
 	 */
 	template <class T>
-	static void getExistsPhiUntilPsiStates(storm::models::Dtmc<T>& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, storm::storage::BitVector* existsPhiUntilPsiStates) {
+	static void getExistsPhiUntilPsiStates(storm::models::AbstractDeterministicModel<T>& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, storm::storage::BitVector* existsPhiUntilPsiStates) {
 		// Check for valid parameter.
 		if (existsPhiUntilPsiStates == nullptr) {
 			LOG4CPLUS_ERROR(logger, "Parameter 'existsPhiUntilPhiStates' must not be null.");
@@ -81,7 +81,7 @@ public:
 	 * have paths satisfying phi until psi.
 	 */
 	template <class T>
-	static void getAlwaysPhiUntilPsiStates(storm::models::Dtmc<T>& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, const storm::storage::BitVector& existsPhiUntilPsiStates, storm::storage::BitVector* alwaysPhiUntilPsiStates) {
+	static void getAlwaysPhiUntilPsiStates(storm::models::AbstractDeterministicModel<T>& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, const storm::storage::BitVector& existsPhiUntilPsiStates, storm::storage::BitVector* alwaysPhiUntilPsiStates) {
 		// Check for valid parameter.
 		if (alwaysPhiUntilPsiStates == nullptr) {
 			LOG4CPLUS_ERROR(logger, "Parameter 'alwaysPhiUntilPhiStates' must not be null.");
@@ -103,7 +103,7 @@ public:
 	 * have paths satisfying phi until psi.
 	 */
 	template <class T>
-	static void getAlwaysPhiUntilPsiStates(storm::models::Dtmc<T>& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, storm::storage::BitVector* alwaysPhiUntilPsiStates) {
+	static void getAlwaysPhiUntilPsiStates(storm::models::AbstractDeterministicModel<T>& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, storm::storage::BitVector* alwaysPhiUntilPsiStates) {
 		// Check for valid parameter.
 		if (alwaysPhiUntilPsiStates == nullptr) {
 			LOG4CPLUS_ERROR(logger, "Parameter 'alwaysPhiUntilPhiStates' must not be null.");
@@ -130,7 +130,7 @@ public:
 	 * have paths satisfying phi until psi.
 	 */
 	template <class T>
-	static void getPhiUntilPsiStates(storm::models::Dtmc<T>& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, storm::storage::BitVector* existsPhiUntilPsiStates, storm::storage::BitVector* alwaysPhiUntilPsiStates) {
+	static void getPhiUntilPsiStates(storm::models::AbstractDeterministicModel<T>& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, storm::storage::BitVector* existsPhiUntilPsiStates, storm::storage::BitVector* alwaysPhiUntilPsiStates) {
 		// Check for valid parameters.
 		if (existsPhiUntilPsiStates == nullptr) {
 			LOG4CPLUS_ERROR(logger, "Parameter 'existsPhiUntilPhiStates' must not be null.");
diff --git a/src/utility/IoUtility.cpp b/src/utility/IoUtility.cpp
index 1c2f75c3c..92d682a7b 100644
--- a/src/utility/IoUtility.cpp
+++ b/src/utility/IoUtility.cpp
@@ -17,7 +17,7 @@ namespace storm {
 	namespace utility {
 
 		void dtmcToDot(storm::models::Dtmc<double> const &dtmc, std::string filename) {
-			std::shared_ptr<storm::storage::SparseMatrix<double>> matrix(dtmc.getTransitionProbabilityMatrix());
+			std::shared_ptr<storm::storage::SparseMatrix<double>> matrix(dtmc.getTransitionMatrix());
 			std::ofstream file;
 			file.open(filename);
 
diff --git a/test/parser/ParseMdpTest.cpp b/test/parser/ParseMdpTest.cpp
index 353b470c2..0dd6a4e3b 100644
--- a/test/parser/ParseMdpTest.cpp
+++ b/test/parser/ParseMdpTest.cpp
@@ -18,7 +18,7 @@ TEST(ParseMdpTest, parseAndOutput) {
 			STORM_CPP_TESTS_BASE_PATH "/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->getTransitionProbabilityMatrix();
+	std::shared_ptr<storm::storage::SparseMatrix<double>> matrix = mdp->getTransitionMatrix();
 
 	ASSERT_EQ(mdp->getNumberOfStates(), (uint_fast64_t)3);
 	ASSERT_EQ(mdp->getNumberOfTransitions(), (uint_fast64_t)11);

From 84c159feba82bcab007169b9f4fb5a40bfe0075d Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 11 Feb 2013 15:11:34 +0100
Subject: [PATCH 4/8] Moved model information output to super class. Moved
 methods to determine data structure size to superclass(es). Added missing
 getType methods for some models.

---
 src/models/AbstractDeterministicModel.h    | 26 +++++++++++++++
 src/models/AbstractModel.h                 | 38 ++++++++++++++++++++--
 src/models/AbstractNonDeterministicModel.h | 25 +++++++++++++-
 src/models/Ctmc.h                          | 30 ++---------------
 src/models/Ctmdp.h                         | 33 +++----------------
 src/models/Dtmc.h                          | 25 ++------------
 src/models/GraphTransitions.h              | 10 ++++++
 src/models/Mdp.h                           | 25 +-------------
 8 files changed, 106 insertions(+), 106 deletions(-)

diff --git a/src/models/AbstractDeterministicModel.h b/src/models/AbstractDeterministicModel.h
index b7dc1a380..c669a295c 100644
--- a/src/models/AbstractDeterministicModel.h
+++ b/src/models/AbstractDeterministicModel.h
@@ -19,22 +19,48 @@ template<class T>
 class AbstractDeterministicModel: public AbstractModel<T> {
 
 	public:
+		/*! Constructs an abstract determinstic model from the given parameters.
+		 * @param transitionMatrix The matrix representing the transitions in the model.
+		 * @param stateLabeling The labeling that assigns a set of atomic
+		 * propositions to each state.
+		 * @param stateRewardVector The reward values associated with the states.
+		 * @param transitionRewardMatrix The reward values associated with the transitions of the model.
+		 */
 		AbstractDeterministicModel(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix,
 			std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling,
 			std::shared_ptr<std::vector<T>> stateRewardVector, std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix)
 			: AbstractModel<T>(transitionMatrix, stateLabeling, stateRewardVector, transitionRewardMatrix), backwardTransitions(nullptr) {
 		}
 
+		/*!
+		 * Destructor.
+		 */
 		virtual ~AbstractDeterministicModel() {
 			// Intentionally left empty.
 		}
 
+		/*!
+		 * Copy Constructor.
+		 */
 		AbstractDeterministicModel(AbstractDeterministicModel const& other) : AbstractModel<T>(other), backwardTransitions(nullptr) {
 			if (other.backwardTransitions != nullptr) {
 				backwardTransitions = new storm::models::GraphTransitions<T>(*other.backwardTransitions);
 			}
 		}
 
+		/*!
+		 * Retrieves the size of the internal representation of the model in memory.
+		 * @return the size of the internal representation of the model in memory
+		 * measured in bytes.
+		 */
+		virtual uint_fast64_t getSizeInMemory() const {
+			uint_fast64_t result = AbstractModel<T>::getSizeInMemory();
+			if (backwardTransitions != nullptr) {
+				result += backwardTransitions->getSizeInMemory();
+			}
+			return result;
+		}
+
 		/*!
 		 * Retrieves a reference to the backwards transition relation.
 		 * @return A reference to the backwards transition relation.
diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h
index 42aa13eb8..0f830b6fc 100644
--- a/src/models/AbstractModel.h
+++ b/src/models/AbstractModel.h
@@ -4,6 +4,7 @@
 #include "src/models/AtomicPropositionsLabeling.h"
 #include "src/storage/BitVector.h"
 #include "src/storage/SparseMatrix.h"
+#include "src/utility/CommandLine.h"
 
 #include <memory>
 #include <vector>
@@ -49,7 +50,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
 		}
 
 		/*!
-		 * Destructors.
+		 * Destructor.
 		 */
 		virtual ~AbstractModel() {
 			// Intentionally left empty.
@@ -82,7 +83,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
 		 *
 		 *	@return	Type of the model.
 		 */
-		virtual ModelType getType() = 0;
+		virtual ModelType getType() const = 0;
 
 		/*!
 		 * Returns the state space size of the model.
@@ -178,6 +179,39 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
 			return transitionRewardMatrix != nullptr;
 		}
 
+		/*!
+		 * Retrieves the size of the internal representation of the model in memory.
+		 * @return the size of the internal representation of the model in memory
+		 * measured in bytes.
+		 */
+		virtual uint_fast64_t getSizeInMemory() const {
+			uint_fast64_t result = transitionMatrix->getSizeInMemory() + stateLabeling->getSizeInMemory();
+			if (stateRewardVector != nullptr) {
+				result += stateRewardVector->size() * sizeof(T);
+			}
+			if (transitionRewardMatrix != nullptr) {
+				result += transitionRewardMatrix->getSizeInMemory();
+			}
+			return result;
+		}
+
+		/*!
+		 * Prints information about the model to the specified stream.
+		 * @param out The stream the information is to be printed to.
+		 */
+		void printModelInformationToStream(std::ostream& out) const {
+			out << "-------------------------------------------------------------- "
+				<< std::endl;
+			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);
+			out << "Size in memory: \t"
+				<< (this->getSizeInMemory())/1024 << " kbytes" << std::endl;
+			out << "-------------------------------------------------------------- "
+				<< std::endl;
+		}
+
 	private:
 		/*! A matrix representing the likelihoods of moving between states. */
 		std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix;
diff --git a/src/models/AbstractNonDeterministicModel.h b/src/models/AbstractNonDeterministicModel.h
index 153ca059c..257644093 100644
--- a/src/models/AbstractNonDeterministicModel.h
+++ b/src/models/AbstractNonDeterministicModel.h
@@ -19,7 +19,15 @@ template<class T>
 class AbstractNonDeterministicModel: public AbstractModel<T> {
 
 	public:
-	AbstractNonDeterministicModel(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix,
+		/*! Constructs an abstract non-determinstic model from the given parameters.
+		 * @param transitionMatrix The matrix representing the transitions in the model.
+		 * @param stateLabeling The labeling that assigns a set of atomic
+		 * propositions to each state.
+		 * @param choiceIndices A mapping from states to rows in the transition matrix.
+		 * @param stateRewardVector The reward values associated with the states.
+		 * @param transitionRewardMatrix The reward values associated with the transitions of the model.
+		 */
+		AbstractNonDeterministicModel(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix,
 			std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling,
 			std::shared_ptr<std::vector<uint_fast64_t>> choiceIndices,
 			std::shared_ptr<std::vector<T>> stateRewardVector,
@@ -28,13 +36,28 @@ class AbstractNonDeterministicModel: public AbstractModel<T> {
 			  choiceIndices(choiceIndices) {
 		}
 
+		/*!
+		 * Destructor.
+		 */
 		virtual ~AbstractNonDeterministicModel() {
 			// Intentionally left empty.
 		}
 
+		/*!
+		 * Copy Constructor.
+		 */
 		AbstractNonDeterministicModel(AbstractNonDeterministicModel const& other) : AbstractModel<T>(other),
 				choiceIndices(other.choiceIndices) {
+			// Intentionally left empty.
+		}
 
+		/*!
+		 * Retrieves the size of the internal representation of the model in memory.
+		 * @return the size of the internal representation of the model in memory
+		 * measured in bytes.
+		 */
+		virtual uint_fast64_t getSizeInMemory() const {
+			return AbstractModel<T>::getSizeInMemory() + choiceIndices->size() * sizeof(uint_fast64_t);
 		}
 
 	private:
diff --git a/src/models/Ctmc.h b/src/models/Ctmc.h
index 3c4a36a75..0b8eff5fd 100644
--- a/src/models/Ctmc.h
+++ b/src/models/Ctmc.h
@@ -8,17 +8,12 @@
 #ifndef STORM_MODELS_CTMC_H_
 #define STORM_MODELS_CTMC_H_
 
-#include <ostream>
-#include <iostream>
 #include <memory>
-#include <cstdlib>
+#include <vector>
 
+#include "AbstractDeterministicModel.h"
 #include "AtomicPropositionsLabeling.h"
-#include "GraphTransitions.h"
 #include "src/storage/SparseMatrix.h"
-#include "src/exceptions/InvalidArgumentException.h"
-
-#include "AbstractDeterministicModel.h"
 
 namespace storm {
 
@@ -57,26 +52,7 @@ public:
 		// Intentionally left empty.
 	}
 
-	/*!
-	 * Prints information about the model to the specified stream.
-	 * @param out The stream the information is to be printed to.
-	 */
-	void printModelInformationToStream(std::ostream& out) const {
-		out << "-------------------------------------------------------------- "
-			<< std::endl;
-		out << "Model type: \t\tCTMC" << std::endl;
-		out << "States: \t\t" << this->getNumberOfStates() << std::endl;
-		out << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl;
-		this->getStateLabeling()->printAtomicPropositionsInformationToStream(out);
-		out << "Size in memory: \t"
-			<< (this->getTransitionMatrix()->getSizeInMemory() +
-				this->stateLabeling()->getSizeInMemory() +
-				sizeof(*this))/1024 << " kbytes" << std::endl;
-		out << "-------------------------------------------------------------- "
-			<< std::endl;
-	}
-
-	storm::models::ModelType getType() {
+	storm::models::ModelType getType() const {
 		return CTMC;
 	}
 };
diff --git a/src/models/Ctmdp.h b/src/models/Ctmdp.h
index 37b73d748..3e1f8f5b8 100644
--- a/src/models/Ctmdp.h
+++ b/src/models/Ctmdp.h
@@ -8,19 +8,13 @@
 #ifndef STORM_MODELS_CTMDP_H_
 #define STORM_MODELS_CTMDP_H_
 
-#include <ostream>
-#include <iostream>
 #include <memory>
-#include <cstdlib>
+#include <vector>
 
 #include "AtomicPropositionsLabeling.h"
-#include "GraphTransitions.h"
+#include "AbstractNonDeterministicModel.h"
 #include "src/storage/SparseMatrix.h"
-#include "src/exceptions/InvalidArgumentException.h"
-#include "src/utility/CommandLine.h"
 #include "src/utility/Settings.h"
-#include "src/models/AbstractNonDeterministicModel.h"
-#include "src/parser/NonDeterministicSparseTransitionParser.h"
 
 namespace storm {
 
@@ -74,27 +68,8 @@ public:
 	~Ctmdp() {
 		// Intentionally left empty.
 	}
-	
-	/*!
-	 * Prints information about the model to the specified stream.
-	 * @param out The stream the information is to be printed to.
-	 */
-	void printModelInformationToStream(std::ostream& out) const {
-		storm::utility::printSeparationLine(out);
-		out << std::endl;
-		out << "Model type: \t\tCTMDP" << std::endl;
-		out << "States: \t\t" << this->getNumberOfStates() << std::endl;
-		out << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl;
-		this->getStateLabeling()->printAtomicPropositionsInformationToStream(out);
-		out << "Size in memory: \t"
-			<< (this->getTransitionMatrix()->getSizeInMemory() +
-				this->getStateLabeling()->getSizeInMemory() +
-				sizeof(*this))/1024 << " kbytes" << std::endl;
-		out << std::endl;
-		storm::utility::printSeparationLine(out);
-	}
-	
-	storm::models::ModelType getType() {
+
+	storm::models::ModelType getType() const {
 		return CTMDP;
 	}
 
diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h
index 42e6279d3..eefcc2ab5 100644
--- a/src/models/Dtmc.h
+++ b/src/models/Dtmc.h
@@ -13,13 +13,11 @@
 #include <memory>
 #include <cstdlib>
 
+#include "AbstractDeterministicModel.h"
 #include "AtomicPropositionsLabeling.h"
-#include "GraphTransitions.h"
 #include "src/storage/SparseMatrix.h"
 #include "src/exceptions/InvalidArgumentException.h"
-#include "src/utility/CommandLine.h"
 #include "src/utility/Settings.h"
-#include "src/models/AbstractDeterministicModel.h"
 
 namespace storm {
 
@@ -75,27 +73,8 @@ public:
 	~Dtmc() {
 		// Intentionally left empty.
 	}
-
-	/*!
-	 * Prints information about the model to the specified stream.
-	 * @param out The stream the information is to be printed to.
-	 */
-	void printModelInformationToStream(std::ostream& out) const {
-		storm::utility::printSeparationLine(out);
-		out << std::endl;
-		out << "Model type: \t\tDTMC" << std::endl;
-		out << "States: \t\t" << this->getNumberOfStates() << std::endl;
-		out << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl;
-		this->getStateLabeling()->printAtomicPropositionsInformationToStream(out);
-		out << "Size in memory: \t"
-			<< (this->getTransitionMatrix()->getSizeInMemory() +
-				this->getStateLabeling()->getSizeInMemory() +
-				sizeof(*this))/1024 << " kbytes" << std::endl;
-		out << std::endl;
-		storm::utility::printSeparationLine(out);
-	}
 	
-	storm::models::ModelType getType() {
+	storm::models::ModelType getType() const {
 		return DTMC;
 	}
 
diff --git a/src/models/GraphTransitions.h b/src/models/GraphTransitions.h
index 1cf152666..561165501 100644
--- a/src/models/GraphTransitions.h
+++ b/src/models/GraphTransitions.h
@@ -61,6 +61,16 @@ public:
 		}
 	}
 
+	/*!
+	 * Retrieves the size of the internal representation of the graph transitions in memory.
+	 * @return the size of the internal representation of the graph transitions in memory
+	 * measured in bytes.
+	 */
+	virtual uint_fast64_t getSizeInMemory() const {
+		uint_fast64_t result = sizeof(this) + (numberOfStates + numberOfNonZeroTransitions + 1) * sizeof(uint_fast64_t);
+		return result;
+	}
+
 	/*!
 	 * Returns an iterator to the successors of the given state.
 	 * @param state The state for which to get the successor iterator.
diff --git a/src/models/Mdp.h b/src/models/Mdp.h
index 357fa1433..dc92dfda6 100644
--- a/src/models/Mdp.h
+++ b/src/models/Mdp.h
@@ -14,13 +14,9 @@
 #include <cstdlib>
 
 #include "AtomicPropositionsLabeling.h"
-#include "GraphTransitions.h"
 #include "src/storage/SparseMatrix.h"
-#include "src/exceptions/InvalidArgumentException.h"
-#include "src/utility/CommandLine.h"
 #include "src/utility/Settings.h"
 #include "src/models/AbstractNonDeterministicModel.h"
-#include "src/parser/NonDeterministicSparseTransitionParser.h"
 
 namespace storm {
 
@@ -75,26 +71,7 @@ public:
 		// Intentionally left empty.
 	}
 
-	/*!
-	 * Prints information about the model to the specified stream.
-	 * @param out The stream the information is to be printed to.
-	 */
-	void printModelInformationToStream(std::ostream& out) const {
-		storm::utility::printSeparationLine(out);
-		out << std::endl;
-		out << "Model type: \t\tMDP" << std::endl;
-		out << "States: \t\t" << this->getNumberOfStates() << std::endl;
-		out << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl;
-		this->getStateLabeling()->printAtomicPropositionsInformationToStream(out);
-		out << "Size in memory: \t"
-			<< (this->getTransitionMatrix()->getSizeInMemory() +
-				this->getStateLabeling()->getSizeInMemory() +
-				sizeof(*this))/1024 << " kbytes" << std::endl;
-		out << std::endl;
-		storm::utility::printSeparationLine(out);
-	}
-	
-	storm::models::ModelType getType() {
+	storm::models::ModelType getType() const {
 		return MDP;
 	}
 

From 5d849018dea45e701e9dd4a3b02461bf7113e67b Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 11 Feb 2013 17:02:05 +0100
Subject: [PATCH 5/8] Some minor fixes to GraphAnalyzer and model checkers.

---
 src/modelchecker/EigenDtmcPrctlModelChecker.h |  19 ++-
 src/modelchecker/GmmxxDtmcPrctlModelChecker.h |  21 ++-
 src/utility/GraphAnalyzer.h                   | 120 +++++++++---------
 3 files changed, 79 insertions(+), 81 deletions(-)

diff --git a/src/modelchecker/EigenDtmcPrctlModelChecker.h b/src/modelchecker/EigenDtmcPrctlModelChecker.h
index 61867620d..6965b3a0c 100644
--- a/src/modelchecker/EigenDtmcPrctlModelChecker.h
+++ b/src/modelchecker/EigenDtmcPrctlModelChecker.h
@@ -126,17 +126,16 @@ public:
 
 		// Then, we need to identify the states which have to be taken out of the matrix, i.e.
 		// all states that have probability 0 and 1 of satisfying the until-formula.
-		storm::storage::BitVector notExistsPhiUntilPsiStates(this->getModel().getNumberOfStates());
-		storm::storage::BitVector alwaysPhiUntilPsiStates(this->getModel().getNumberOfStates());
-		storm::utility::GraphAnalyzer::getPhiUntilPsiStates<double>(this->getModel(), *leftStates, *rightStates, &notExistsPhiUntilPsiStates, &alwaysPhiUntilPsiStates);
-		notExistsPhiUntilPsiStates.complement();
+		storm::storage::BitVector statesWithProbability0(this->getModel().getNumberOfStates());
+		storm::storage::BitVector statesWithProbability1(this->getModel().getNumberOfStates());
+		storm::utility::GraphAnalyzer::performProb01(this->getModel(), *leftStates, *rightStates, &statesWithProbability0, &statesWithProbability1);
 
 		delete leftStates;
 		delete rightStates;
 
-		LOG4CPLUS_INFO(logger, "Found " << notExistsPhiUntilPsiStates.getNumberOfSetBits() << " 'no' states.");
-		LOG4CPLUS_INFO(logger, "Found " << alwaysPhiUntilPsiStates.getNumberOfSetBits() << " 'yes' states.");
-		storm::storage::BitVector maybeStates = ~(notExistsPhiUntilPsiStates | alwaysPhiUntilPsiStates);
+		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 and set values accordingly.
@@ -175,7 +174,7 @@ public:
 			Type *pb = &(b[0]); // get the address storing the data for b
 			MapType vectorB(pb, b.size()); // vectorB shares data 
 
-			this->getModel().getTransitionProbabilityMatrix()->getConstrainedRowCountVector(maybeStates, alwaysPhiUntilPsiStates, &x);
+			this->getModel().getTransitionProbabilityMatrix()->getConstrainedRowCountVector(maybeStates, statesWithProbability1, &x);
 
 			Eigen::BiCGSTAB<Eigen::SparseMatrix<Type, 1, int_fast32_t>> solver;
 			solver.compute(*eigenSubMatrix);
@@ -212,8 +211,8 @@ public:
 			delete eigenSubMatrix;
 		}
 
-		storm::utility::setVectorValues<Type>(result, notExistsPhiUntilPsiStates, storm::utility::constGetZero<Type>());
-		storm::utility::setVectorValues<Type>(result, alwaysPhiUntilPsiStates, storm::utility::constGetOne<Type>());
+		storm::utility::setVectorValues<Type>(result, statesWithProbability0, storm::utility::constGetZero<Type>());
+		storm::utility::setVectorValues<Type>(result, statesWithProbability1, storm::utility::constGetOne<Type>());
 
 		return result;
 	}
diff --git a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h
index 6d11358b9..359462c1f 100644
--- a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h
+++ b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h
@@ -111,18 +111,17 @@ public:
 
 		// Then, we need to identify the states which have to be taken out of the matrix, i.e.
 		// all states that have probability 0 and 1 of satisfying the until-formula.
-		storm::storage::BitVector notExistsPhiUntilPsiStates(this->getModel().getNumberOfStates());
-		storm::storage::BitVector alwaysPhiUntilPsiStates(this->getModel().getNumberOfStates());
-		storm::utility::GraphAnalyzer::getPhiUntilPsiStates(this->getModel(), *leftStates, *rightStates, &notExistsPhiUntilPsiStates, &alwaysPhiUntilPsiStates);
-		notExistsPhiUntilPsiStates.complement();
+		storm::storage::BitVector statesWithProbability0(this->getModel().getNumberOfStates());
+		storm::storage::BitVector statesWithProbability1(this->getModel().getNumberOfStates());
+		storm::utility::GraphAnalyzer::performProb01(this->getModel(), *leftStates, *rightStates, &statesWithProbability0, &statesWithProbability1);
 
 		// Delete sub-results that are obsolete now.
 		delete leftStates;
 		delete rightStates;
 
-		LOG4CPLUS_INFO(logger, "Found " << notExistsPhiUntilPsiStates.getNumberOfSetBits() << " 'no' states.");
-		LOG4CPLUS_INFO(logger, "Found " << alwaysPhiUntilPsiStates.getNumberOfSetBits() << " 'yes' states.");
-		storm::storage::BitVector maybeStates = ~(notExistsPhiUntilPsiStates | alwaysPhiUntilPsiStates);
+		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.
@@ -149,7 +148,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(mayBeStatesSetBitCount);
-			this->getModel().getTransitionMatrix()->getConstrainedRowCountVector(maybeStates, alwaysPhiUntilPsiStates, &b);
+			this->getModel().getTransitionMatrix()->getConstrainedRowCountVector(maybeStates, statesWithProbability1, &b);
 
 			// Solve the corresponding system of linear equations.
 			this->solveLinearEquationSystem(*gmmxxMatrix, x, b);
@@ -162,8 +161,8 @@ public:
 		}
 
 		// Set values of resulting vector that are known exactly.
-		storm::utility::setVectorValues<Type>(result, notExistsPhiUntilPsiStates, storm::utility::constGetZero<Type>());
-		storm::utility::setVectorValues<Type>(result, alwaysPhiUntilPsiStates, storm::utility::constGetOne<Type>());
+		storm::utility::setVectorValues<Type>(result, statesWithProbability0, storm::utility::constGetZero<Type>());
+		storm::utility::setVectorValues<Type>(result, statesWithProbability1, storm::utility::constGetOne<Type>());
 
 		return result;
 	}
@@ -253,7 +252,7 @@ public:
 		// Determine which states have a reward of infinity by definition.
 		storm::storage::BitVector infinityStates(this->getModel().getNumberOfStates());
 		storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true);
-		storm::utility::GraphAnalyzer::getAlwaysPhiUntilPsiStates(this->getModel(), trueStates, *targetStates, &infinityStates);
+		storm::utility::GraphAnalyzer::performProb1(this->getModel(), trueStates, *targetStates, &infinityStates);
 		infinityStates.complement();
 
 		// Create resulting vector.
diff --git a/src/utility/GraphAnalyzer.h b/src/utility/GraphAnalyzer.h
index 02c122d89..07ba3eeaf 100644
--- a/src/utility/GraphAnalyzer.h
+++ b/src/utility/GraphAnalyzer.h
@@ -22,30 +22,58 @@ namespace utility {
 
 class GraphAnalyzer {
 public:
+	/*!
+	 * Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a
+	 * deterministic model.
+	 * @param model The model whose graph structure to search.
+	 * @param phiStates The set of all states satisfying phi.
+	 * @param psiStates The set of all states satisfying psi.
+	 * @param statesWithProbability0 A pointer to a bit vector that is initially empty and will contain all states with
+	 * probability 0 after the invocation of the function.
+	 * @param statesWithProbability1 A pointer to a bit vector that is initially empty and will contain all states with
+	 * probability 1 after the invocation of the function.
+	 */
+	template <class T>
+	static void performProb01(storm::models::AbstractDeterministicModel<T>& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) {
+		// Check for valid parameters.
+		if (statesWithProbability0 == nullptr) {
+			LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability0' must not be null.");
+			throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability0' must not be null.");
+		}
+		if (statesWithProbability1 == nullptr) {
+			LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability1' must not be null.");
+			throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability1' must not be null.");
+		}
+
+		// Perform the actual search.
+		GraphAnalyzer::performProbGreater0(model, phiStates, psiStates, statesWithProbability0);
+		GraphAnalyzer::performProb1(model, phiStates, psiStates, *statesWithProbability0, statesWithProbability1);
+		statesWithProbability0->complement();
+	}
+
 	/*!
 	 * Performs a backwards depth-first search trough the underlying graph structure
-	 * of the given model to determine which states of the model can reach one
-	 * of the given target states whilst always staying in the set of filter states
-	 * before. The resulting states are written to the given bit vector.
+	 * of the given model to determine which states of the model have a positive probability
+	 * of satisfying phi until psi. The resulting states are written to the given bit vector.
 	 * @param model The model whose graph structure to search.
 	 * @param phiStates A bit vector of all states satisfying phi.
 	 * @param psiStates A bit vector of all states satisfying psi.
-	 * @param existsPhiUntilPsiStates A pointer to the result of the search for states that possess
-	 * a paths satisfying phi until psi.
+	 * @param statesWithProbabilityGreater0 A pointer to the result of the search for states that possess
+	 * a positive probability of satisfying phi until psi.
 	 */
 	template <class T>
-	static void getExistsPhiUntilPsiStates(storm::models::AbstractDeterministicModel<T>& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, storm::storage::BitVector* existsPhiUntilPsiStates) {
+	static void performProbGreater0(storm::models::AbstractDeterministicModel<T>& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, storm::storage::BitVector* statesWithProbabilityGreater0) {
 		// Check for valid parameter.
-		if (existsPhiUntilPsiStates == nullptr) {
-			LOG4CPLUS_ERROR(logger, "Parameter 'existsPhiUntilPhiStates' must not be null.");
-			throw storm::exceptions::InvalidArgumentException("Parameter 'existsPhiUntilPhiStates' must not be null.");
+		if (statesWithProbabilityGreater0 == nullptr) {
+			LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbabilityGreater0' must not be null.");
+			throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbabilityGreater0' must not be null.");
 		}
 
 		// Get the backwards transition relation from the model to ease the search.
 		storm::models::GraphTransitions<T>& backwardTransitions = model.getBackwardTransitions();
 
 		// Add all psi states as the already satisfy the condition.
-		*existsPhiUntilPsiStates |= psiStates;
+		*statesWithProbabilityGreater0 |= psiStates;
 
 		// Initialize the stack used for the DFS with the states
 		std::vector<uint_fast64_t> stack;
@@ -58,8 +86,8 @@ public:
 			stack.pop_back();
 
 			for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) {
-				if (phiStates.get(*it) && !existsPhiUntilPsiStates->get(*it)) {
-					existsPhiUntilPsiStates->set(*it, true);
+				if (phiStates.get(*it) && !statesWithProbabilityGreater0->get(*it)) {
+					statesWithProbabilityGreater0->set(*it, true);
 					stack.push_back(*it);
 				}
 			}
@@ -75,27 +103,29 @@ public:
 	 * @param model The model whose graph structure to search.
 	 * @param phiStates A bit vector of all states satisfying phi.
 	 * @param psiStates A bit vector of all states satisfying psi.
-	 * @param existsPhiUntilPsiStates A reference to a bit vector of states that possess a path
-	 * satisfying phi until psi.
+	 * @param statesWithProbabilityGreater0 A reference to a bit vector of states that possess a positive
+	 * probability mass of satisfying phi until psi.
 	 * @param alwaysPhiUntilPsiStates A pointer to the result of the search for states that only
 	 * have paths satisfying phi until psi.
 	 */
 	template <class T>
-	static void getAlwaysPhiUntilPsiStates(storm::models::AbstractDeterministicModel<T>& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, const storm::storage::BitVector& existsPhiUntilPsiStates, storm::storage::BitVector* alwaysPhiUntilPsiStates) {
+	static void performProb1(storm::models::AbstractDeterministicModel<T>& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, const storm::storage::BitVector& statesWithProbabilityGreater0, storm::storage::BitVector* statesWithProbability1) {
 		// Check for valid parameter.
-		if (alwaysPhiUntilPsiStates == nullptr) {
-			LOG4CPLUS_ERROR(logger, "Parameter 'alwaysPhiUntilPhiStates' must not be null.");
-			throw storm::exceptions::InvalidArgumentException("Parameter 'alwaysPhiUntilPhiStates' must not be null.");
+		if (statesWithProbability1 == nullptr) {
+			LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability1' must not be null.");
+			throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability1' must not be null.");
 		}
 
-		GraphAnalyzer::getExistsPhiUntilPsiStates(model, ~psiStates, ~existsPhiUntilPsiStates, alwaysPhiUntilPsiStates);
-		alwaysPhiUntilPsiStates->complement();
+		GraphAnalyzer::performProbGreater0(model, ~psiStates, ~statesWithProbabilityGreater0, statesWithProbability1);
+		statesWithProbability1->complement();
 	}
 
 	/*!
 	 * Computes the set of states of the given model for which all paths lead to
 	 * the given set of target states and only visit states from the filter set
-	 * before. The results are written to the given bit vector.
+	 * before. In order to do this, it uses the given set of states that
+	 * characterizes the states that possess at least one path to a target state.
+	 * The results are written to the given bit vector.
 	 * @param model The model whose graph structure to search.
 	 * @param phiStates A bit vector of all states satisfying phi.
 	 * @param psiStates A bit vector of all states satisfying psi.
@@ -103,49 +133,19 @@ public:
 	 * have paths satisfying phi until psi.
 	 */
 	template <class T>
-	static void getAlwaysPhiUntilPsiStates(storm::models::AbstractDeterministicModel<T>& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, storm::storage::BitVector* alwaysPhiUntilPsiStates) {
+	static void performProb1(storm::models::AbstractDeterministicModel<T>& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, storm::storage::BitVector* statesWithProbability1) {
 		// Check for valid parameter.
-		if (alwaysPhiUntilPsiStates == nullptr) {
-			LOG4CPLUS_ERROR(logger, "Parameter 'alwaysPhiUntilPhiStates' must not be null.");
-			throw storm::exceptions::InvalidArgumentException("Parameter 'alwaysPhiUntilPhiStates' must not be null.");
+		if (statesWithProbability1 == nullptr) {
+			LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability1' must not be null.");
+			throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability1' must not be null.");
 		}
 
-		storm::storage::BitVector existsPhiUntilPsiStates(model.getNumberOfStates());
-		GraphAnalyzer::getExistsPhiUntilPsiStates(model, phiStates, psiStates, &existsPhiUntilPsiStates);
-		GraphAnalyzer::getExistsPhiUntilPsiStates(model, ~psiStates, ~existsPhiUntilPsiStates, alwaysPhiUntilPsiStates);
-		alwaysPhiUntilPsiStates->complement();
+		storm::storage::BitVector* statesWithProbabilityGreater0 = new storm::storage::BitVector(model.getNumberOfStates());
+		GraphAnalyzer::performProbGreater0(model, phiStates, psiStates, statesWithProbabilityGreater0);
+		GraphAnalyzer::performProbGreater0(model, ~psiStates, ~(*statesWithProbabilityGreater0), statesWithProbability1);
+		delete statesWithProbabilityGreater0;
+		statesWithProbability1->complement();
 	}
-
-
-	/*!
-	 * Computes the set of states of the given model for which all paths lead to
-	 * the given set of target states and only visit states from the filter set
-	 * before.
-	 * @param model The model whose graph structure to search.
-	 * @param phiStates A bit vector of all states satisfying phi.
-	 * @param psiStates A bit vector of all states satisfying psi.
-	 * @param existsPhiUntilPsiStates A pointer to the result of the search for states that possess
-	 * a path satisfying phi until psi.
-	 * @param alwaysPhiUntilPsiStates A pointer to the result of the search for states that only
-	 * have paths satisfying phi until psi.
-	 */
-	template <class T>
-	static void getPhiUntilPsiStates(storm::models::AbstractDeterministicModel<T>& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, storm::storage::BitVector* existsPhiUntilPsiStates, storm::storage::BitVector* alwaysPhiUntilPsiStates) {
-		// Check for valid parameters.
-		if (existsPhiUntilPsiStates == nullptr) {
-			LOG4CPLUS_ERROR(logger, "Parameter 'existsPhiUntilPhiStates' must not be null.");
-			throw storm::exceptions::InvalidArgumentException("Parameter 'existsPhiUntilPhiStates' must not be null.");
-		}
-		if (alwaysPhiUntilPsiStates == nullptr) {
-			LOG4CPLUS_ERROR(logger, "Parameter 'alwaysPhiUntilPhiStates' must not be null.");
-			throw storm::exceptions::InvalidArgumentException("Parameter 'alwaysPhiUntilPhiStates' must not be null.");
-		}
-
-		// Perform search.
-		GraphAnalyzer::getExistsPhiUntilPsiStates(model, phiStates, psiStates, existsPhiUntilPsiStates);
-		GraphAnalyzer::getAlwaysPhiUntilPsiStates(model, phiStates, psiStates, *existsPhiUntilPsiStates, alwaysPhiUntilPsiStates);
-	}
-
 };
 
 } // namespace utility

From 19cbe13691f96a21b16383372bf01610ce75c60c Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 11 Feb 2013 19:14:13 +0100
Subject: [PATCH 6/8] Prepared methods for performing reachability searches for
 non-deterministic models. Removed storage of backward transition relation: it
 is now (re-)created on demand in the model checkers.

---
 src/models/AbstractDeterministicModel.h       | 39 +----------
 src/models/GraphTransitions.h                 |  4 +-
 ...NonDeterministicSparseTransitionParser.cpp |  4 +-
 src/utility/GraphAnalyzer.h                   | 67 +++++++++++++++++--
 4 files changed, 70 insertions(+), 44 deletions(-)

diff --git a/src/models/AbstractDeterministicModel.h b/src/models/AbstractDeterministicModel.h
index c669a295c..aa44ba736 100644
--- a/src/models/AbstractDeterministicModel.h
+++ b/src/models/AbstractDeterministicModel.h
@@ -29,7 +29,7 @@ class AbstractDeterministicModel: public AbstractModel<T> {
 		AbstractDeterministicModel(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix,
 			std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling,
 			std::shared_ptr<std::vector<T>> stateRewardVector, std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix)
-			: AbstractModel<T>(transitionMatrix, stateLabeling, stateRewardVector, transitionRewardMatrix), backwardTransitions(nullptr) {
+			: AbstractModel<T>(transitionMatrix, stateLabeling, stateRewardVector, transitionRewardMatrix) {
 		}
 
 		/*!
@@ -42,42 +42,9 @@ class AbstractDeterministicModel: public AbstractModel<T> {
 		/*!
 		 * Copy Constructor.
 		 */
-		AbstractDeterministicModel(AbstractDeterministicModel const& other) : AbstractModel<T>(other), backwardTransitions(nullptr) {
-			if (other.backwardTransitions != nullptr) {
-				backwardTransitions = new storm::models::GraphTransitions<T>(*other.backwardTransitions);
-			}
-		}
-
-		/*!
-		 * Retrieves the size of the internal representation of the model in memory.
-		 * @return the size of the internal representation of the model in memory
-		 * measured in bytes.
-		 */
-		virtual uint_fast64_t getSizeInMemory() const {
-			uint_fast64_t result = AbstractModel<T>::getSizeInMemory();
-			if (backwardTransitions != nullptr) {
-				result += backwardTransitions->getSizeInMemory();
-			}
-			return result;
-		}
-
-		/*!
-		 * Retrieves a reference to the backwards transition relation.
-		 * @return A reference to the backwards transition relation.
-		 */
-		storm::models::GraphTransitions<T>& getBackwardTransitions() {
-			if (this->backwardTransitions == nullptr) {
-				this->backwardTransitions = std::shared_ptr<storm::models::GraphTransitions<T>>(new storm::models::GraphTransitions<T>(this->getTransitionMatrix(), this->getNumberOfStates(), false));
-			}
-			return *this->backwardTransitions;
+		AbstractDeterministicModel(AbstractDeterministicModel const& other) : AbstractModel<T>(other) {
+			// Intentionally left empty.
 		}
-
-	private:
-		/*!
-		 * A data structure that stores the predecessors for all states. This is
-		 * needed for backwards directed searches.
-		 */
-		std::shared_ptr<storm::models::GraphTransitions<T>> backwardTransitions;
 };
 
 } // namespace models
diff --git a/src/models/GraphTransitions.h b/src/models/GraphTransitions.h
index 561165501..64d5c65cd 100644
--- a/src/models/GraphTransitions.h
+++ b/src/models/GraphTransitions.h
@@ -39,8 +39,8 @@ public:
 	 * @param forward If set to true, this objects will store the graph structure
 	 * of the backwards transition relation.
 	 */
-	GraphTransitions(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix, uint_fast64_t numberOfStates, bool forward)
-			: successorList(nullptr), stateIndications(nullptr), numberOfStates(numberOfStates), numberOfNonZeroTransitions(transitionMatrix->getNonZeroEntryCount()) {
+	GraphTransitions(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix, bool forward)
+			: successorList(nullptr), stateIndications(nullptr), numberOfStates(transitionMatrix->getColumnCount()), numberOfNonZeroTransitions(transitionMatrix->getNonZeroEntryCount()) {
 		if (forward) {
 			this->initializeForward(transitionMatrix);
 		} else {
diff --git a/src/parser/NonDeterministicSparseTransitionParser.cpp b/src/parser/NonDeterministicSparseTransitionParser.cpp
index f6b70e719..26436fb55 100644
--- a/src/parser/NonDeterministicSparseTransitionParser.cpp
+++ b/src/parser/NonDeterministicSparseTransitionParser.cpp
@@ -214,7 +214,7 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s
 	/*
 	 *	Create row mapping.
 	 */
-	this->rowMapping = std::shared_ptr<std::vector<uint_fast64_t>>(new std::vector<uint_fast64_t>(maxnode+1,0));
+	this->rowMapping = std::shared_ptr<std::vector<uint_fast64_t>>(new std::vector<uint_fast64_t>(maxnode+2,0));
 
 	/*
 	 *	Parse file content.
@@ -288,6 +288,8 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s
 		curRow++;
 	}
 
+	this->rowMapping->at(maxnode+1) = curRow;
+
 	if (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly.";
 
 	/*
diff --git a/src/utility/GraphAnalyzer.h b/src/utility/GraphAnalyzer.h
index 07ba3eeaf..3464c9710 100644
--- a/src/utility/GraphAnalyzer.h
+++ b/src/utility/GraphAnalyzer.h
@@ -9,6 +9,7 @@
 #define STORM_UTILITY_GRAPHANALYZER_H_
 
 #include "src/models/AbstractDeterministicModel.h"
+#include "src/models/AbstractNonDeterministicModel.h"
 #include "src/exceptions/InvalidArgumentException.h"
 
 #include "log4cplus/logger.h"
@@ -34,7 +35,7 @@ public:
 	 * probability 1 after the invocation of the function.
 	 */
 	template <class T>
-	static void performProb01(storm::models::AbstractDeterministicModel<T>& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) {
+	static void performProb01(storm::models::AbstractDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) {
 		// Check for valid parameters.
 		if (statesWithProbability0 == nullptr) {
 			LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability0' must not be null.");
@@ -62,7 +63,7 @@ public:
 	 * a positive probability of satisfying phi until psi.
 	 */
 	template <class T>
-	static void performProbGreater0(storm::models::AbstractDeterministicModel<T>& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, storm::storage::BitVector* statesWithProbabilityGreater0) {
+	static void performProbGreater0(storm::models::AbstractDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbabilityGreater0) {
 		// Check for valid parameter.
 		if (statesWithProbabilityGreater0 == nullptr) {
 			LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbabilityGreater0' must not be null.");
@@ -70,7 +71,7 @@ public:
 		}
 
 		// Get the backwards transition relation from the model to ease the search.
-		storm::models::GraphTransitions<T>& backwardTransitions = model.getBackwardTransitions();
+		storm::models::GraphTransitions<T> backwardTransitions(model.getTransitionMatrix(), false);
 
 		// Add all psi states as the already satisfy the condition.
 		*statesWithProbabilityGreater0 |= psiStates;
@@ -109,7 +110,7 @@ public:
 	 * have paths satisfying phi until psi.
 	 */
 	template <class T>
-	static void performProb1(storm::models::AbstractDeterministicModel<T>& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, const storm::storage::BitVector& statesWithProbabilityGreater0, storm::storage::BitVector* statesWithProbability1) {
+	static void performProb1(storm::models::AbstractDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0, storm::storage::BitVector* statesWithProbability1) {
 		// Check for valid parameter.
 		if (statesWithProbability1 == nullptr) {
 			LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability1' must not be null.");
@@ -133,7 +134,7 @@ public:
 	 * have paths satisfying phi until psi.
 	 */
 	template <class T>
-	static void performProb1(storm::models::AbstractDeterministicModel<T>& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, storm::storage::BitVector* statesWithProbability1) {
+	static void performProb1(storm::models::AbstractDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) {
 		// Check for valid parameter.
 		if (statesWithProbability1 == nullptr) {
 			LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability1' must not be null.");
@@ -146,6 +147,62 @@ public:
 		delete statesWithProbabilityGreater0;
 		statesWithProbability1->complement();
 	}
+
+	template <class T>
+	static void performProb01Max(storm::models::AbstractNonDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) {
+		// Check for valid parameters.
+		if (statesWithProbability0 == nullptr) {
+			LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability0' must not be null.");
+			throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability0' must not be null.");
+		}
+		if (statesWithProbability1 == nullptr) {
+			LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability1' must not be null.");
+			throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability1' must not be null.");
+		}
+
+		// Perform the actual search.
+		GraphAnalyzer::performProb0A(model, phiStates, psiStates, statesWithProbability0);
+		GraphAnalyzer::performProb1E(model, phiStates, psiStates, statesWithProbability1);
+	}
+
+	template <class T>
+	static void performProb0A(storm::models::AbstractNonDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0) {
+
+	}
+
+	template <class T>
+	static void performProb1E(storm::models::AbstractNonDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) {
+
+	}
+
+	template <class T>
+	static void performProb01Min(storm::models::AbstractNonDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) {
+		// Check for valid parameters.
+		if (statesWithProbability0 == nullptr) {
+			LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability0' must not be null.");
+			throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability0' must not be null.");
+		}
+		if (statesWithProbability1 == nullptr) {
+			LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability1' must not be null.");
+			throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability1' must not be null.");
+		}
+
+		// Perform the actual search.
+		GraphAnalyzer::performProb0E(model, phiStates, psiStates, statesWithProbability0);
+		GraphAnalyzer::performProb1A(model, phiStates, psiStates, statesWithProbability1);
+	}
+
+	template <class T>
+	static void performProb0E(storm::models::AbstractNonDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0) {
+
+	}
+
+	template <class T>
+	static void performProb1A(storm::models::AbstractNonDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) {
+		// This result is a rough guess and does not compute all states with probability 1.
+		// TODO: Check whether it makes sense to implement the precise but complicated algorithm here.
+		*statesWithProbability1 = psiStates;
+	}
 };
 
 } // namespace utility

From 73ab4a78a973dc1a0eafc20fd3a579adb2d50de4 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 11 Feb 2013 20:12:28 +0100
Subject: [PATCH 7/8] Renamed methods get*Pointer in sparse matrix class,
 because they do not return a pointer. Added initial versions of
 forward/backward graph transition creation for nondeterministic models.

---
 src/models/GraphTransitions.h | 94 ++++++++++++++++++++++++++++++-----
 src/storage/SparseMatrix.h    |  6 +--
 2 files changed, 84 insertions(+), 16 deletions(-)

diff --git a/src/models/GraphTransitions.h b/src/models/GraphTransitions.h
index 64d5c65cd..6f4da36f1 100644
--- a/src/models/GraphTransitions.h
+++ b/src/models/GraphTransitions.h
@@ -40,7 +40,7 @@ public:
 	 * of the backwards transition relation.
 	 */
 	GraphTransitions(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix, bool forward)
-			: successorList(nullptr), stateIndications(nullptr), numberOfStates(transitionMatrix->getColumnCount()), numberOfNonZeroTransitions(transitionMatrix->getNonZeroEntryCount()) {
+			: successorList(nullptr), stateIndications(nullptr), numberOfStates(transitionMatrix->getColumnCount()), numberOfTransitions(transitionMatrix->getNonZeroEntryCount()) {
 		if (forward) {
 			this->initializeForward(transitionMatrix);
 		} else {
@@ -48,6 +48,15 @@ public:
 		}
 	}
 
+	GraphTransitions(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix, std::shared_ptr<std::vector<uint_fast64_t>> choiceIndices, bool forward)
+		: successorList(nullptr), stateIndications(nullptr), numberOfStates(transitionMatrix->getColumnCount()), numberOfTransitions(transitionMatrix->getNonZeroEntryCount()) {
+		if (forward) {
+			this->initializeForward(transitionMatrix, choiceIndices);
+		} else {
+			this->initializeBackward(transitionMatrix, choiceIndices);
+		}
+	}
+
 	//! Destructor
 	/*!
 	 * Destructor. Frees the internal storage.
@@ -67,7 +76,7 @@ public:
 	 * measured in bytes.
 	 */
 	virtual uint_fast64_t getSizeInMemory() const {
-		uint_fast64_t result = sizeof(this) + (numberOfStates + numberOfNonZeroTransitions + 1) * sizeof(uint_fast64_t);
+		uint_fast64_t result = sizeof(this) + (numberOfStates + numberOfTransitions + 1) * sizeof(uint_fast64_t);
 		return result;
 	}
 
@@ -98,18 +107,37 @@ private:
 	 * relation given by means of a sparse matrix.
 	 */
 	void initializeForward(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix) {
-		this->successorList = new uint_fast64_t[numberOfNonZeroTransitions];
+		this->successorList = new uint_fast64_t[numberOfTransitions];
 		this->stateIndications = new uint_fast64_t[numberOfStates + 1];
 
 		// First, we copy the index list from the sparse matrix as this will
 		// stay the same.
-		std::copy(transitionMatrix->getRowIndicationsPointer().begin(), transitionMatrix->getRowIndicationsPointer().end(), this->stateIndications);
+		std::copy(transitionMatrix->getRowIndications().begin(), transitionMatrix->getRowIndications().end(), this->stateIndications);
 
 		// Now we can iterate over all rows of the transition matrix and record
 		// the target state.
 		for (uint_fast64_t i = 0, currentNonZeroElement = 0; i < numberOfStates; i++) {
 			for (auto rowIt = transitionMatrix->beginConstColumnIterator(i); rowIt != transitionMatrix->endConstColumnIterator(i); ++rowIt) {
-				this->stateIndications[currentNonZeroElement++] = *rowIt;
+				this->successorList[currentNonZeroElement++] = *rowIt;
+			}
+		}
+	}
+
+	void initializeForward(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix, std::shared_ptr<std::vector<uint_fast64_t>> choiceIndices) {
+		this->successorList = new uint_fast64_t[numberOfTransitions];
+		this->stateIndications = new uint_fast64_t[numberOfStates + 1];
+
+		for (uint_fast64_t i = 0; i < numberOfStates; ++i) {
+			this->stateIndications[i] = transitionMatrix->getRowIndications().at(choiceIndices->at(i));
+		}
+
+		// Now we can iterate over all rows of the transition matrix and record
+		// the target state.
+		for (uint_fast64_t i = 0, currentNonZeroElement = 0; i < numberOfStates; i++) {
+			for (uint_fast64_t j = choiceIndices->at(i); j < choiceIndices->at(i + 1); ++j) {
+				for (auto rowIt = transitionMatrix->beginConstColumnIterator(j); rowIt != transitionMatrix->endConstColumnIterator(j); ++rowIt) {
+					this->successorList[currentNonZeroElement++] = *rowIt;
+				}
 			}
 		}
 	}
@@ -120,27 +148,25 @@ private:
 	 * matrix.
 	 */
 	void initializeBackward(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix) {
-		this->successorList = new uint_fast64_t[numberOfNonZeroTransitions];
+		this->successorList = new uint_fast64_t[numberOfTransitions];
 		this->stateIndications = new uint_fast64_t[numberOfStates + 1]();
 
 		// First, we need to count how many backward transitions each state has.
-		// NOTE: We disregard the diagonal here, as we only consider "true"
-		// predecessors.
-		for (uint_fast64_t i = 0; i < numberOfStates; i++) {
+		for (uint_fast64_t i = 0; i < numberOfStates; ++i) {
 			for (auto rowIt = transitionMatrix->beginConstColumnIterator(i); rowIt != transitionMatrix->endConstColumnIterator(i); ++rowIt) {
 				this->stateIndications[*rowIt + 1]++;
 			}
 		}
 
 		// Now compute the accumulated offsets.
-		for (uint_fast64_t i = 1; i < numberOfStates; i++) {
+		for (uint_fast64_t i = 1; i < numberOfStates; ++i) {
 			this->stateIndications[i] = this->stateIndications[i - 1] + this->stateIndications[i];
 		}
 
 		// Put a sentinel element at the end of the indices list. This way,
 		// for each state i the range of indices can be read off between
 		// state_indices_list[i] and state_indices_list[i + 1].
-		this->stateIndications[numberOfStates] = numberOfNonZeroTransitions;
+		this->stateIndications[numberOfStates] = numberOfTransitions;
 
 		// Create an array that stores the next index for each state. Initially
 		// this corresponds to the previously computed accumulated offsets.
@@ -149,7 +175,7 @@ private:
 
 		// Now we are ready to actually fill in the list of predecessors for
 		// every state. Again, we start by considering all but the last row.
-		for (uint_fast64_t i = 0; i < numberOfStates; i++) {
+		for (uint_fast64_t i = 0; i < numberOfStates; ++i) {
 			for (auto rowIt = transitionMatrix->beginConstColumnIterator(i); rowIt != transitionMatrix->endConstColumnIterator(i); ++rowIt) {
 				this->successorList[nextIndicesList[*rowIt]++] = i;
 			}
@@ -159,6 +185,48 @@ private:
 		delete[] nextIndicesList;
 	}
 
+	void initializeBackward(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix, std::shared_ptr<std::vector<uint_fast64_t>> choiceIndices) {
+		this->successorList = new uint_fast64_t[numberOfTransitions];
+		this->stateIndications = new uint_fast64_t[numberOfStates + 1]();
+
+		// First, we need to count how many backward transitions each state has.
+		for (uint_fast64_t i = 0; i < numberOfStates; ++i) {
+			for (uint_fast64_t j = choiceIndices->at(i); j < choiceIndices->at(i + 1); ++j) {
+				for (auto rowIt = transitionMatrix->beginConstColumnIterator(j); rowIt != transitionMatrix->endConstColumnIterator(j); ++rowIt) {
+					this->stateIndications[*rowIt + 1]++;
+				}
+			}
+		}
+
+		// Now compute the accumulated offsets.
+		for (uint_fast64_t i = 1; i < numberOfStates; i++) {
+			this->stateIndications[i] = this->stateIndications[i - 1] + this->stateIndications[i];
+		}
+
+		// Put a sentinel element at the end of the indices list. This way,
+		// for each state i the range of indices can be read off between
+		// state_indices_list[i] and state_indices_list[i + 1].
+		this->stateIndications[numberOfStates] = numberOfTransitions;
+
+		// Create an array that stores the next index for each state. Initially
+		// this corresponds to the previously computed accumulated offsets.
+		uint_fast64_t* nextIndicesList = new uint_fast64_t[numberOfStates];
+		std::copy(stateIndications, stateIndications + numberOfStates, nextIndicesList);
+
+		// Now we are ready to actually fill in the list of predecessors for
+		// every state. Again, we start by considering all but the last row.
+		for (uint_fast64_t i = 0; i < numberOfStates; i++) {
+			for (uint_fast64_t j = choiceIndices->at(i); j < choiceIndices->at(i + 1); ++j) {
+				for (auto rowIt = transitionMatrix->beginConstColumnIterator(j); rowIt != transitionMatrix->endConstColumnIterator(j); ++rowIt) {
+					this->successorList[nextIndicesList[*rowIt]++] = i;
+				}
+			}
+		}
+
+		// Now we can dispose of the auxiliary array.
+		delete[] nextIndicesList;
+	}
+
 	/*! A list of successors for *all* states. */
 	uint_fast64_t* successorList;
 
@@ -178,7 +246,7 @@ private:
 	 * Store the number of non-zero transition entries to determine the highest
 	 * index at which the predecessor_list may be accessed.
 	 */
-	uint_fast64_t numberOfNonZeroTransitions;
+	uint_fast64_t numberOfTransitions;
 };
 
 } // namespace models
diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h
index 94d663d3b..a35df8b47 100644
--- a/src/storage/SparseMatrix.h
+++ b/src/storage/SparseMatrix.h
@@ -476,7 +476,7 @@ public:
 	 * Returns a pointer to the value storage of the matrix.
 	 * @return A pointer to the value storage of the matrix.
 	 */
-	std::vector<T> const & getStoragePointer() const {
+	std::vector<T> const& getStorage() const {
 		return valueStorage;
 	}
 
@@ -486,7 +486,7 @@ public:
 	 * @return A pointer to the array that stores the start indices of non-zero
 	 * entries in the value storage for each row.
 	 */
-	std::vector<uint_fast64_t> const & getRowIndicationsPointer() const {
+	std::vector<uint_fast64_t> const& getRowIndications() const {
 		return rowIndications;
 	}
 
@@ -496,7 +496,7 @@ public:
 	 * @return A pointer to an array that stores the column of each non-zero
 	 * element.
 	 */
-	std::vector<uint_fast64_t> const & getColumnIndicationsPointer() const {
+	std::vector<uint_fast64_t> const& getColumnIndications() const {
 		return columnIndications;
 	}
 

From 8c248c05c553118db4cb73adad471bd491610983 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 11 Feb 2013 20:47:47 +0100
Subject: [PATCH 8/8] Renamed NonDeterministic to Nondeterministic in all
 places. Fixed (hopefully) all occurrences of these names. Implemented Prob0A
 algorithm.

---
 ...odel.h => AbstractNondeterministicModel.h} | 28 ++++++++----
 src/models/Ctmdp.h                            |  8 ++--
 src/models/Mdp.h                              |  8 ++--
 src/parser/AutoParser.h                       |  6 +--
 ...er.cpp => NondeterministicModelParser.cpp} |  8 ++--
 ...Parser.h => NondeterministicModelParser.h} |  7 ++-
 ...ondeterministicSparseTransitionParser.cpp} |  6 +--
 ... NondeterministicSparseTransitionParser.h} |  4 +-
 src/utility/GraphAnalyzer.h                   | 44 ++++++++++++++++---
 test/parser/ParseMdpTest.cpp                  |  6 +--
 test/storage/SparseMatrixTest.cpp             |  8 ++--
 11 files changed, 88 insertions(+), 45 deletions(-)
 rename src/models/{AbstractNonDeterministicModel.h => AbstractNondeterministicModel.h} (65%)
 rename src/parser/{NonDeterministicModelParser.cpp => NondeterministicModelParser.cpp} (87%)
 rename src/parser/{NonDeterministicModelParser.h => NondeterministicModelParser.h} (93%)
 rename src/parser/{NonDeterministicSparseTransitionParser.cpp => NondeterministicSparseTransitionParser.cpp} (97%)
 rename src/parser/{NonDeterministicSparseTransitionParser.h => NondeterministicSparseTransitionParser.h} (88%)

diff --git a/src/models/AbstractNonDeterministicModel.h b/src/models/AbstractNondeterministicModel.h
similarity index 65%
rename from src/models/AbstractNonDeterministicModel.h
rename to src/models/AbstractNondeterministicModel.h
index 257644093..0ca1dea37 100644
--- a/src/models/AbstractNonDeterministicModel.h
+++ b/src/models/AbstractNondeterministicModel.h
@@ -16,7 +16,7 @@ namespace models {
  *	This is base class defines a common interface for all non-deterministic models.
  */
 template<class T>
-class AbstractNonDeterministicModel: public AbstractModel<T> {
+class AbstractNondeterministicModel: public AbstractModel<T> {
 
 	public:
 		/*! Constructs an abstract non-determinstic model from the given parameters.
@@ -27,27 +27,27 @@ class AbstractNonDeterministicModel: public AbstractModel<T> {
 		 * @param stateRewardVector The reward values associated with the states.
 		 * @param transitionRewardMatrix The reward values associated with the transitions of the model.
 		 */
-		AbstractNonDeterministicModel(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix,
+		AbstractNondeterministicModel(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix,
 			std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling,
-			std::shared_ptr<std::vector<uint_fast64_t>> choiceIndices,
+			std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices,
 			std::shared_ptr<std::vector<T>> stateRewardVector,
 			std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix)
 			: AbstractModel<T>(transitionMatrix, stateLabeling, stateRewardVector, transitionRewardMatrix),
-			  choiceIndices(choiceIndices) {
+			  nondeterministicChoiceIndices(nondeterministicChoiceIndices) {
 		}
 
 		/*!
 		 * Destructor.
 		 */
-		virtual ~AbstractNonDeterministicModel() {
+		virtual ~AbstractNondeterministicModel() {
 			// Intentionally left empty.
 		}
 
 		/*!
 		 * Copy Constructor.
 		 */
-		AbstractNonDeterministicModel(AbstractNonDeterministicModel const& other) : AbstractModel<T>(other),
-				choiceIndices(other.choiceIndices) {
+		AbstractNondeterministicModel(AbstractNondeterministicModel const& other) : AbstractModel<T>(other),
+				nondeterministicChoiceIndices(other.nondeterministicChoiceIndices) {
 			// Intentionally left empty.
 		}
 
@@ -57,12 +57,22 @@ class AbstractNonDeterministicModel: public AbstractModel<T> {
 		 * measured in bytes.
 		 */
 		virtual uint_fast64_t getSizeInMemory() const {
-			return AbstractModel<T>::getSizeInMemory() + choiceIndices->size() * sizeof(uint_fast64_t);
+			return AbstractModel<T>::getSizeInMemory() + nondeterministicChoiceIndices->size() * sizeof(uint_fast64_t);
+		}
+
+		/*!
+		 * Retrieves the vector indicating which matrix rows represent non-deterministic choices
+		 * of a certain state.
+		 * @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;
 		}
 
 	private:
 		/*! A vector of indices mapping states to the choices (rows) in the transition matrix. */
-		std::shared_ptr<std::vector<uint_fast64_t>> choiceIndices;
+		std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices;
 };
 
 } // namespace models
diff --git a/src/models/Ctmdp.h b/src/models/Ctmdp.h
index 3e1f8f5b8..e693c70a1 100644
--- a/src/models/Ctmdp.h
+++ b/src/models/Ctmdp.h
@@ -12,7 +12,7 @@
 #include <vector>
 
 #include "AtomicPropositionsLabeling.h"
-#include "AbstractNonDeterministicModel.h"
+#include "AbstractNondeterministicModel.h"
 #include "src/storage/SparseMatrix.h"
 #include "src/utility/Settings.h"
 
@@ -25,7 +25,7 @@ namespace models {
  * labeled with atomic propositions.
  */
 template <class T>
-class Ctmdp : public storm::models::AbstractNonDeterministicModel<T> {
+class Ctmdp : public storm::models::AbstractNondeterministicModel<T> {
 
 public:
 	//! Constructor
@@ -42,7 +42,7 @@ public:
 			std::shared_ptr<std::vector<uint_fast64_t>> choiceIndices,
 			std::shared_ptr<std::vector<T>> stateRewardVector = nullptr,
 			std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix = nullptr)
-			: AbstractNonDeterministicModel<T>(probabilityMatrix, stateLabeling, choiceIndices, stateRewardVector, transitionRewardMatrix) {
+			: AbstractNondeterministicModel<T>(probabilityMatrix, stateLabeling, choiceIndices, stateRewardVector, transitionRewardMatrix) {
 		if (!this->checkValidityOfProbabilityMatrix()) {
 			LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
 			throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
@@ -54,7 +54,7 @@ public:
 	 * Copy Constructor. Performs a deep copy of the given CTMDP.
 	 * @param ctmdp A reference to the CTMDP that is to be copied.
 	 */
-	Ctmdp(const Ctmdp<T> &ctmdp) : AbstractNonDeterministicModel<T>(ctmdp) {
+	Ctmdp(const Ctmdp<T> &ctmdp) : AbstractNondeterministicModel<T>(ctmdp) {
 		if (!this->checkValidityOfProbabilityMatrix()) {
 			LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
 			throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
diff --git a/src/models/Mdp.h b/src/models/Mdp.h
index dc92dfda6..515a1842e 100644
--- a/src/models/Mdp.h
+++ b/src/models/Mdp.h
@@ -16,7 +16,7 @@
 #include "AtomicPropositionsLabeling.h"
 #include "src/storage/SparseMatrix.h"
 #include "src/utility/Settings.h"
-#include "src/models/AbstractNonDeterministicModel.h"
+#include "src/models/AbstractNondeterministicModel.h"
 
 namespace storm {
 
@@ -27,7 +27,7 @@ namespace models {
  * labeled with atomic propositions.
  */
 template <class T>
-class Mdp : public storm::models::AbstractNonDeterministicModel<T> {
+class Mdp : public storm::models::AbstractNondeterministicModel<T> {
 
 public:
 	//! Constructor
@@ -44,7 +44,7 @@ public:
 			std::shared_ptr<std::vector<uint_fast64_t>> choiceIndices,
 			std::shared_ptr<std::vector<T>> stateRewardVector = nullptr,
 			std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix = nullptr)
-			: AbstractNonDeterministicModel<T>(probabilityMatrix, stateLabeling, choiceIndices, stateRewardVector, transitionRewardMatrix) {
+			: AbstractNondeterministicModel<T>(probabilityMatrix, stateLabeling, choiceIndices, stateRewardVector, transitionRewardMatrix) {
 		if (!this->checkValidityOfProbabilityMatrix()) {
 			LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
 			throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
@@ -56,7 +56,7 @@ public:
 	 * Copy Constructor. Performs a deep copy of the given MDP.
 	 * @param mdp A reference to the MDP that is to be copied.
 	 */
-	Mdp(const Mdp<T> &mdp) : AbstractNonDeterministicModel<T>(mdp) {
+	Mdp(const Mdp<T> &mdp) : AbstractNondeterministicModel<T>(mdp) {
 		if (!this->checkValidityOfProbabilityMatrix()) {
 			LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
 			throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
diff --git a/src/parser/AutoParser.h b/src/parser/AutoParser.h
index d7337ae54..f7331da7e 100644
--- a/src/parser/AutoParser.h
+++ b/src/parser/AutoParser.h
@@ -7,7 +7,7 @@
 #include "src/exceptions/WrongFileFormatException.h"
 #include "src/models/AbstractModel.h"
 #include "src/parser/DeterministicModelParser.h"
-#include "src/parser/NonDeterministicModelParser.h"
+#include "src/parser/NondeterministicModelParser.h"
 
 #include <memory>
 #include <iostream>
@@ -57,12 +57,12 @@ class AutoParser : Parser {
 					break;
 				}
 				case storm::models::MDP: {
-					NonDeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
+					NondeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
 					this->model = parser.getMdp();
 					break;
 				}
 				case storm::models::CTMDP: {
-					NonDeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
+					NondeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
 					this->model = parser.getCtmdp();
 					break;
 				}
diff --git a/src/parser/NonDeterministicModelParser.cpp b/src/parser/NondeterministicModelParser.cpp
similarity index 87%
rename from src/parser/NonDeterministicModelParser.cpp
rename to src/parser/NondeterministicModelParser.cpp
index 017d3b31e..036f0dc9b 100644
--- a/src/parser/NonDeterministicModelParser.cpp
+++ b/src/parser/NondeterministicModelParser.cpp
@@ -10,7 +10,7 @@
 #include <string>
 #include <vector>
 
-#include "src/parser/NonDeterministicSparseTransitionParser.h"
+#include "src/parser/NondeterministicSparseTransitionParser.h"
 #include "src/parser/AtomicPropositionLabelingParser.h"
 #include "src/parser/SparseStateRewardParser.h"
 
@@ -27,9 +27,9 @@ namespace parser {
  * @param stateRewardFile String containing the location of the state reward file (...srew)
  * @param transitionRewardFile String containing the location of the transition reward file (...trew)
  */
-NonDeterministicModelParser::NonDeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile,
+NondeterministicModelParser::NondeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile,
 		std::string const & stateRewardFile, std::string const & transitionRewardFile) {
-	storm::parser::NonDeterministicSparseTransitionParser tp(transitionSystemFile);
+	storm::parser::NondeterministicSparseTransitionParser tp(transitionSystemFile);
 	uint_fast64_t stateCount = tp.getMatrix()->getRowCount();
 
 	storm::parser::AtomicPropositionLabelingParser lp(stateCount, labelingFile);
@@ -38,7 +38,7 @@ NonDeterministicModelParser::NonDeterministicModelParser(std::string const & tra
 		this->stateRewards = srp.getStateRewards();
 	}
 	if (transitionRewardFile != "") {
-		storm::parser::NonDeterministicSparseTransitionParser trp(transitionRewardFile);
+		storm::parser::NondeterministicSparseTransitionParser trp(transitionRewardFile);
 		this->transitionRewardMatrix = trp.getMatrix();
 	}
 
diff --git a/src/parser/NonDeterministicModelParser.h b/src/parser/NondeterministicModelParser.h
similarity index 93%
rename from src/parser/NonDeterministicModelParser.h
rename to src/parser/NondeterministicModelParser.h
index 379fdf07c..bdc4c42d4 100644
--- a/src/parser/NonDeterministicModelParser.h
+++ b/src/parser/NondeterministicModelParser.h
@@ -13,6 +13,7 @@
 #include "src/models/Ctmdp.h"
 
 namespace storm {
+
 namespace parser {
 
 /*!
@@ -23,9 +24,9 @@ namespace parser {
  *
  *	@note The labeling representation in the file may use at most as much nodes as are specified in the mdp.
  */
-class NonDeterministicModelParser: public storm::parser::Parser {
+class NondeterministicModelParser: public storm::parser::Parser {
 public:
-	NonDeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile,
+	NondeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile,
 			std::string const & stateRewardFile = "", std::string const & transitionRewardFile = "");
 
 	std::shared_ptr<storm::models::Mdp<double>> getMdp() {
@@ -58,5 +59,7 @@ private:
 };
 
 } /* namespace parser */
+
 } /* namespace storm */
+
 #endif /* STORM_PARSER_NONDETERMINISTICMODELPARSER_H_ */
diff --git a/src/parser/NonDeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp
similarity index 97%
rename from src/parser/NonDeterministicSparseTransitionParser.cpp
rename to src/parser/NondeterministicSparseTransitionParser.cpp
index 26436fb55..a17f48552 100644
--- a/src/parser/NonDeterministicSparseTransitionParser.cpp
+++ b/src/parser/NondeterministicSparseTransitionParser.cpp
@@ -5,7 +5,7 @@
  *		Author: Gereon Kremer
  */
 
-#include "src/parser/NonDeterministicSparseTransitionParser.h"
+#include "src/parser/NondeterministicSparseTransitionParser.h"
 
 #include <errno.h>
 #include <time.h>
@@ -49,7 +49,7 @@ namespace parser {
  *	@param maxnode Is set to highest id of all nodes.
  *	@return The number of non-zero elements.
  */
-uint_fast64_t NonDeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode) {
+uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode) {
 	/*
 	 *	Check file header and extract number of transitions.
 	 */
@@ -154,7 +154,7 @@ uint_fast64_t NonDeterministicSparseTransitionParser::firstPass(char* buf, uint_
  *	@return a pointer to the created sparse matrix.
  */
 
-NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(std::string const &filename)
+NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(std::string const &filename)
 	: matrix(nullptr) {
 	/*
 	 *	Enforce locale where decimal point is '.'.
diff --git a/src/parser/NonDeterministicSparseTransitionParser.h b/src/parser/NondeterministicSparseTransitionParser.h
similarity index 88%
rename from src/parser/NonDeterministicSparseTransitionParser.h
rename to src/parser/NondeterministicSparseTransitionParser.h
index a0d9ea50a..209c0e7a0 100644
--- a/src/parser/NonDeterministicSparseTransitionParser.h
+++ b/src/parser/NondeterministicSparseTransitionParser.h
@@ -17,9 +17,9 @@ namespace parser {
  *	@brief	Load a nondeterministic transition system from file and create a
  *	sparse adjacency matrix whose entries represent the weights of the edges
  */
-class NonDeterministicSparseTransitionParser : public Parser {
+class NondeterministicSparseTransitionParser : public Parser {
 	public:
-		NonDeterministicSparseTransitionParser(std::string const &filename);
+		NondeterministicSparseTransitionParser(std::string const &filename);
 		
 		inline std::shared_ptr<storm::storage::SparseMatrix<double>> getMatrix() const {
 			return this->matrix;
diff --git a/src/utility/GraphAnalyzer.h b/src/utility/GraphAnalyzer.h
index 3464c9710..4b1db5178 100644
--- a/src/utility/GraphAnalyzer.h
+++ b/src/utility/GraphAnalyzer.h
@@ -9,7 +9,7 @@
 #define STORM_UTILITY_GRAPHANALYZER_H_
 
 #include "src/models/AbstractDeterministicModel.h"
-#include "src/models/AbstractNonDeterministicModel.h"
+#include "src/models/AbstractNondeterministicModel.h"
 #include "src/exceptions/InvalidArgumentException.h"
 
 #include "log4cplus/logger.h"
@@ -149,7 +149,7 @@ public:
 	}
 
 	template <class T>
-	static void performProb01Max(storm::models::AbstractNonDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) {
+	static void performProb01Max(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) {
 		// Check for valid parameters.
 		if (statesWithProbability0 == nullptr) {
 			LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability0' must not be null.");
@@ -166,17 +166,47 @@ public:
 	}
 
 	template <class T>
-	static void performProb0A(storm::models::AbstractNonDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0) {
+	static void performProb0A(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0) {
+		// Check for valid parameter.
+		if (statesWithProbability0 == nullptr) {
+			LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability0' must not be null.");
+			throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability0' must not be null.");
+		}
+
+		// Get the backwards transition relation from the model to ease the search.
+		storm::models::GraphTransitions<T> backwardTransitions(model.getTransitionMatrix(), model.getNondeterministicChoiceIndices(), false);
+
+		// Add all psi states as the already satisfy the condition.
+		*statesWithProbability0 |= psiStates;
+
+		// Initialize the stack used for the DFS with the states
+		std::vector<uint_fast64_t> stack;
+		stack.reserve(model.getNumberOfStates());
+		psiStates.getList(stack);
 
+		// Perform the actual DFS.
+		while(!stack.empty()) {
+			uint_fast64_t currentState = stack.back();
+			stack.pop_back();
+
+			for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) {
+				if (phiStates.get(*it) && !statesWithProbability0->get(*it)) {
+					statesWithProbability0->set(*it, true);
+					stack.push_back(*it);
+				}
+			}
+		}
+
+		statesWithProbability0->complement();
 	}
 
 	template <class T>
-	static void performProb1E(storm::models::AbstractNonDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) {
+	static void performProb1E(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) {
 
 	}
 
 	template <class T>
-	static void performProb01Min(storm::models::AbstractNonDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) {
+	static void performProb01Min(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) {
 		// Check for valid parameters.
 		if (statesWithProbability0 == nullptr) {
 			LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability0' must not be null.");
@@ -193,12 +223,12 @@ public:
 	}
 
 	template <class T>
-	static void performProb0E(storm::models::AbstractNonDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0) {
+	static void performProb0E(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0) {
 
 	}
 
 	template <class T>
-	static void performProb1A(storm::models::AbstractNonDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) {
+	static void performProb1A(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) {
 		// This result is a rough guess and does not compute all states with probability 1.
 		// TODO: Check whether it makes sense to implement the precise but complicated algorithm here.
 		*statesWithProbability1 = psiStates;
diff --git a/test/parser/ParseMdpTest.cpp b/test/parser/ParseMdpTest.cpp
index 0dd6a4e3b..02302dc2a 100644
--- a/test/parser/ParseMdpTest.cpp
+++ b/test/parser/ParseMdpTest.cpp
@@ -8,12 +8,12 @@
 
 #include "gtest/gtest.h"
 #include "storm-config.h"
-#include "src/parser/NonDeterministicModelParser.h"
+#include "src/parser/NondeterministicModelParser.h"
 #include "src/utility/IoUtility.h"
 
 TEST(ParseMdpTest, parseAndOutput) {
-	storm::parser::NonDeterministicModelParser* mdpParser = nullptr;
-	ASSERT_NO_THROW(mdpParser = new storm::parser::NonDeterministicModelParser(
+	storm::parser::NondeterministicModelParser* mdpParser = nullptr;
+	ASSERT_NO_THROW(mdpParser = new storm::parser::NondeterministicModelParser(
 			STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/mdp_general_input_01.tra",
 			STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab"));
 
diff --git a/test/storage/SparseMatrixTest.cpp b/test/storage/SparseMatrixTest.cpp
index 6a20050dd..69d11cc37 100644
--- a/test/storage/SparseMatrixTest.cpp
+++ b/test/storage/SparseMatrixTest.cpp
@@ -80,7 +80,7 @@ TEST(SparseMatrixTest, Test) {
 	int position_row[50] = {
 		2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
 		2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
-		2, 2, 2, 2, /* first row empty, one full row ��������� 25 minus the diagonal entry */
+		2, 2, 2, 2, /* first row empty, one full row 25 minus the diagonal entry */
 		4, 4, /* one empty row, then first and last column */
 		13, 13, 13, 13, /* a few empty rows, middle columns */
 		24, 24, 24, 24, 24, 24, 24, 24, 24, 24,
@@ -288,9 +288,9 @@ TEST(SparseMatrixTest, ConversionFromSparseEigen_RowMajor_SparseMatrixTest) {
 
 	ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::ReadReady);
 	
-	const std::vector<uint_fast64_t> rowP = ssm->getRowIndicationsPointer();
-	const std::vector<uint_fast64_t> colP = ssm->getColumnIndicationsPointer();
-	const std::vector<int> valP = ssm->getStoragePointer();
+	const std::vector<uint_fast64_t> rowP = ssm->getRowIndications();
+	const std::vector<uint_fast64_t> colP = ssm->getColumnIndications();
+	const std::vector<int> valP = ssm->getStorage();
 
 	int target = -1;
 	for (auto &coeff: tripletList) {