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] 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);