diff --git a/CMakeLists.txt b/CMakeLists.txt
index 1a7aa28f0..f338ee334 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -267,6 +267,8 @@ file(GLOB STORM_MODELCHECKER_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/*.h ${
 file(GLOB_RECURSE STORM_MODELCHECKER_PRCTL_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/prctl/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/prctl/*.cpp)
 file(GLOB_RECURSE STORM_MODELCHECKER_CSL_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/csl/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/csl/*.cpp)
 file(GLOB_RECURSE STORM_MODELCHECKER_REACHABILITY_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/reachability/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/reachability/*.cpp)
+file(GLOB_RECURSE STORM_MODELCHECKER_PROPOSITIONAL_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/propositional/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/propositional/*.cpp)
+file(GLOB_RECURSE STORM_MODELCHECKER_RESULTS_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/results/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/results/*.cpp)
 file(GLOB_RECURSE STORM_COUNTEREXAMPLES_FILES ${PROJECT_SOURCE_DIR}/src/counterexamples/*.h ${PROJECT_SOURCE_DIR}/src/counterexamples/*.cpp)
 file(GLOB_RECURSE STORM_MODELS_FILES ${PROJECT_SOURCE_DIR}/src/models/*.h ${PROJECT_SOURCE_DIR}/src/models/*.cpp)
 file(GLOB STORM_PARSER_FILES ${PROJECT_SOURCE_DIR}/src/parser/*.h ${PROJECT_SOURCE_DIR}/src/parser/*.cpp)
@@ -302,6 +304,8 @@ source_group(modelchecker FILES ${STORM_MODELCHECKER_FILES})
 source_group(modelchecker\\prctl FILES ${STORM_MODELCHECKER_PRCTL_FILES})
 source_group(modelchecker\\csl FILES ${STORM_MODELCHECKER_CSL_FILES})
 source_group(modelchecker\\reachability FILES ${STORM_MODELCHECKER_REACHABILITY_FILES})
+source_group(modelchecker\\propositional FILES ${STORM_MODELCHECKER_PROPOSITIONAL_FILES})
+source_group(modelchecker\\results FILES ${STORM_MODELCHECKER_RESULTS_FILES})
 source_group(counterexamples FILES ${STORM_COUNTEREXAMPLES_FILES})
 source_group(models FILES ${STORM_MODELS_FILES})
 source_group(parser FILES ${STORM_PARSER_FILES})
diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h
index 43694e74b..4e09ae838 100644
--- a/src/counterexamples/MILPMinimalLabelSetGenerator.h
+++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h
@@ -7,8 +7,8 @@
 #include "src/logic/Formulas.h"
 #include "src/storage/prism/Program.h"
 #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
-#include "src/modelchecker/ExplicitQualitativeCheckResult.h"
-#include "src/modelchecker/ExplicitQuantitativeCheckResult.h"
+#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
+#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 #include "src/exceptions/NotImplementedException.h"
 #include "src/exceptions/InvalidPropertyException.h"
 #include "src/exceptions/InvalidArgumentException.h"
diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h
index 1300b6efc..bde97a841 100644
--- a/src/counterexamples/SMTMinimalCommandSetGenerator.h
+++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h
@@ -9,7 +9,7 @@
 #include "src/storage/prism/Program.h"
 #include "src/storage/expressions/Expression.h"
 #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
-#include "src/modelchecker/ExplicitQuantitativeCheckResult.h"
+#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 #include "src/solver/GmmxxNondeterministicLinearEquationSolver.h"
 
 #include "src/utility/counterexamples.h"
diff --git a/src/logic/Formula.h b/src/logic/Formula.h
index 3de19882f..ba6dedd67 100644
--- a/src/logic/Formula.h
+++ b/src/logic/Formula.h
@@ -4,7 +4,7 @@
 #include <memory>
 #include <iostream>
 
-#include "src/modelchecker/CheckResult.h"
+#include "src/modelchecker/results/CheckResult.h"
 
 namespace storm {
     namespace logic {
diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
index 123be8cbc..f641854d4 100644
--- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
+++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
@@ -8,8 +8,8 @@
 #include "src/utility/vector.h"
 #include "src/utility/graph.h"
 
-#include "src/modelchecker/ExplicitQualitativeCheckResult.h"
-#include "src/modelchecker/ExplicitQuantitativeCheckResult.h"
+#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
+#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 
 #include "src/solver/LpSolver.h"
 
diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
index f21e4fdc4..9d12d6166 100644
--- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
+++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
@@ -6,20 +6,20 @@
 #include "src/utility/vector.h"
 #include "src/utility/graph.h"
 
-#include "src/modelchecker/ExplicitQualitativeCheckResult.h"
-#include "src/modelchecker/ExplicitQuantitativeCheckResult.h"
+#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
+#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 
 #include "src/exceptions/InvalidPropertyException.h"
 
 namespace storm {
     namespace modelchecker {
         template<typename ValueType>
-        SparseDtmcPrctlModelChecker<ValueType>::SparseDtmcPrctlModelChecker(storm::models::Dtmc<ValueType> const& model, std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>>&& linearEquationSolver) : model(model), linearEquationSolver(std::move(linearEquationSolver)) {
+        SparseDtmcPrctlModelChecker<ValueType>::SparseDtmcPrctlModelChecker(storm::models::Dtmc<ValueType> const& model, std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>>&& linearEquationSolver) : SparsePropositionalModelChecker<ValueType>(model), linearEquationSolver(std::move(linearEquationSolver)) {
             // Intentionally left empty.
         }
         
         template<typename ValueType>
-        SparseDtmcPrctlModelChecker<ValueType>::SparseDtmcPrctlModelChecker(storm::models::Dtmc<ValueType> const& model) : model(model), linearEquationSolver(storm::utility::solver::getLinearEquationSolver<ValueType>()) {
+        SparseDtmcPrctlModelChecker<ValueType>::SparseDtmcPrctlModelChecker(storm::models::Dtmc<ValueType> const& model) : SparsePropositionalModelChecker<ValueType>(model), linearEquationSolver(storm::utility::solver::getLinearEquationSolver<ValueType>()) {
             // Intentionally left empty.
         }
         
@@ -30,15 +30,15 @@ namespace storm {
         
         template<typename ValueType>
         std::vector<ValueType> SparseDtmcPrctlModelChecker<ValueType>::computeBoundedUntilProbabilitiesHelper(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound) const {
-            std::vector<ValueType> result(model.getNumberOfStates(), storm::utility::zero<ValueType>());
+            std::vector<ValueType> result(this->getModel().getNumberOfStates(), storm::utility::zero<ValueType>());
             
             // If we identify the states that have probability 0 of reaching the target states, we can exclude them in the further analysis.
-            storm::storage::BitVector statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(model.getBackwardTransitions(), phiStates, psiStates, true, stepBound);
+            storm::storage::BitVector statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(this->getModel().getBackwardTransitions(), phiStates, psiStates, true, stepBound);
             STORM_LOG_INFO("Found " << statesWithProbabilityGreater0.getNumberOfSetBits() << " 'maybe' states.");
             
             if (!statesWithProbabilityGreater0.empty()) {
                 // We can eliminate the rows and columns from the original transition probability matrix that have probability 0.
-                storm::storage::SparseMatrix<ValueType> submatrix = model.getTransitionMatrix().getSubmatrix(true, statesWithProbabilityGreater0, statesWithProbabilityGreater0, true);
+                storm::storage::SparseMatrix<ValueType> submatrix = this->getModel().getTransitionMatrix().getSubmatrix(true, statesWithProbabilityGreater0, statesWithProbabilityGreater0, true);
                 
                 // Compute the new set of target states in the reduced system.
                 storm::storage::BitVector rightStatesInReducedSystem = psiStates % statesWithProbabilityGreater0;
@@ -76,12 +76,12 @@ namespace storm {
         template<typename ValueType>
         std::vector<ValueType> SparseDtmcPrctlModelChecker<ValueType>::computeNextProbabilitiesHelper(storm::storage::BitVector const& nextStates) {
             // Create the vector with which to multiply and initialize it correctly.
-            std::vector<ValueType> result(model.getNumberOfStates());
+            std::vector<ValueType> result(this->getModel().getNumberOfStates());
             storm::utility::vector::setVectorValues(result, nextStates, storm::utility::one<ValueType>());
             
             // Perform one single matrix-vector multiplication.
             STORM_LOG_THROW(linearEquationSolver != nullptr, storm::exceptions::InvalidStateException, "No valid linear equation solver available.");
-            this->linearEquationSolver->performMatrixVectorMultiplication(model.getTransitionMatrix(), result);
+            this->linearEquationSolver->performMatrixVectorMultiplication(this->getModel().getTransitionMatrix(), result);
             return result;
         }
         
@@ -96,7 +96,7 @@ namespace storm {
         std::vector<ValueType> SparseDtmcPrctlModelChecker<ValueType>::computeUntilProbabilitiesHelper(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) const {
             // 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.
-            std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(model, phiStates, psiStates);
+            std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(this->getModel(), phiStates, psiStates);
             storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first);
             storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second);
             
@@ -107,7 +107,7 @@ namespace storm {
             STORM_LOG_INFO("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
             
             // Create resulting vector.
-            std::vector<ValueType> result(model.getNumberOfStates());
+            std::vector<ValueType> result(this->getModel().getNumberOfStates());
             
             // Check whether we need to compute exact probabilities for some states.
             if (qualitative) {
@@ -118,7 +118,7 @@ namespace storm {
                     // In this case we have have to compute the probabilities.
                     
                     // We can eliminate the rows and columns from the original transition probability matrix.
-                    storm::storage::SparseMatrix<ValueType> submatrix = model.getTransitionMatrix().getSubmatrix(true, maybeStates, maybeStates, true);
+                    storm::storage::SparseMatrix<ValueType> submatrix = this->getModel().getTransitionMatrix().getSubmatrix(true, maybeStates, maybeStates, true);
                     
                     // 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.
@@ -131,7 +131,7 @@ namespace storm {
                     
                     // 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<ValueType> b = model.getTransitionMatrix().getConstrainedRowSumVector(maybeStates, statesWithProbability1);
+                    std::vector<ValueType> b = this->getModel().getTransitionMatrix().getConstrainedRowSumVector(maybeStates, statesWithProbability1);
                     
                     // Now solve the created system of linear equations.
                     STORM_LOG_THROW(linearEquationSolver != nullptr, storm::exceptions::InvalidStateException, "No valid linear equation solver available.");
@@ -160,31 +160,31 @@ namespace storm {
         
         template<typename ValueType>
         std::vector<ValueType> SparseDtmcPrctlModelChecker<ValueType>::computeCumulativeRewardsHelper(uint_fast64_t stepBound) const {
-            // Only compute the result if the model has at least one reward model.
-            STORM_LOG_THROW(model.hasStateRewards() || model.hasTransitionRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
+            // Only compute the result if the model has at least one reward this->getModel().
+            STORM_LOG_THROW(this->getModel().hasStateRewards() || this->getModel().hasTransitionRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
             
             // Compute the reward vector to add in each step based on the available reward models.
             std::vector<ValueType> totalRewardVector;
-            if (model.hasTransitionRewards()) {
-                totalRewardVector = model.getTransitionMatrix().getPointwiseProductRowSumVector(model.getTransitionRewardMatrix());
-                if (model.hasStateRewards()) {
-                    storm::utility::vector::addVectorsInPlace(totalRewardVector, model.getStateRewardVector());
+            if (this->getModel().hasTransitionRewards()) {
+                totalRewardVector = this->getModel().getTransitionMatrix().getPointwiseProductRowSumVector(this->getModel().getTransitionRewardMatrix());
+                if (this->getModel().hasStateRewards()) {
+                    storm::utility::vector::addVectorsInPlace(totalRewardVector, this->getModel().getStateRewardVector());
                 }
             } else {
-                totalRewardVector = std::vector<ValueType>(model.getStateRewardVector());
+                totalRewardVector = std::vector<ValueType>(this->getModel().getStateRewardVector());
             }
             
             // Initialize result to either the state rewards of the model or the null vector.
             std::vector<ValueType> result;
-            if (model.hasStateRewards()) {
-                result = std::vector<ValueType>(model.getStateRewardVector());
+            if (this->getModel().hasStateRewards()) {
+                result = std::vector<ValueType>(this->getModel().getStateRewardVector());
             } else {
-                result.resize(model.getNumberOfStates());
+                result.resize(this->getModel().getNumberOfStates());
             }
             
             // Perform the matrix vector multiplication as often as required by the formula bound.
             STORM_LOG_THROW(linearEquationSolver != nullptr, storm::exceptions::InvalidStateException, "No valid linear equation solver available.");
-            this->linearEquationSolver->performMatrixVectorMultiplication(model.getTransitionMatrix(), result, &totalRewardVector, stepBound);
+            this->linearEquationSolver->performMatrixVectorMultiplication(this->getModel().getTransitionMatrix(), result, &totalRewardVector, stepBound);
             
             return result;
         }
@@ -196,15 +196,15 @@ namespace storm {
         
         template<typename ValueType>
         std::vector<ValueType> SparseDtmcPrctlModelChecker<ValueType>::computeInstantaneousRewardsHelper(uint_fast64_t stepCount) const {
-            // Only compute the result if the model has a state-based reward model.
-            STORM_LOG_THROW(model.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
+            // Only compute the result if the model has a state-based reward this->getModel().
+            STORM_LOG_THROW(this->getModel().hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
             
-            // Initialize result to state rewards of the model.
-            std::vector<ValueType> result(model.getStateRewardVector());
+            // Initialize result to state rewards of the this->getModel().
+            std::vector<ValueType> result(this->getModel().getStateRewardVector());
             
             // Perform the matrix vector multiplication as often as required by the formula bound.
             STORM_LOG_THROW(linearEquationSolver != nullptr, storm::exceptions::InvalidStateException, "No valid linear equation solver available.");
-            this->linearEquationSolver->performMatrixVectorMultiplication(model.getTransitionMatrix(), result, nullptr, stepCount);
+            this->linearEquationSolver->performMatrixVectorMultiplication(this->getModel().getTransitionMatrix(), result, nullptr, stepCount);
             
             return result;
         }
@@ -216,12 +216,12 @@ namespace storm {
         
         template<typename ValueType>
         std::vector<ValueType> SparseDtmcPrctlModelChecker<ValueType>::computeReachabilityRewardsHelper(storm::storage::BitVector const& targetStates, bool qualitative) const {
-            // Only compute the result if the model has at least one reward model.
-            STORM_LOG_THROW(model.hasStateRewards() || model.hasTransitionRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
+            // Only compute the result if the model has at least one reward this->getModel().
+            STORM_LOG_THROW(this->getModel().hasStateRewards() || this->getModel().hasTransitionRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
             
             // Determine which states have a reward of infinity by definition.
-            storm::storage::BitVector trueStates(model.getNumberOfStates(), true);
-            storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(model.getBackwardTransitions(), trueStates, targetStates);
+            storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true);
+            storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(this->getModel().getBackwardTransitions(), trueStates, targetStates);
             infinityStates.complement();
             storm::storage::BitVector maybeStates = ~targetStates & ~infinityStates;
             STORM_LOG_INFO("Found " << infinityStates.getNumberOfSetBits() << " 'infinity' states.");
@@ -229,7 +229,7 @@ namespace storm {
             STORM_LOG_INFO("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
             
             // Create resulting vector.
-            std::vector<ValueType> result(model.getNumberOfStates());
+            std::vector<ValueType> result(this->getModel().getNumberOfStates());
             
             // Check whether we need to compute exact rewards for some states.
             if (qualitative) {
@@ -239,7 +239,7 @@ namespace storm {
             } else {
                 // In this case we have to compute the reward values for the remaining states.
                 // We can eliminate the rows and columns from the original transition probability matrix.
-                storm::storage::SparseMatrix<ValueType> submatrix = model.getTransitionMatrix().getSubmatrix(true, maybeStates, maybeStates, true);
+                storm::storage::SparseMatrix<ValueType> submatrix = this->getModel().getTransitionMatrix().getSubmatrix(true, maybeStates, maybeStates, true);
                 
                 // 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.
@@ -251,20 +251,20 @@ namespace storm {
                 
                 // Prepare the right-hand side of the equation system.
                 std::vector<ValueType> b(submatrix.getRowCount());
-                if (model.hasTransitionRewards()) {
+                if (this->getModel().hasTransitionRewards()) {
                     // If a transition-based reward model is available, we initialize the right-hand
                     // side to the vector resulting from summing the rows of the pointwise product
                     // of the transition probability matrix and the transition reward matrix.
-                    std::vector<ValueType> pointwiseProductRowSumVector = model.getTransitionMatrix().getPointwiseProductRowSumVector(model.getTransitionRewardMatrix());
+                    std::vector<ValueType> pointwiseProductRowSumVector = this->getModel().getTransitionMatrix().getPointwiseProductRowSumVector(this->getModel().getTransitionRewardMatrix());
                     storm::utility::vector::selectVectorValues(b, maybeStates, pointwiseProductRowSumVector);
                     
-                    if (model.hasStateRewards()) {
+                    if (this->getModel().hasStateRewards()) {
                         // If a state-based reward model is also available, we need to add this vector
                         // as well. As the state reward vector contains entries not just for the states
                         // that we still consider (i.e. maybeStates), we need to extract these values
                         // first.
                         std::vector<ValueType> subStateRewards(b.size());
-                        storm::utility::vector::selectVectorValues(subStateRewards, maybeStates, model.getStateRewardVector());
+                        storm::utility::vector::selectVectorValues(subStateRewards, maybeStates, this->getModel().getStateRewardVector());
                         storm::utility::vector::addVectorsInPlace(b, subStateRewards);
                     }
                 } else {
@@ -272,7 +272,7 @@ namespace storm {
                     // right-hand side. As the state reward vector contains entries not just for the
                     // states that we still consider (i.e. maybeStates), we need to extract these values
                     // first.
-                    storm::utility::vector::selectVectorValues(b, maybeStates, model.getStateRewardVector());
+                    storm::utility::vector::selectVectorValues(b, maybeStates, this->getModel().getStateRewardVector());
                 }
                 
                 // Now solve the resulting equation system.
@@ -298,18 +298,8 @@ namespace storm {
         }
         
         template<typename ValueType>
-        std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<ValueType>::checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) {
-            if (stateFormula.isTrueFormula()) {
-                return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(storm::storage::BitVector(model.getNumberOfStates(), true)));
-            } else {
-                return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(storm::storage::BitVector(model.getNumberOfStates())));
-            }
-        }
-        
-        template<typename ValueType>
-        std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<ValueType>::checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) {
-            STORM_LOG_THROW(model.hasAtomicProposition(stateFormula.getLabel()), storm::exceptions::InvalidPropertyException, "The property refers to unknown label '" << stateFormula.getLabel() << "'.");
-            return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(model.getLabeledStates(stateFormula.getLabel())));
+        storm::models::Dtmc<ValueType> const& SparseDtmcPrctlModelChecker<ValueType>::getModel() const {
+            return this->template getModelAs<storm::models::Dtmc<ValueType>>();
         }
         
         template class SparseDtmcPrctlModelChecker<double>;
diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
index f48465b58..f7557d63b 100644
--- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
+++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
@@ -1,7 +1,7 @@
 #ifndef STORM_MODELCHECKER_SPARSEDTMCPRCTLMODELCHECKER_H_
 #define STORM_MODELCHECKER_SPARSEDTMCPRCTLMODELCHECKER_H_
 
-#include "src/modelchecker/AbstractModelChecker.h"
+#include "src/modelchecker/propositional/SparsePropositionalModelChecker.h"
 #include "src/models/Dtmc.h"
 #include "src/utility/solver.h"
 #include "src/solver/LinearEquationSolver.h"
@@ -10,7 +10,7 @@ namespace storm {
     namespace modelchecker {
         
         template<class ValueType>
-        class SparseDtmcPrctlModelChecker : public AbstractModelChecker {
+        class SparseDtmcPrctlModelChecker : public SparsePropositionalModelChecker<ValueType> {
         public:
             explicit SparseDtmcPrctlModelChecker(storm::models::Dtmc<ValueType> const& model);
             explicit SparseDtmcPrctlModelChecker(storm::models::Dtmc<ValueType> const& model, std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>>&& linearEquationSolver);
@@ -23,8 +23,9 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
             virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
             virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
-            virtual std::unique_ptr<CheckResult> checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) override;
-            virtual std::unique_ptr<CheckResult> checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) override;
+            
+        protected:
+            storm::models::Dtmc<ValueType> const& getModel() const override;
             
         private:
             // The methods that perform the actual checking.
@@ -35,9 +36,6 @@ namespace storm {
             std::vector<ValueType> computeCumulativeRewardsHelper(uint_fast64_t stepBound) const;
             std::vector<ValueType> computeReachabilityRewardsHelper(storm::storage::BitVector const& targetStates, bool qualitative) const;
             
-            // The model this model checker is supposed to analyze.
-            storm::models::Dtmc<ValueType> const& model;
-            
             // An object that is used for solving linear equations and performing matrix-vector multiplication.
             std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> linearEquationSolver;
         };
diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
index c1c760f99..a12489838 100644
--- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
+++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
@@ -7,20 +7,20 @@
 #include "src/utility/vector.h"
 #include "src/utility/graph.h"
 
-#include "src/modelchecker/ExplicitQualitativeCheckResult.h"
-#include "src/modelchecker/ExplicitQuantitativeCheckResult.h"
+#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
+#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 
 #include "src/exceptions/InvalidPropertyException.h"
 
 namespace storm {
     namespace modelchecker {
         template<typename ValueType>
-        SparseMdpPrctlModelChecker<ValueType>::SparseMdpPrctlModelChecker(storm::models::Mdp<ValueType> const& model) : model(model), nondeterministicLinearEquationSolver(storm::utility::solver::getNondeterministicLinearEquationSolver<ValueType>()) {
+        SparseMdpPrctlModelChecker<ValueType>::SparseMdpPrctlModelChecker(storm::models::Mdp<ValueType> const& model) : SparsePropositionalModelChecker<ValueType>(model), nondeterministicLinearEquationSolver(storm::utility::solver::getNondeterministicLinearEquationSolver<ValueType>()) {
             // Intentionally left empty.
         }
         
         template<typename ValueType>
-        SparseMdpPrctlModelChecker<ValueType>::SparseMdpPrctlModelChecker(storm::models::Mdp<ValueType> const& model, std::shared_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> nondeterministicLinearEquationSolver) : model(model), nondeterministicLinearEquationSolver(nondeterministicLinearEquationSolver) {
+        SparseMdpPrctlModelChecker<ValueType>::SparseMdpPrctlModelChecker(storm::models::Mdp<ValueType> const& model, std::shared_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> nondeterministicLinearEquationSolver) : SparsePropositionalModelChecker<ValueType>(model), nondeterministicLinearEquationSolver(nondeterministicLinearEquationSolver) {
             // Intentionally left empty.
         }
         
@@ -31,20 +31,20 @@ namespace storm {
         
         template<typename ValueType>
         std::vector<ValueType> SparseMdpPrctlModelChecker<ValueType>::computeBoundedUntilProbabilitiesHelper(bool minimize, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound) const {
-            std::vector<ValueType> result(model.getNumberOfStates(), storm::utility::zero<ValueType>());
+            std::vector<ValueType> result(this->getModel().getNumberOfStates(), storm::utility::zero<ValueType>());
             
             // Determine the states that have 0 probability of reaching the target states.
             storm::storage::BitVector statesWithProbabilityGreater0;
             if (minimize) {
-                statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0A(model.getTransitionMatrix(), model.getTransitionMatrix().getRowGroupIndices(), model.getBackwardTransitions(), phiStates, psiStates, true, stepBound);
+                statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0A(this->getModel().getTransitionMatrix(), this->getModel().getTransitionMatrix().getRowGroupIndices(), this->getModel().getBackwardTransitions(), phiStates, psiStates, true, stepBound);
             } else {
-                statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0E(model.getTransitionMatrix(), model.getTransitionMatrix().getRowGroupIndices(), model.getBackwardTransitions(), phiStates, psiStates, true, stepBound);
+                statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0E(this->getModel().getTransitionMatrix(), this->getModel().getTransitionMatrix().getRowGroupIndices(), this->getModel().getBackwardTransitions(), phiStates, psiStates, true, stepBound);
             }
             STORM_LOG_INFO("Found " << statesWithProbabilityGreater0.getNumberOfSetBits() << " 'maybe' states.");
             
             if (!statesWithProbabilityGreater0.empty()) {
                 // We can eliminate the rows and columns from the original transition probability matrix that have probability 0.
-                storm::storage::SparseMatrix<ValueType> submatrix = model.getTransitionMatrix().getSubmatrix(true, statesWithProbabilityGreater0, statesWithProbabilityGreater0, false);
+                storm::storage::SparseMatrix<ValueType> submatrix = this->getModel().getTransitionMatrix().getSubmatrix(true, statesWithProbabilityGreater0, statesWithProbabilityGreater0, false);
                 
                 // Compute the new set of target states in the reduced system.
                 storm::storage::BitVector rightStatesInReducedSystem = psiStates % statesWithProbabilityGreater0;
@@ -69,7 +69,7 @@ namespace storm {
         
         template<typename ValueType>
         std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<ValueType>::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
-            STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
+            STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic this->getModel().");
             std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula());
             std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
             ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
@@ -81,23 +81,28 @@ namespace storm {
         template<typename ValueType>
         std::vector<ValueType> SparseMdpPrctlModelChecker<ValueType>::computeNextProbabilitiesHelper(bool minimize, storm::storage::BitVector const& nextStates) {
             // Create the vector with which to multiply and initialize it correctly.
-            std::vector<ValueType> result(model.getNumberOfStates());
+            std::vector<ValueType> result(this->getModel().getNumberOfStates());
             storm::utility::vector::setVectorValues(result, nextStates, storm::utility::one<ValueType>());
             
             STORM_LOG_THROW(nondeterministicLinearEquationSolver != nullptr, storm::exceptions::InvalidStateException, "No valid equation solver available.");
-            this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(minimize, model.getTransitionMatrix(), result);
+            this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(minimize, this->getModel().getTransitionMatrix(), result);
             
             return result;
         }
         
         template<typename ValueType>
         std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<ValueType>::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
-            STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
+            STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic this->getModel().");
             std::unique_ptr<CheckResult> subResultPointer = this->check(pathFormula.getSubformula());
             ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeNextProbabilitiesHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, subResult.getTruthValuesVector())));
         }
         
+        template<typename ValueType>
+        std::vector<ValueType> SparseMdpPrctlModelChecker<ValueType>::computeUntilProbabilitiesHelper(bool minimize, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) const {
+            return computeUntilProbabilitiesHelper(minimize, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), phiStates, psiStates, nondeterministicLinearEquationSolver, qualitative);
+        }
+        
         template<typename ValueType>
         std::vector<ValueType> SparseMdpPrctlModelChecker<ValueType>::computeUntilProbabilitiesHelper(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::shared_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> nondeterministicLinearEquationSolver, bool qualitative) {
             size_t numberOfStates = phiStates.size();
@@ -156,81 +161,81 @@ namespace storm {
         
         template<typename ValueType>
         std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<ValueType>::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
-            STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
+            STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic this->getModel().");
             std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula());
             std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
             ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
             ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
-            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(SparseMdpPrctlModelChecker<ValueType>::computeUntilProbabilitiesHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, model.getTransitionMatrix(), model.getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), nondeterministicLinearEquationSolver, qualitative)));
+            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(SparseMdpPrctlModelChecker<ValueType>::computeUntilProbabilitiesHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), nondeterministicLinearEquationSolver, qualitative)));
         }
         
         template<typename ValueType>
         std::vector<ValueType> SparseMdpPrctlModelChecker<ValueType>::computeCumulativeRewardsHelper(bool minimize, uint_fast64_t stepBound) const {
-            // Only compute the result if the model has at least one reward model.
-            STORM_LOG_THROW(model.hasStateRewards() || model.hasTransitionRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
+            // Only compute the result if the model has at least one reward this->getModel().
+            STORM_LOG_THROW(this->getModel().hasStateRewards() || this->getModel().hasTransitionRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
             
             // Compute the reward vector to add in each step based on the available reward models.
             std::vector<ValueType> totalRewardVector;
-            if (model.hasTransitionRewards()) {
-                totalRewardVector = model.getTransitionMatrix().getPointwiseProductRowSumVector(model.getTransitionRewardMatrix());
-                if (model.hasStateRewards()) {
-                    storm::utility::vector::addVectorsInPlace(totalRewardVector, model.getStateRewardVector());
+            if (this->getModel().hasTransitionRewards()) {
+                totalRewardVector = this->getModel().getTransitionMatrix().getPointwiseProductRowSumVector(this->getModel().getTransitionRewardMatrix());
+                if (this->getModel().hasStateRewards()) {
+                    storm::utility::vector::addVectorsInPlace(totalRewardVector, this->getModel().getStateRewardVector());
                 }
             } else {
-                totalRewardVector = std::vector<ValueType>(model.getStateRewardVector());
+                totalRewardVector = std::vector<ValueType>(this->getModel().getStateRewardVector());
             }
             
             // Initialize result to either the state rewards of the model or the null vector.
             std::vector<ValueType> result;
-            if (model.hasStateRewards()) {
-                result = std::vector<ValueType>(model.getStateRewardVector());
+            if (this->getModel().hasStateRewards()) {
+                result = std::vector<ValueType>(this->getModel().getStateRewardVector());
             } else {
-                result.resize(model.getNumberOfStates());
+                result.resize(this->getModel().getNumberOfStates());
             }
             
-            this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(minimize, model.getTransitionMatrix(), result, &totalRewardVector, stepBound);
+            this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(minimize, this->getModel().getTransitionMatrix(), result, &totalRewardVector, stepBound);
             
             return result;
         }
         
         template<typename ValueType>
         std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<ValueType>::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
-            STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
+            STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic this->getModel().");
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeCumulativeRewardsHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, rewardPathFormula.getStepBound())));
         }
         
         template<typename ValueType>
         std::vector<ValueType> SparseMdpPrctlModelChecker<ValueType>::computeInstantaneousRewardsHelper(bool minimize, uint_fast64_t stepCount) const {
-            // Only compute the result if the model has a state-based reward model.
-            STORM_LOG_THROW(model.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
+            // Only compute the result if the model has a state-based reward this->getModel().
+            STORM_LOG_THROW(this->getModel().hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
             
-            // Initialize result to state rewards of the model.
-            std::vector<ValueType> result(model.getStateRewardVector());
+            // Initialize result to state rewards of the this->getModel().
+            std::vector<ValueType> result(this->getModel().getStateRewardVector());
             
             STORM_LOG_THROW(nondeterministicLinearEquationSolver != nullptr, storm::exceptions::InvalidStateException, "No valid linear equation solver available.");
-            this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(minimize, model.getTransitionMatrix(), result, nullptr, stepCount);
+            this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(minimize, this->getModel().getTransitionMatrix(), result, nullptr, stepCount);
             
             return result;
         }
         
         template<typename ValueType>
         std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<ValueType>::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
-            STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
+            STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic this->getModel().");
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeInstantaneousRewardsHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, rewardPathFormula.getStepCount())));
         }
         
         template<typename ValueType>
         std::vector<ValueType> SparseMdpPrctlModelChecker<ValueType>::computeReachabilityRewardsHelper(bool minimize, storm::storage::BitVector const& targetStates, bool qualitative) const {
-            // Only compute the result if the model has at least one reward model.
-            STORM_LOG_THROW(model.hasStateRewards() || model.hasTransitionRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
+            // Only compute the result if the model has at least one reward this->getModel().
+            STORM_LOG_THROW(this->getModel().hasStateRewards() || this->getModel().hasTransitionRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
             
             // Determine which states have a reward of infinity by definition.
             storm::storage::BitVector infinityStates;
-            storm::storage::BitVector trueStates(model.getNumberOfStates(), true);
+            storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true);
             if (minimize) {
-                infinityStates = std::move(storm::utility::graph::performProb1A(model.getTransitionMatrix(), model.getTransitionMatrix().getRowGroupIndices(), model.getBackwardTransitions(), trueStates, targetStates));
+                infinityStates = std::move(storm::utility::graph::performProb1A(this->getModel().getTransitionMatrix(), this->getModel().getTransitionMatrix().getRowGroupIndices(), this->getModel().getBackwardTransitions(), trueStates, targetStates));
             } else {
-                infinityStates = std::move(storm::utility::graph::performProb1E(model.getTransitionMatrix(), model.getTransitionMatrix().getRowGroupIndices(), model.getBackwardTransitions(), trueStates, targetStates));
+                infinityStates = std::move(storm::utility::graph::performProb1E(this->getModel().getTransitionMatrix(), this->getModel().getTransitionMatrix().getRowGroupIndices(), this->getModel().getBackwardTransitions(), trueStates, targetStates));
             }
             infinityStates.complement();
             storm::storage::BitVector maybeStates = ~targetStates & ~infinityStates;
@@ -239,10 +244,10 @@ namespace storm {
             LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
             
             // Create resulting vector.
-            std::vector<ValueType> result(model.getNumberOfStates());
+            std::vector<ValueType> result(this->getModel().getNumberOfStates());
             
             // Check whether we need to compute exact rewards for some states.
-            if (model.getInitialStates().isDisjointFrom(maybeStates)) {
+            if (this->getModel().getInitialStates().isDisjointFrom(maybeStates)) {
                 LOG4CPLUS_INFO(logger, "The rewards for the initial states were determined in a preprocessing step."
                                << " No exact rewards were computed.");
                 // Set the values for all maybe-states to 1 to indicate that their reward values
@@ -253,26 +258,26 @@ namespace storm {
                 
                 // We can eliminate the rows and columns from the original transition probability matrix for states
                 // whose reward values are already known.
-                storm::storage::SparseMatrix<ValueType> submatrix = model.getTransitionMatrix().getSubmatrix(true, maybeStates, maybeStates, false);
+                storm::storage::SparseMatrix<ValueType> submatrix = this->getModel().getTransitionMatrix().getSubmatrix(true, maybeStates, maybeStates, false);
                 
                 // 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<ValueType> b(submatrix.getRowCount());
                 
-                if (model.hasTransitionRewards()) {
+                if (this->getModel().hasTransitionRewards()) {
                     // If a transition-based reward model is available, we initialize the right-hand
                     // side to the vector resulting from summing the rows of the pointwise product
                     // of the transition probability matrix and the transition reward matrix.
-                    std::vector<ValueType> pointwiseProductRowSumVector = model.getTransitionMatrix().getPointwiseProductRowSumVector(model.getTransitionRewardMatrix());
-                    storm::utility::vector::selectVectorValues(b, maybeStates, model.getTransitionMatrix().getRowGroupIndices(), pointwiseProductRowSumVector);
+                    std::vector<ValueType> pointwiseProductRowSumVector = this->getModel().getTransitionMatrix().getPointwiseProductRowSumVector(this->getModel().getTransitionRewardMatrix());
+                    storm::utility::vector::selectVectorValues(b, maybeStates, this->getModel().getTransitionMatrix().getRowGroupIndices(), pointwiseProductRowSumVector);
                     
-                    if (model.hasStateRewards()) {
+                    if (this->getModel().hasStateRewards()) {
                         // If a state-based reward model is also available, we need to add this vector
                         // as well. As the state reward vector contains entries not just for the states
                         // that we still consider (i.e. maybeStates), we need to extract these values
                         // first.
                         std::vector<ValueType> subStateRewards(b.size());
-                        storm::utility::vector::selectVectorValuesRepeatedly(subStateRewards, maybeStates, model.getTransitionMatrix().getRowGroupIndices(), model.getStateRewardVector());
+                        storm::utility::vector::selectVectorValuesRepeatedly(subStateRewards, maybeStates, this->getModel().getTransitionMatrix().getRowGroupIndices(), this->getModel().getStateRewardVector());
                         storm::utility::vector::addVectorsInPlace(b, subStateRewards);
                     }
                 } else {
@@ -280,7 +285,7 @@ namespace storm {
                     // right-hand side. As the state reward vector contains entries not just for the
                     // states that we still consider (i.e. maybeStates), we need to extract these values
                     // first.
-                    storm::utility::vector::selectVectorValuesRepeatedly(b, maybeStates, model.getTransitionMatrix().getRowGroupIndices(), model.getStateRewardVector());
+                    storm::utility::vector::selectVectorValuesRepeatedly(b, maybeStates, this->getModel().getTransitionMatrix().getRowGroupIndices(), this->getModel().getStateRewardVector());
                 }
                 
                 // Create vector for results for maybe states.
@@ -302,27 +307,17 @@ namespace storm {
         
         template<typename ValueType>
         std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<ValueType>::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
-            STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
+            STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic this->getModel().");
             std::unique_ptr<CheckResult> subResultPointer = this->check(rewardPathFormula.getSubformula());
             ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeReachabilityRewardsHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, subResult.getTruthValuesVector(), qualitative)));
         }
         
         template<typename ValueType>
-        std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<ValueType>::checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) {
-            if (stateFormula.isTrueFormula()) {
-                return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(storm::storage::BitVector(model.getNumberOfStates(), true)));
-            } else {
-                return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(storm::storage::BitVector(model.getNumberOfStates())));
-            }
-        }
-        
-        template<typename ValueType>
-        std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<ValueType>::checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) {
-            STORM_LOG_THROW(model.hasAtomicProposition(stateFormula.getLabel()), storm::exceptions::InvalidPropertyException, "The property refers to unknown label '" << stateFormula.getLabel() << "'.");
-            return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(model.getLabeledStates(stateFormula.getLabel())));
+        storm::models::Mdp<ValueType> const& SparseMdpPrctlModelChecker<ValueType>::getModel() const {
+            return this->template getModelAs<storm::models::Mdp<ValueType>>();
         }
-        
+                
         template class SparseMdpPrctlModelChecker<double>;
     }
 }
\ No newline at end of file
diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
index a3a7a9c08..848abc452 100644
--- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
+++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
@@ -1,7 +1,7 @@
 #ifndef STORM_MODELCHECKER_SPARSEMDPPRCTLMODELCHECKER_H_
 #define STORM_MODELCHECKER_SPARSEMDPPRCTLMODELCHECKER_H_
 
-#include "src/modelchecker/AbstractModelChecker.h"
+#include "src/modelchecker/propositional/SparsePropositionalModelChecker.h"
 #include "src/models/Mdp.h"
 #include "src/utility/solver.h"
 #include "src/solver/NondeterministicLinearEquationSolver.h"
@@ -19,7 +19,7 @@ namespace storm {
         class SparseMarkovAutomatonCslModelChecker;
         
         template<class ValueType>
-        class SparseMdpPrctlModelChecker : public AbstractModelChecker {
+        class SparseMdpPrctlModelChecker : public SparsePropositionalModelChecker<ValueType> {
         public:
             friend class SparseMarkovAutomatonCslModelChecker<ValueType>;
             friend class counterexamples::SMTMinimalCommandSetGenerator<ValueType>;
@@ -35,8 +35,9 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
             virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
             virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
-            virtual std::unique_ptr<CheckResult> checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) override;
-            virtual std::unique_ptr<CheckResult> checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) override;
+            
+        protected:
+            storm::models::Mdp<ValueType> const& getModel() const override;
             
         private:
             // The methods that perform the actual checking.
@@ -48,9 +49,6 @@ namespace storm {
             std::vector<ValueType> computeCumulativeRewardsHelper(bool minimize, uint_fast64_t stepBound) const;
             std::vector<ValueType> computeReachabilityRewardsHelper(bool minimize, storm::storage::BitVector const& targetStates, bool qualitative) const;
             
-            // The model this model checker is supposed to analyze.
-            storm::models::Mdp<ValueType> const& model;
-            
             // A solver that is used for solving systems of linear equations that are the result of nondeterministic choices.
             std::shared_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> nondeterministicLinearEquationSolver;
         };
diff --git a/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp b/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp
new file mode 100644
index 000000000..a4e540300
--- /dev/null
+++ b/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp
@@ -0,0 +1,58 @@
+#include "src/modelchecker/propositional/SparsePropositionalModelChecker.h"
+
+#include "storm-config.h"
+#include "src/storage/parameters.h"
+
+#include "src/models/Dtmc.h"
+#include "src/models/Mdp.h"
+
+#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
+
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidPropertyException.h"
+
+namespace storm {
+    namespace modelchecker {
+        template<typename ValueType>
+        SparsePropositionalModelChecker<ValueType>::SparsePropositionalModelChecker(storm::models::AbstractModel<ValueType> const& model) : model(model) {
+            // Intentionally left empty.
+        }
+        
+        template<typename ValueType>
+        std::unique_ptr<CheckResult> SparsePropositionalModelChecker<ValueType>::checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) {
+            if (stateFormula.isTrueFormula()) {
+                return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(storm::storage::BitVector(model.getNumberOfStates(), true)));
+            } else {
+                return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(storm::storage::BitVector(model.getNumberOfStates())));
+            }
+        }
+        
+        template<typename ValueType>
+        std::unique_ptr<CheckResult> SparsePropositionalModelChecker<ValueType>::checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) {
+            STORM_LOG_THROW(model.hasAtomicProposition(stateFormula.getLabel()), storm::exceptions::InvalidPropertyException, "The property refers to unknown label '" << stateFormula.getLabel() << "'.");
+            return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(model.getLabeledStates(stateFormula.getLabel())));
+        }
+        
+        template<typename ValueType>
+        storm::models::AbstractModel<ValueType> const& SparsePropositionalModelChecker<ValueType>::getModel() const {
+            return model;
+        }
+        
+        template<typename ValueType>
+        template<typename ModelType>
+        ModelType const& SparsePropositionalModelChecker<ValueType>::getModelAs() const {
+            return dynamic_cast<ModelType const&>(model);
+        }
+        
+        // Explicitly instantiate the template class.
+        template storm::models::Dtmc<double> const& SparsePropositionalModelChecker<double>::getModelAs() const;
+        template storm::models::Mdp<double> const& SparsePropositionalModelChecker<double>::getModelAs() const;
+        template class SparsePropositionalModelChecker<double>;
+        
+#ifdef PARAMETRIC_SYSTEMS
+        template storm::models::Dtmc<storm::RationalFunction> const& SparsePropositionalModelChecker<storm::RationalFunction>::getModelAs() const;
+        template storm::models::Mdp<storm::RationalFunction> const& SparsePropositionalModelChecker<storm::RationalFunction>::getModelAs() const;
+        template class SparsePropositionalModelChecker<storm::RationalFunction>;
+#endif
+    }
+}
\ No newline at end of file
diff --git a/src/modelchecker/propositional/SparsePropositionalModelChecker.h b/src/modelchecker/propositional/SparsePropositionalModelChecker.h
new file mode 100644
index 000000000..c6309e4f0
--- /dev/null
+++ b/src/modelchecker/propositional/SparsePropositionalModelChecker.h
@@ -0,0 +1,43 @@
+#ifndef STORM_MODELCHECKER_SPARSEPROPOSITIONALMODELCHECKER_H_
+#define STORM_MODELCHECKER_SPARSEPROPOSITIONALMODELCHECKER_H_
+
+#include "src/modelchecker/AbstractModelChecker.h"
+
+#include "src/models/AbstractModel.h"
+
+namespace storm {
+    namespace modelchecker {
+        
+        template<typename ValueType>
+        class SparsePropositionalModelChecker : public AbstractModelChecker {
+        public:
+            explicit SparsePropositionalModelChecker(storm::models::AbstractModel<ValueType> const& model);
+            
+            // The implemented methods of the AbstractModelChecker interface.
+            virtual std::unique_ptr<CheckResult> checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) override;
+            virtual std::unique_ptr<CheckResult> checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) override;
+            
+        protected:
+            /*!
+             * Retrieves the model associated with this model checker instance.
+             *
+             * @return The model associated with this model checker instance.
+             */
+            virtual storm::models::AbstractModel<ValueType> const& getModel() const;
+            
+            /*!
+             * Retrieves the model associated with this model checker instance as the given template parameter type.
+             *
+             * @return The model associated with this model checker instance.
+             */
+            template<typename ModelType>
+            ModelType const& getModelAs() const;
+            
+        private:
+            // The model that is to be analyzed by the model checker.
+            storm::models::AbstractModel<ValueType> const& model;
+        };
+    }
+}
+
+#endif /* STORM_MODELCHECKER_SPARSEPROPOSITIONALMODELCHECKER_H_ */
\ No newline at end of file
diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
index c2c4f8cb1..950e0d834 100644
--- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
+++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
@@ -9,8 +9,8 @@
 
 #include "src/storage/StronglyConnectedComponentDecomposition.h"
 
-#include "src/modelchecker/ExplicitQualitativeCheckResult.h"
-#include "src/modelchecker/ExplicitQuantitativeCheckResult.h"
+#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
+#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 
 #include "src/utility/graph.h"
 #include "src/utility/vector.h"
diff --git a/src/modelchecker/CheckResult.cpp b/src/modelchecker/results/CheckResult.cpp
similarity index 95%
rename from src/modelchecker/CheckResult.cpp
rename to src/modelchecker/results/CheckResult.cpp
index e646d4633..735e6c021 100644
--- a/src/modelchecker/CheckResult.cpp
+++ b/src/modelchecker/results/CheckResult.cpp
@@ -1,10 +1,10 @@
-#include "src/modelchecker/CheckResult.h"
+#include "src/modelchecker/results/CheckResult.h"
 
 #include "storm-config.h"
 #include "src/storage/parameters.h"
 
-#include "src/modelchecker/ExplicitQualitativeCheckResult.h"
-#include "src/modelchecker/ExplicitQuantitativeCheckResult.h"
+#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
+#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 
 #include "src/utility/macros.h"
 #include "src/exceptions/InvalidOperationException.h"
diff --git a/src/modelchecker/CheckResult.h b/src/modelchecker/results/CheckResult.h
similarity index 100%
rename from src/modelchecker/CheckResult.h
rename to src/modelchecker/results/CheckResult.h
diff --git a/src/modelchecker/ExplicitQualitativeCheckResult.cpp b/src/modelchecker/results/ExplicitQualitativeCheckResult.cpp
similarity index 99%
rename from src/modelchecker/ExplicitQualitativeCheckResult.cpp
rename to src/modelchecker/results/ExplicitQualitativeCheckResult.cpp
index 114819af6..167837a19 100644
--- a/src/modelchecker/ExplicitQualitativeCheckResult.cpp
+++ b/src/modelchecker/results/ExplicitQualitativeCheckResult.cpp
@@ -1,4 +1,4 @@
-#include "src/modelchecker/ExplicitQualitativeCheckResult.h"
+#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
 
 #include "src/utility/macros.h"
 #include "src/exceptions/InvalidOperationException.h"
diff --git a/src/modelchecker/ExplicitQualitativeCheckResult.h b/src/modelchecker/results/ExplicitQualitativeCheckResult.h
similarity index 97%
rename from src/modelchecker/ExplicitQualitativeCheckResult.h
rename to src/modelchecker/results/ExplicitQualitativeCheckResult.h
index 7c56fd8bb..2cda892b9 100644
--- a/src/modelchecker/ExplicitQualitativeCheckResult.h
+++ b/src/modelchecker/results/ExplicitQualitativeCheckResult.h
@@ -5,7 +5,7 @@
 #include <functional>
 #include <boost/variant.hpp>
 
-#include "src/modelchecker/QualitativeCheckResult.h"
+#include "src/modelchecker/results/QualitativeCheckResult.h"
 #include "src/storage/sparse/StateType.h"
 #include "src/storage/BitVector.h"
 #include "src/utility/OsDetection.h"
diff --git a/src/modelchecker/ExplicitQuantitativeCheckResult.cpp b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
similarity index 98%
rename from src/modelchecker/ExplicitQuantitativeCheckResult.cpp
rename to src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
index f6d79429c..d1c5aebae 100644
--- a/src/modelchecker/ExplicitQuantitativeCheckResult.cpp
+++ b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
@@ -1,6 +1,6 @@
-#include "src/modelchecker/ExplicitQuantitativeCheckResult.h"
+#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 
-#include "src/modelchecker/ExplicitQualitativeCheckResult.h"
+#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
 #include "src/storage/BitVector.h"
 #include "src/utility/macros.h"
 #include "src/exceptions/InvalidOperationException.h"
diff --git a/src/modelchecker/ExplicitQuantitativeCheckResult.h b/src/modelchecker/results/ExplicitQuantitativeCheckResult.h
similarity index 97%
rename from src/modelchecker/ExplicitQuantitativeCheckResult.h
rename to src/modelchecker/results/ExplicitQuantitativeCheckResult.h
index 699840c05..85f1218fd 100644
--- a/src/modelchecker/ExplicitQuantitativeCheckResult.h
+++ b/src/modelchecker/results/ExplicitQuantitativeCheckResult.h
@@ -5,7 +5,7 @@
 #include <map>
 #include <boost/variant.hpp>
 
-#include "src/modelchecker/QuantitativeCheckResult.h"
+#include "src/modelchecker/results/QuantitativeCheckResult.h"
 #include "src/storage/sparse/StateType.h"
 #include "src/utility/OsDetection.h"
 
diff --git a/src/modelchecker/QualitativeCheckResult.cpp b/src/modelchecker/results/QualitativeCheckResult.cpp
similarity index 70%
rename from src/modelchecker/QualitativeCheckResult.cpp
rename to src/modelchecker/results/QualitativeCheckResult.cpp
index 5a0dab196..88cc4b956 100644
--- a/src/modelchecker/QualitativeCheckResult.cpp
+++ b/src/modelchecker/results/QualitativeCheckResult.cpp
@@ -1,4 +1,4 @@
-#include "src/modelchecker/QualitativeCheckResult.h"
+#include "src/modelchecker/results/QualitativeCheckResult.h"
 
 namespace storm {
     namespace modelchecker {
diff --git a/src/modelchecker/QualitativeCheckResult.h b/src/modelchecker/results/QualitativeCheckResult.h
similarity index 74%
rename from src/modelchecker/QualitativeCheckResult.h
rename to src/modelchecker/results/QualitativeCheckResult.h
index 88691e1c6..40675add8 100644
--- a/src/modelchecker/QualitativeCheckResult.h
+++ b/src/modelchecker/results/QualitativeCheckResult.h
@@ -1,7 +1,7 @@
 #ifndef STORM_MODELCHECKER_QUALITATIVECHECKRESULT_H_
 #define STORM_MODELCHECKER_QUALITATIVECHECKRESULT_H_
 
-#include "src/modelchecker/CheckResult.h"
+#include "src/modelchecker/results/CheckResult.h"
 
 namespace storm {
     namespace modelchecker {
diff --git a/src/modelchecker/QuantitativeCheckResult.cpp b/src/modelchecker/results/QuantitativeCheckResult.cpp
similarity index 89%
rename from src/modelchecker/QuantitativeCheckResult.cpp
rename to src/modelchecker/results/QuantitativeCheckResult.cpp
index df03db786..0b6e2c9d2 100644
--- a/src/modelchecker/QuantitativeCheckResult.cpp
+++ b/src/modelchecker/results/QuantitativeCheckResult.cpp
@@ -1,4 +1,4 @@
-#include "src/modelchecker/QuantitativeCheckResult.h"
+#include "src/modelchecker/results/QuantitativeCheckResult.h"
 
 #include "storm-config.h"
 #include "src/storage/parameters.h"
diff --git a/src/modelchecker/QuantitativeCheckResult.h b/src/modelchecker/results/QuantitativeCheckResult.h
similarity index 76%
rename from src/modelchecker/QuantitativeCheckResult.h
rename to src/modelchecker/results/QuantitativeCheckResult.h
index 73eda6c6a..9abad1652 100644
--- a/src/modelchecker/QuantitativeCheckResult.h
+++ b/src/modelchecker/results/QuantitativeCheckResult.h
@@ -1,7 +1,7 @@
 #ifndef STORM_MODELCHECKER_QUANTITATIVECHECKRESULT_H_
 #define STORM_MODELCHECKER_QUANTITATIVECHECKRESULT_H_
 
-#include "src/modelchecker/CheckResult.h"
+#include "src/modelchecker/results/CheckResult.h"
 
 namespace storm {
     namespace modelchecker {
diff --git a/src/models/AbstractDeterministicModel.h b/src/models/AbstractDeterministicModel.h
index 28953c878..379e571b3 100644
--- a/src/models/AbstractDeterministicModel.h
+++ b/src/models/AbstractDeterministicModel.h
@@ -70,7 +70,14 @@ class AbstractDeterministicModel: public AbstractModel<T> {
 		AbstractDeterministicModel(AbstractDeterministicModel && other) : AbstractModel<T>(std::move(other)) {
 			// Intentionally left empty.
 		}
-        
+    
+    AbstractDeterministicModel<T>& operator=(AbstractDeterministicModel<T>&& model) {
+        if (this != &model) {
+            AbstractModel<T>::operator=(std::move(model));
+        }
+        return *this;
+    }
+    
 		/*!
 		 * Calculates a hash over all values contained in this Model.
 		 * @return size_t A Hash Value
diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h
index 8f093f8cf..a3287a85b 100644
--- a/src/models/AbstractModel.h
+++ b/src/models/AbstractModel.h
@@ -105,6 +105,17 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
                 transitionRewardMatrix(std::move(optionalTransitionRewardMatrix)) {
             // Intentionally left empty.
         }
+    
+    AbstractModel<T>& operator=(AbstractModel<T>&& model) {
+        if (this != &model) {
+            this->transitionMatrix = std::move(model.transitionMatrix);
+            this->choiceLabeling = std::move(model.choiceLabeling);
+            this->stateLabeling = std::move(model.stateLabeling);
+            this->stateRewardVector = std::move(model.stateRewardVector);
+            this->transitionRewardMatrix = std::move(model.transitionRewardMatrix);
+        }
+        return *this;
+    }
 
 		/*!
 		 * Destructor.
diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h
index 06f3911cd..b42e0c9e3 100644
--- a/src/models/Dtmc.h
+++ b/src/models/Dtmc.h
@@ -106,6 +106,13 @@ public:
 	Dtmc(Dtmc<T>&& dtmc) : AbstractDeterministicModel<T>(std::move(dtmc)) {
 		// Intentionally left empty.
 	}
+    
+    Dtmc<T>& operator=(Dtmc<T>&& dtmc) {
+        if (this != &dtmc) {
+            AbstractDeterministicModel<T>::operator=(std::move(dtmc));
+        }
+        return *this;
+    }
 
 	//! Destructor
 	/*!
diff --git a/src/stormParametric.cpp b/src/stormParametric.cpp
index 3adba87ff..6d71b4955 100644
--- a/src/stormParametric.cpp
+++ b/src/stormParametric.cpp
@@ -208,10 +208,10 @@ void check() {
     if (storm::settings::generalSettings().isBisimulationSet()) {
         if (measureDrivenBisimulation) {
             storm::storage::DeterministicModelBisimulationDecomposition<ValueType> bisimulationDecomposition(*dtmc, phiLabel, psiLabel, checkRewards, storm::settings::bisimulationSettings().isWeakBisimulationSet(), false, true);
-            dtmc = bisimulationDecomposition.getQuotient()->template as<storm::models::Dtmc<ValueType>>();
+            *dtmc = std::move(*bisimulationDecomposition.getQuotient()->template as<storm::models::Dtmc<ValueType>>());
         } else {
             storm::storage::DeterministicModelBisimulationDecomposition<ValueType> bisimulationDecomposition(*dtmc, boost::optional<std::set<std::string>>(), checkRewards, storm::settings::bisimulationSettings().isWeakBisimulationSet(), true);
-            dtmc = bisimulationDecomposition.getQuotient()->template as<storm::models::Dtmc<ValueType>>();
+            *dtmc = std::move(*bisimulationDecomposition.getQuotient()->template as<storm::models::Dtmc<ValueType>>());
         }
         
         dtmc->printModelInformationToStream(std::cout);
@@ -231,6 +231,7 @@ void check() {
     if (std::is_same<ValueType, storm::RationalFunction>::value) {
         printApproximateResult(result->asExplicitQuantitativeCheckResult<ValueType>()[*model->getInitialStates().begin()]);
     }
+    std::cout << std::endl;
 }
 
 /*!
diff --git a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
index 8afe7ddd3..d4942a59d 100644
--- a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
@@ -4,7 +4,7 @@
 #include "src/logic/Formulas.h"
 #include "src/solver/GmmxxLinearEquationSolver.h"
 #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
-#include "src/modelchecker/ExplicitQuantitativeCheckResult.h"
+#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 #include "src/settings/SettingsManager.h"
 #include "src/settings/SettingMemento.h"
 #include "src/parser/AutoParser.h"
diff --git a/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp b/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp
index 52ec38e24..80a1d8760 100644
--- a/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp
+++ b/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp
@@ -4,7 +4,7 @@
 #include "src/logic/Formulas.h"
 #include "src/solver/GmmxxLinearEquationSolver.h"
 #include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h"
-#include "src/modelchecker/ExplicitQuantitativeCheckResult.h"
+#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 #include "src/settings/SettingsManager.h"
 #include "src/settings/SettingMemento.h"
 #include "src/parser/AutoParser.h"
diff --git a/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
index 525d69d0e..e7fb71382 100644
--- a/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
@@ -4,7 +4,7 @@
 #include "src/logic/Formulas.h"
 #include "src/solver/NativeNondeterministicLinearEquationSolver.h"
 #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
-#include "src/modelchecker/ExplicitQuantitativeCheckResult.h"
+#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 #include "src/settings/SettingsManager.h"
 #include "src/parser/AutoParser.h"
 
diff --git a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
index df2c40732..97a44d2be 100644
--- a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
+++ b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
@@ -3,7 +3,7 @@
 #include "src/settings/SettingsManager.h"
 #include "src/settings/SettingMemento.h"
 #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
-#include "src/modelchecker/ExplicitQuantitativeCheckResult.h"
+#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 #include "src/solver/GmmxxLinearEquationSolver.h"
 #include "src/parser/AutoParser.h"
 
diff --git a/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
index 402eae502..2f3794675 100644
--- a/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
+++ b/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
@@ -3,7 +3,7 @@
 
 #include "src/settings/SettingsManager.h"
 #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
-#include "src/modelchecker/ExplicitQuantitativeCheckResult.h"
+#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 #include "src/solver/NativeNondeterministicLinearEquationSolver.h"
 #include "src/parser/AutoParser.h"