diff --git a/test/functional/builder/wlan0-2-4.nm b/resources/examples/testfiles/mdp/wlan0-2-4.nm
similarity index 100%
rename from test/functional/builder/wlan0-2-4.nm
rename to resources/examples/testfiles/mdp/wlan0-2-4.nm
diff --git a/src/storm/abstraction/AbstractionInformation.cpp b/src/storm/abstraction/AbstractionInformation.cpp
index f2999f9cd..4da158bf7 100644
--- a/src/storm/abstraction/AbstractionInformation.cpp
+++ b/src/storm/abstraction/AbstractionInformation.cpp
@@ -1,12 +1,12 @@
-#include "src/abstraction/AbstractionInformation.h"
+#include "storm/abstraction/AbstractionInformation.h"
 
-#include "src/storage/dd/DdManager.h"
+#include "storm/storage/dd/DdManager.h"
 
-#include "src/utility/macros.h"
-#include "src/exceptions/InvalidOperationException.h"
+#include "storm/utility/macros.h"
+#include "storm/exceptions/InvalidOperationException.h"
 
-#include "src/storage/expressions/Expression.h"
-#include "src/storage/expressions/ExpressionManager.h"
+#include "storm/storage/expressions/Expression.h"
+#include "storm/storage/expressions/ExpressionManager.h"
 
 namespace storm {
     namespace abstraction {
diff --git a/src/storm/abstraction/AbstractionInformation.h b/src/storm/abstraction/AbstractionInformation.h
index dcd35f52c..64265f202 100644
--- a/src/storm/abstraction/AbstractionInformation.h
+++ b/src/storm/abstraction/AbstractionInformation.h
@@ -4,9 +4,9 @@
 #include <set>
 #include <cstdint>
 
-#include "src/storage/dd/DdType.h"
+#include "storm/storage/dd/DdType.h"
 
-#include "src/storage/dd/Bdd.h"
+#include "storm/storage/dd/Bdd.h"
 
 namespace storm {
     namespace expressions {
@@ -524,4 +524,4 @@ namespace storm {
         };
         
     }
-}
\ No newline at end of file
+}
diff --git a/src/storm/abstraction/BottomStateResult.cpp b/src/storm/abstraction/BottomStateResult.cpp
index 32b1417b7..a5f9576af 100644
--- a/src/storm/abstraction/BottomStateResult.cpp
+++ b/src/storm/abstraction/BottomStateResult.cpp
@@ -1,4 +1,4 @@
-#include "src/abstraction/BottomStateResult.h"
+#include "storm/abstraction/BottomStateResult.h"
 
 namespace storm {
     namespace abstraction {
@@ -11,4 +11,4 @@ namespace storm {
         template class BottomStateResult<storm::dd::DdType::CUDD>;
         template class BottomStateResult<storm::dd::DdType::Sylvan>;
     }
-}
\ No newline at end of file
+}
diff --git a/src/storm/abstraction/BottomStateResult.h b/src/storm/abstraction/BottomStateResult.h
index c3f2f69d4..e5b158c14 100644
--- a/src/storm/abstraction/BottomStateResult.h
+++ b/src/storm/abstraction/BottomStateResult.h
@@ -1,7 +1,7 @@
 #pragma once
 
-#include "src/storage/dd/DdType.h"
-#include "src/storage/dd/Bdd.h"
+#include "storm/storage/dd/DdType.h"
+#include "storm/storage/dd/Bdd.h"
 
 namespace storm {
     namespace abstraction {
@@ -16,4 +16,4 @@ namespace storm {
         };
         
     }
-}
\ No newline at end of file
+}
diff --git a/src/storm/abstraction/LocalExpressionInformation.cpp b/src/storm/abstraction/LocalExpressionInformation.cpp
index 91a1af80d..6424c55c1 100644
--- a/src/storm/abstraction/LocalExpressionInformation.cpp
+++ b/src/storm/abstraction/LocalExpressionInformation.cpp
@@ -1,8 +1,8 @@
-#include "src/abstraction/LocalExpressionInformation.h"
+#include "storm/abstraction/LocalExpressionInformation.h"
 
 #include <boost/algorithm/string/join.hpp>
 
-#include "src/utility/macros.h"
+#include "storm/utility/macros.h"
 
 namespace storm {
     namespace abstraction {
@@ -193,4 +193,4 @@ namespace storm {
         }
         
     }
-}
\ No newline at end of file
+}
diff --git a/src/storm/abstraction/LocalExpressionInformation.h b/src/storm/abstraction/LocalExpressionInformation.h
index b9fc39b91..391ed32aa 100644
--- a/src/storm/abstraction/LocalExpressionInformation.h
+++ b/src/storm/abstraction/LocalExpressionInformation.h
@@ -5,8 +5,8 @@
 #include <vector>
 #include <ostream>
 
-#include "src/storage/expressions/Variable.h"
-#include "src/storage/expressions/Expression.h"
+#include "storm/storage/expressions/Variable.h"
+#include "storm/storage/expressions/Expression.h"
 
 namespace storm {
     namespace abstraction {
diff --git a/src/storm/abstraction/MenuGame.cpp b/src/storm/abstraction/MenuGame.cpp
index 82ad3ebfe..eb203a48d 100644
--- a/src/storm/abstraction/MenuGame.cpp
+++ b/src/storm/abstraction/MenuGame.cpp
@@ -1,16 +1,16 @@
-#include "src/abstraction/MenuGame.h"
+#include "storm/abstraction/MenuGame.h"
 
-#include "src/exceptions/InvalidOperationException.h"
-#include "src/exceptions/InvalidArgumentException.h"
+#include "storm/exceptions/InvalidOperationException.h"
+#include "storm/exceptions/InvalidArgumentException.h"
 
-#include "src/storage/dd/Bdd.h"
-#include "src/storage/dd/Add.h"
-#include "src/storage/dd/DdManager.h"
+#include "storm/storage/dd/Bdd.h"
+#include "storm/storage/dd/Add.h"
+#include "storm/storage/dd/DdManager.h"
 
-#include "src/models/symbolic/StandardRewardModel.h"
+#include "storm/models/symbolic/StandardRewardModel.h"
 
 #include "storm-config.h"
-#include "src/adapters/CarlAdapter.h"
+#include "storm/adapters/CarlAdapter.h"
 
 namespace storm {
     namespace abstraction {
diff --git a/src/storm/abstraction/MenuGame.h b/src/storm/abstraction/MenuGame.h
index e559632b1..2cc45ba25 100644
--- a/src/storm/abstraction/MenuGame.h
+++ b/src/storm/abstraction/MenuGame.h
@@ -2,9 +2,9 @@
 
 #include <map>
 
-#include "src/models/symbolic/StochasticTwoPlayerGame.h"
+#include "storm/models/symbolic/StochasticTwoPlayerGame.h"
 
-#include "src/utility/OsDetection.h"
+#include "storm/utility/OsDetection.h"
 
 namespace storm {
     namespace abstraction {
diff --git a/src/storm/abstraction/MenuGameAbstractor.h b/src/storm/abstraction/MenuGameAbstractor.h
index f144ce82b..ad836a318 100644
--- a/src/storm/abstraction/MenuGameAbstractor.h
+++ b/src/storm/abstraction/MenuGameAbstractor.h
@@ -1,8 +1,8 @@
 #pragma once
 
-#include "src/storage/dd/DdType.h"
+#include "storm/storage/dd/DdType.h"
 
-#include "src/abstraction/MenuGame.h"
+#include "storm/abstraction/MenuGame.h"
 
 namespace storm {
     namespace abstraction {
@@ -16,4 +16,4 @@ namespace storm {
         };
         
     }
-}
\ No newline at end of file
+}
diff --git a/src/storm/abstraction/StateSetAbstractor.cpp b/src/storm/abstraction/StateSetAbstractor.cpp
index 92c763e5c..0483635b6 100644
--- a/src/storm/abstraction/StateSetAbstractor.cpp
+++ b/src/storm/abstraction/StateSetAbstractor.cpp
@@ -1,14 +1,14 @@
-#include "src/abstraction/StateSetAbstractor.h"
+#include "storm/abstraction/StateSetAbstractor.h"
 
-#include "src/abstraction/AbstractionInformation.h"
+#include "storm/abstraction/AbstractionInformation.h"
 
-#include "src/storage/dd/DdManager.h"
+#include "storm/storage/dd/DdManager.h"
 
-#include "src/utility/macros.h"
-#include "src/utility/solver.h"
+#include "storm/utility/macros.h"
+#include "storm/utility/solver.h"
 
 #include "storm-config.h"
-#include "src/adapters/CarlAdapter.h"
+#include "storm/adapters/CarlAdapter.h"
 
 namespace storm {
     namespace abstraction {
diff --git a/src/storm/abstraction/StateSetAbstractor.h b/src/storm/abstraction/StateSetAbstractor.h
index 20950939c..8a3f500c5 100644
--- a/src/storm/abstraction/StateSetAbstractor.h
+++ b/src/storm/abstraction/StateSetAbstractor.h
@@ -4,14 +4,14 @@
 #include <set>
 #include <boost/optional.hpp>
 
-#include "src/utility/OsDetection.h"
+#include "storm/utility/OsDetection.h"
 
-#include "src/storage/dd/DdType.h"
+#include "storm/storage/dd/DdType.h"
 
-#include "src/utility/solver.h"
-#include "src/solver/SmtSolver.h"
+#include "storm/utility/solver.h"
+#include "storm/solver/SmtSolver.h"
 
-#include "src/abstraction/LocalExpressionInformation.h"
+#include "storm/abstraction/LocalExpressionInformation.h"
 
 namespace storm {
     namespace utility {
diff --git a/src/storm/abstraction/prism/AbstractCommand.cpp b/src/storm/abstraction/prism/AbstractCommand.cpp
index 70438d216..40c910cd0 100644
--- a/src/storm/abstraction/prism/AbstractCommand.cpp
+++ b/src/storm/abstraction/prism/AbstractCommand.cpp
@@ -1,21 +1,21 @@
-#include "src/abstraction/prism/AbstractCommand.h"
+#include "storm/abstraction/prism/AbstractCommand.h"
 
 #include <boost/iterator/transform_iterator.hpp>
 
-#include "src/abstraction/AbstractionInformation.h"
-#include "src/abstraction/BottomStateResult.h"
+#include "storm/abstraction/AbstractionInformation.h"
+#include "storm/abstraction/BottomStateResult.h"
 
-#include "src/storage/dd/DdManager.h"
-#include "src/storage/dd/Add.h"
+#include "storm/storage/dd/DdManager.h"
+#include "storm/storage/dd/Add.h"
 
-#include "src/storage/prism/Command.h"
-#include "src/storage/prism/Update.h"
+#include "storm/storage/prism/Command.h"
+#include "storm/storage/prism/Update.h"
 
-#include "src/utility/solver.h"
-#include "src/utility/macros.h"
+#include "storm/utility/solver.h"
+#include "storm/utility/macros.h"
 
 #include "storm-config.h"
-#include "src/adapters/CarlAdapter.h"
+#include "storm/adapters/CarlAdapter.h"
 
 namespace storm {
     namespace abstraction {
diff --git a/src/storm/abstraction/prism/AbstractCommand.h b/src/storm/abstraction/prism/AbstractCommand.h
index d8b1434d2..7446333e9 100644
--- a/src/storm/abstraction/prism/AbstractCommand.h
+++ b/src/storm/abstraction/prism/AbstractCommand.h
@@ -5,16 +5,16 @@
 #include <set>
 #include <map>
 
-#include "src/abstraction/LocalExpressionInformation.h"
-#include "src/abstraction/StateSetAbstractor.h"
-#include "src/abstraction/prism/GameBddResult.h"
+#include "storm/abstraction/LocalExpressionInformation.h"
+#include "storm/abstraction/StateSetAbstractor.h"
+#include "storm/abstraction/prism/GameBddResult.h"
 
-#include "src/storage/expressions/ExpressionEvaluator.h"
+#include "storm/storage/expressions/ExpressionEvaluator.h"
 
-#include "src/storage/dd/DdType.h"
-#include "src/storage/expressions/Expression.h"
+#include "storm/storage/dd/DdType.h"
+#include "storm/storage/expressions/Expression.h"
 
-#include "src/solver/SmtSolver.h"
+#include "storm/solver/SmtSolver.h"
 
 namespace storm {
     namespace utility {
@@ -60,7 +60,7 @@ namespace storm {
                  * @param guardIsPredicate A flag indicating whether the guard of the command was added as a predicate.
                  */
                 AbstractCommand(storm::prism::Command const& command, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool guardIsPredicate = false);
-                
+                               
                 /*!
                  * Refines the abstract command with the given predicates.
                  *
diff --git a/src/storm/abstraction/prism/AbstractModule.cpp b/src/storm/abstraction/prism/AbstractModule.cpp
index b9b001bd7..8630e28a3 100644
--- a/src/storm/abstraction/prism/AbstractModule.cpp
+++ b/src/storm/abstraction/prism/AbstractModule.cpp
@@ -1,18 +1,18 @@
-#include "src/abstraction/prism/AbstractModule.h"
+#include "storm/abstraction/prism/AbstractModule.h"
 
-#include "src/abstraction/AbstractionInformation.h"
-#include "src/abstraction/BottomStateResult.h"
-#include "src/abstraction/prism/GameBddResult.h"
+#include "storm/abstraction/AbstractionInformation.h"
+#include "storm/abstraction/BottomStateResult.h"
+#include "storm/abstraction/prism/GameBddResult.h"
 
-#include "src/storage/dd/DdManager.h"
-#include "src/storage/dd/Add.h"
+#include "storm/storage/dd/DdManager.h"
+#include "storm/storage/dd/Add.h"
 
-#include "src/storage/prism/Module.h"
+#include "storm/storage/prism/Module.h"
 
 #include "storm-config.h"
-#include "src/adapters/CarlAdapter.h"
+#include "storm/adapters/CarlAdapter.h"
 
-#include "src/utility/macros.h"
+#include "storm/utility/macros.h"
 
 namespace storm {
     namespace abstraction {
diff --git a/src/storm/abstraction/prism/AbstractModule.h b/src/storm/abstraction/prism/AbstractModule.h
index bc885194c..b507a39e5 100644
--- a/src/storm/abstraction/prism/AbstractModule.h
+++ b/src/storm/abstraction/prism/AbstractModule.h
@@ -1,12 +1,12 @@
 #pragma once
 
-#include "src/storage/dd/DdType.h"
+#include "storm/storage/dd/DdType.h"
 
-#include "src/abstraction/prism/AbstractCommand.h"
+#include "storm/abstraction/prism/AbstractCommand.h"
 
-#include "src/storage/expressions/Expression.h"
+#include "storm/storage/expressions/Expression.h"
 
-#include "src/utility/solver.h"
+#include "storm/utility/solver.h"
 
 namespace storm {
     namespace prism {
diff --git a/src/storm/abstraction/prism/AbstractProgram.cpp b/src/storm/abstraction/prism/AbstractProgram.cpp
index 2cd938941..849285757 100644
--- a/src/storm/abstraction/prism/AbstractProgram.cpp
+++ b/src/storm/abstraction/prism/AbstractProgram.cpp
@@ -1,24 +1,24 @@
-#include "src/abstraction/prism/AbstractProgram.h"
+#include "storm/abstraction/prism/AbstractProgram.h"
 
-#include "src/abstraction/BottomStateResult.h"
+#include "storm/abstraction/BottomStateResult.h"
 
-#include "src/storage/BitVector.h"
+#include "storm/storage/BitVector.h"
 
-#include "src/storage/prism/Program.h"
+#include "storm/storage/prism/Program.h"
 
-#include "src/storage/dd/DdManager.h"
-#include "src/storage/dd/Add.h"
+#include "storm/storage/dd/DdManager.h"
+#include "storm/storage/dd/Add.h"
 
-#include "src/models/symbolic/StandardRewardModel.h"
+#include "storm/models/symbolic/StandardRewardModel.h"
 
-#include "src/utility/dd.h"
-#include "src/utility/macros.h"
-#include "src/utility/solver.h"
-#include "src/exceptions/WrongFormatException.h"
-#include "src/exceptions/InvalidArgumentException.h"
+#include "storm/utility/dd.h"
+#include "storm/utility/macros.h"
+#include "storm/utility/solver.h"
+#include "storm/exceptions/WrongFormatException.h"
+#include "storm/exceptions/InvalidArgumentException.h"
 
 #include "storm-config.h"
-#include "src/adapters/CarlAdapter.h"
+#include "storm/adapters/CarlAdapter.h"
 
 //#define LOCAL_DEBUG
 
diff --git a/src/storm/abstraction/prism/AbstractProgram.h b/src/storm/abstraction/prism/AbstractProgram.h
index 47c67ac8e..f37c28327 100644
--- a/src/storm/abstraction/prism/AbstractProgram.h
+++ b/src/storm/abstraction/prism/AbstractProgram.h
@@ -1,14 +1,14 @@
 #pragma once
 
-#include "src/storage/dd/DdType.h"
+#include "storm/storage/dd/DdType.h"
 
-#include "src/abstraction/AbstractionInformation.h"
-#include "src/abstraction/MenuGame.h"
-#include "src/abstraction/prism/AbstractModule.h"
+#include "storm/abstraction/AbstractionInformation.h"
+#include "storm/abstraction/MenuGame.h"
+#include "storm/abstraction/prism/AbstractModule.h"
 
-#include "src/storage/dd/Add.h"
+#include "storm/storage/dd/Add.h"
 
-#include "src/storage/expressions/Expression.h"
+#include "storm/storage/expressions/Expression.h"
 
 namespace storm {
     namespace utility {
diff --git a/src/storm/abstraction/prism/GameBddResult.cpp b/src/storm/abstraction/prism/GameBddResult.cpp
index 2e7df1f5e..d2dd31a57 100644
--- a/src/storm/abstraction/prism/GameBddResult.cpp
+++ b/src/storm/abstraction/prism/GameBddResult.cpp
@@ -1,4 +1,4 @@
-#include "src/abstraction/prism/GameBddResult.h"
+#include "storm/abstraction/prism/GameBddResult.h"
 
 namespace storm {
     namespace abstraction {
@@ -18,4 +18,4 @@ namespace storm {
             template class GameBddResult<storm::dd::DdType::Sylvan>;
         }
     }
-}
\ No newline at end of file
+}
diff --git a/src/storm/abstraction/prism/GameBddResult.h b/src/storm/abstraction/prism/GameBddResult.h
index 02ad2f724..386549e46 100644
--- a/src/storm/abstraction/prism/GameBddResult.h
+++ b/src/storm/abstraction/prism/GameBddResult.h
@@ -1,6 +1,6 @@
 #pragma once
 
-#include "src/storage/dd/Bdd.h"
+#include "storm/storage/dd/Bdd.h"
 
 namespace storm {
     namespace abstraction {
@@ -17,4 +17,4 @@ namespace storm {
             
         }
     }
-}
\ No newline at end of file
+}
diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp
index ad8c22e78..b1c5eee1e 100644
--- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp
+++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp
@@ -1,9 +1,9 @@
-#include "src/abstraction/prism/PrismMenuGameAbstractor.h"
+#include "storm/abstraction/prism/PrismMenuGameAbstractor.h"
 
-#include "src/models/symbolic/StandardRewardModel.h"
+#include "storm/models/symbolic/StandardRewardModel.h"
 
-#include "src/settings/SettingsManager.h"
-#include "src/settings/modules/AbstractionSettings.h"
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/AbstractionSettings.h"
 
 namespace storm {
     namespace abstraction {
diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h
index 6aa450ff8..a99c202ac 100644
--- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h
+++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h
@@ -1,8 +1,8 @@
 #pragma once
 
-#include "src/abstraction/MenuGameAbstractor.h"
+#include "storm/abstraction/MenuGameAbstractor.h"
 
-#include "src/abstraction/prism/AbstractProgram.h"
+#include "storm/abstraction/prism/AbstractProgram.h"
 
 namespace storm {
     namespace abstraction {
diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp
index 22437f2ed..82b1fe639 100644
--- a/src/storm/builder/DdJaniModelBuilder.cpp
+++ b/src/storm/builder/DdJaniModelBuilder.cpp
@@ -126,12 +126,7 @@ namespace storm {
         bool DdJaniModelBuilder<Type, ValueType>::Options::isBuildAllLabelsSet() const {
             return buildAllLabels;
         }
-        
-        template <storm::dd::DdType Type, typename ValueType>
-        std::set<std::string> const& DdJaniModelBuilder<Type, ValueType>::Options::getRewardModelNames() const {
-            return rewardModelsToBuild;
-        }
-        
+                
         template <storm::dd::DdType Type, typename ValueType>
         void DdJaniModelBuilder<Type, ValueType>::Options::addLabel(std::string const& labelName) {
             STORM_LOG_THROW(!buildAllLabels, storm::exceptions::InvalidSettingsException, "Cannot add label, because all labels are built anyway.");
diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp
index 0142a95bb..4f1ad61c3 100644
--- a/src/storm/cli/cli.cpp
+++ b/src/storm/cli/cli.cpp
@@ -12,6 +12,7 @@
 #include "storm/settings/modules/ResourceSettings.h"
 #include "storm/settings/modules/JaniExportSettings.h"
 
+#include "storm/utility/resources.h"
 #include "storm/utility/storm-version.h"
 #include "storm/storage/jani/JSONExporter.h"
 
diff --git a/src/storm/cli/entrypoints.h b/src/storm/cli/entrypoints.h
index dd47795dc..26c6f77ac 100644
--- a/src/storm/cli/entrypoints.h
+++ b/src/storm/cli/entrypoints.h
@@ -112,11 +112,14 @@ namespace storm {
 #endif
 
         template<storm::dd::DdType DdType>
-        void verifySymbolicModelWithAbstractionRefinementEngine(storm::prism::Program const& program, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas, bool onlyInitialStatesRelevant = false) {
+        void verifySymbolicModelWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const& model, std::vector<storm::jani::Property> const& properties, bool onlyInitialStatesRelevant = false) {
+            STORM_LOG_THROW(model.isPrismProgram(), storm::exceptions::NotImplementedException, "Abstraction-refinement is currently only available for PRISM programs.");
+            storm::prism::Program const& program = model.asPrismProgram();
+            
             typedef double ValueType;
-            for (auto const& formula : formulas) {
-                std::cout << std::endl << "Model checking property: " << *formula << " ...";
-                std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifyProgramWithAbstractionRefinementEngine<DdType, ValueType>(program, formula, onlyInitialStatesRelevant));
+            for (auto const& property : properties) {
+                std::cout << std::endl << "Model checking property: " << property << " ...";
+                std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifyProgramWithAbstractionRefinementEngine<DdType, ValueType>(program, property.getFilter().getFormula(), onlyInitialStatesRelevant));
                 if (result) {
                     std::cout << " done." << std::endl;
                     std::cout << "Result (initial states): ";
diff --git a/src/storm/exceptions/InvalidModelException.h b/src/storm/exceptions/InvalidModelException.h
index 3d8b8b7c4..fd6aaa444 100644
--- a/src/storm/exceptions/InvalidModelException.h
+++ b/src/storm/exceptions/InvalidModelException.h
@@ -1,7 +1,7 @@
 #pragma once
 
-#include "src/exceptions/BaseException.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "storm/exceptions/BaseException.h"
+#include "storm/exceptions/ExceptionMacros.h"
 
 namespace storm {
     namespace exceptions {
diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
index c8fd9e3bb..05a24ebe9 100644
--- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
+++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
@@ -1,32 +1,32 @@
-#include "src/modelchecker/abstraction/GameBasedMdpModelChecker.h"
+#include "storm/modelchecker/abstraction/GameBasedMdpModelChecker.h"
 
-#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
-#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
+#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
+#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
 
-#include "src/models/symbolic/StandardRewardModel.h"
-#include "src/models/symbolic/Dtmc.h"
-#include "src/models/symbolic/Mdp.h"
+#include "storm/models/symbolic/StandardRewardModel.h"
+#include "storm/models/symbolic/Dtmc.h"
+#include "storm/models/symbolic/Mdp.h"
 
-#include "src/storage/expressions/ExpressionManager.h"
+#include "storm/storage/expressions/ExpressionManager.h"
 
-#include "src/storage/dd/DdManager.h"
+#include "storm/storage/dd/DdManager.h"
 
-#include "src/abstraction/prism/PrismMenuGameAbstractor.h"
+#include "storm/abstraction/prism/PrismMenuGameAbstractor.h"
 
-#include "src/logic/FragmentSpecification.h"
+#include "storm/logic/FragmentSpecification.h"
 
-#include "src/solver/SymbolicGameSolver.h"
+#include "storm/solver/SymbolicGameSolver.h"
 
-#include "src/utility/solver.h"
-#include "src/utility/dd.h"
-#include "src/utility/prism.h"
-#include "src/utility/macros.h"
+#include "storm/utility/solver.h"
+#include "storm/utility/dd.h"
+#include "storm/utility/prism.h"
+#include "storm/utility/macros.h"
 
-#include "src/exceptions/NotSupportedException.h"
-#include "src/exceptions/InvalidPropertyException.h"
-#include "src/exceptions/InvalidModelException.h"
+#include "storm/exceptions/NotSupportedException.h"
+#include "storm/exceptions/InvalidPropertyException.h"
+#include "storm/exceptions/InvalidModelException.h"
 
-#include "src/modelchecker/results/CheckResult.h"
+#include "storm/modelchecker/results/CheckResult.h"
 
 //#define LOCAL_DEBUG
 
diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h
index c83dc9dba..3323d55a4 100644
--- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h
+++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h
@@ -1,14 +1,14 @@
 #ifndef STORM_MODELCHECKER_GAMEBASEDMDPMODELCHECKER_H_
 #define STORM_MODELCHECKER_GAMEBASEDMDPMODELCHECKER_H_
 
-#include "src/modelchecker/AbstractModelChecker.h"
+#include "storm/modelchecker/AbstractModelChecker.h"
 
-#include "src/storage/prism/Program.h"
+#include "storm/storage/prism/Program.h"
 
-#include "src/storage/dd/DdType.h"
+#include "storm/storage/dd/DdType.h"
 
-#include "src/utility/solver.h"
-#include "src/utility/graph.h"
+#include "storm/utility/solver.h"
+#include "storm/utility/graph.h"
 
 namespace storm {
     namespace abstraction {
@@ -70,4 +70,4 @@ namespace storm {
     }
 }
 
-#endif /* STORM_MODELCHECKER_GAMEBASEDMDPMODELCHECKER_H_ */
\ No newline at end of file
+#endif /* STORM_MODELCHECKER_GAMEBASEDMDPMODELCHECKER_H_ */
diff --git a/src/storm/models/symbolic/Model.cpp b/src/storm/models/symbolic/Model.cpp
index 7f1b8bd44..29f1d6ec7 100644
--- a/src/storm/models/symbolic/Model.cpp
+++ b/src/storm/models/symbolic/Model.cpp
@@ -14,7 +14,7 @@
 #include "storm/models/symbolic/StandardRewardModel.h"
 
 #include "storm-config.h"
-#include "src/adapters/CarlAdapter.h"
+#include "storm/adapters/CarlAdapter.h"
 
 namespace storm {
     namespace models {
diff --git a/src/storm/models/symbolic/NondeterministicModel.cpp b/src/storm/models/symbolic/NondeterministicModel.cpp
index 808dc42e7..dc6ffc07c 100644
--- a/src/storm/models/symbolic/NondeterministicModel.cpp
+++ b/src/storm/models/symbolic/NondeterministicModel.cpp
@@ -7,7 +7,7 @@
 #include "storm/models/symbolic/StandardRewardModel.h"
 
 #include "storm-config.h"
-#include "src/adapters/CarlAdapter.h"
+#include "storm/adapters/CarlAdapter.h"
 
 namespace storm {
     namespace models {
diff --git a/src/storm/models/symbolic/StochasticTwoPlayerGame.cpp b/src/storm/models/symbolic/StochasticTwoPlayerGame.cpp
index 9b853c41d..b48a263ca 100644
--- a/src/storm/models/symbolic/StochasticTwoPlayerGame.cpp
+++ b/src/storm/models/symbolic/StochasticTwoPlayerGame.cpp
@@ -7,7 +7,7 @@
 #include "storm/models/symbolic/StandardRewardModel.h"
 
 #include "storm-config.h"
-#include "src/adapters/CarlAdapter.h"
+#include "storm/adapters/CarlAdapter.h"
 
 namespace storm {
     namespace models {
diff --git a/src/storm/settings/modules/AbstractionSettings.cpp b/src/storm/settings/modules/AbstractionSettings.cpp
index 06aec79ee..ff573bdd9 100644
--- a/src/storm/settings/modules/AbstractionSettings.cpp
+++ b/src/storm/settings/modules/AbstractionSettings.cpp
@@ -1,7 +1,7 @@
-#include "src/settings/modules/AbstractionSettings.h"
+#include "storm/settings/modules/AbstractionSettings.h"
 
-#include "src/settings/Option.h"
-#include "src/settings/OptionBuilder.h"
+#include "storm/settings/Option.h"
+#include "storm/settings/OptionBuilder.h"
 
 namespace storm {
     namespace settings {
@@ -20,4 +20,4 @@ namespace storm {
             
         }
     }
-}
\ No newline at end of file
+}
diff --git a/src/storm/settings/modules/AbstractionSettings.h b/src/storm/settings/modules/AbstractionSettings.h
index 44a504171..f09bf5694 100644
--- a/src/storm/settings/modules/AbstractionSettings.h
+++ b/src/storm/settings/modules/AbstractionSettings.h
@@ -1,6 +1,6 @@
 #pragma once
 
-#include "src/settings/modules/ModuleSettings.h"
+#include "storm/settings/modules/ModuleSettings.h"
 
 namespace storm {
     namespace settings {
@@ -31,4 +31,4 @@ namespace storm {
             
         }
     }
-}
\ No newline at end of file
+}
diff --git a/src/storm/settings/modules/ResourceSettings.cpp b/src/storm/settings/modules/ResourceSettings.cpp
index a38c99bb7..d79d7eac8 100644
--- a/src/storm/settings/modules/ResourceSettings.cpp
+++ b/src/storm/settings/modules/ResourceSettings.cpp
@@ -1,10 +1,10 @@
-#include "src/settings/modules/ResourceSettings.h"
+#include "storm/settings/modules/ResourceSettings.h"
 
-#include "src/settings/SettingsManager.h"
-#include "src/settings/Option.h"
-#include "src/settings/OptionBuilder.h"
-#include "src/settings/ArgumentBuilder.h"
-#include "src/settings/Argument.h"
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/Option.h"
+#include "storm/settings/OptionBuilder.h"
+#include "storm/settings/ArgumentBuilder.h"
+#include "storm/settings/Argument.h"
 
 namespace storm {
     namespace settings {
@@ -29,4 +29,4 @@ namespace storm {
             
         }
     }
-}
\ No newline at end of file
+}
diff --git a/src/storm/settings/modules/ResourceSettings.h b/src/storm/settings/modules/ResourceSettings.h
index 8c76346ed..9abd5cc0d 100644
--- a/src/storm/settings/modules/ResourceSettings.h
+++ b/src/storm/settings/modules/ResourceSettings.h
@@ -1,7 +1,7 @@
 #pragma once
 
 #include "storm-config.h"
-#include "src/settings/modules/ModuleSettings.h"
+#include "storm/settings/modules/ModuleSettings.h"
 
 namespace storm {
     namespace settings {
diff --git a/src/storm/solver/SymbolicGameSolver.cpp b/src/storm/solver/SymbolicGameSolver.cpp
index 616d0c9bc..8924f1415 100644
--- a/src/storm/solver/SymbolicGameSolver.cpp
+++ b/src/storm/solver/SymbolicGameSolver.cpp
@@ -7,9 +7,9 @@
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/NativeEquationSolverSettings.h"
 
-#include "src/utility/constants.h"
-#include "src/utility/macros.h"
-#include "src/exceptions/IllegalFunctionCallException.h"
+#include "storm/utility/constants.h"
+#include "storm/utility/macros.h"
+#include "storm/exceptions/IllegalFunctionCallException.h"
 
 namespace storm {
     namespace solver {
diff --git a/src/storm/storage/dd/Add.cpp b/src/storm/storage/dd/Add.cpp
index 9e2c93f5c..748729907 100644
--- a/src/storm/storage/dd/Add.cpp
+++ b/src/storm/storage/dd/Add.cpp
@@ -13,7 +13,7 @@
 #include "storm/exceptions/InvalidArgumentException.h"
 
 #include "storm-config.h"
-#include "src/adapters/CarlAdapter.h"
+#include "storm/adapters/CarlAdapter.h"
 
 namespace storm {
     namespace dd {
diff --git a/src/storm/storage/dd/Bdd.cpp b/src/storm/storage/dd/Bdd.cpp
index 836d7dbad..b1a83d226 100644
--- a/src/storm/storage/dd/Bdd.cpp
+++ b/src/storm/storage/dd/Bdd.cpp
@@ -16,7 +16,7 @@
 #include "storm/exceptions/InvalidArgumentException.h"
 
 #include "storm-config.h"
-#include "src/adapters/CarlAdapter.h"
+#include "storm/adapters/CarlAdapter.h"
 
 namespace storm {
     namespace dd {
diff --git a/src/storm/storage/dd/MetaVariablePosition.h b/src/storm/storage/dd/MetaVariablePosition.h
index 5fb9724f2..5ce0e2571 100644
--- a/src/storm/storage/dd/MetaVariablePosition.h
+++ b/src/storm/storage/dd/MetaVariablePosition.h
@@ -1,7 +1,7 @@
 #ifndef STORM_STORAGE_DD_METAVARIABLEPOSITION_H_
 #define STORM_STORAGE_DD_METAVARIABLEPOSITION_H_
 
-#include "src/storage/dd/DdType.h"
+#include "storm/storage/dd/DdType.h"
 
 namespace storm {
     namespace dd {
diff --git a/src/storm/storage/dd/cudd/InternalCuddBdd.cpp b/src/storm/storage/dd/cudd/InternalCuddBdd.cpp
index f6e9c332f..5ad9b5846 100644
--- a/src/storm/storage/dd/cudd/InternalCuddBdd.cpp
+++ b/src/storm/storage/dd/cudd/InternalCuddBdd.cpp
@@ -8,7 +8,7 @@
 #include "storm/storage/BitVector.h"
 #include "storm/storage/PairHash.h"
 
-#include "src/utility/macros.h"
+#include "storm/utility/macros.h"
 
 namespace storm {
     namespace dd {
diff --git a/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp b/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp
index eadb71933..de2e641ed 100644
--- a/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp
+++ b/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp
@@ -10,7 +10,7 @@
 #include "storm/utility/macros.h"
 #include "storm/exceptions/NotSupportedException.h"
 
-#include "src/utility/sylvan.h"
+#include "storm/utility/sylvan.h"
 
 #include "storm-config.h"
 
diff --git a/src/storm/storage/dd/sylvan/SylvanAddIterator.cpp b/src/storm/storage/dd/sylvan/SylvanAddIterator.cpp
index 9cba2f10f..169b8922c 100644
--- a/src/storm/storage/dd/sylvan/SylvanAddIterator.cpp
+++ b/src/storm/storage/dd/sylvan/SylvanAddIterator.cpp
@@ -10,7 +10,7 @@
 
 #include <cmath>
 
-#include "src/adapters/CarlAdapter.h"
+#include "storm/adapters/CarlAdapter.h"
 #include "storm-config.h"
 
 namespace storm {
diff --git a/src/storm/storage/expressions/ExprtkExpressionEvaluator.cpp b/src/storm/storage/expressions/ExprtkExpressionEvaluator.cpp
index da4b86ef2..7cd49114d 100755
--- a/src/storm/storage/expressions/ExprtkExpressionEvaluator.cpp
+++ b/src/storm/storage/expressions/ExprtkExpressionEvaluator.cpp
@@ -48,9 +48,9 @@ namespace storm {
         typename ExprtkExpressionEvaluatorBase<RationalType>::CompiledExpressionType& ExprtkExpressionEvaluatorBase<RationalType>::getCompiledExpression(storm::expressions::Expression const& expression) const {
             std::pair<CacheType::iterator, bool> result = this->compiledExpressions.emplace(expression.getBaseExpressionPointer(), CompiledExpressionType());
             CompiledExpressionType& compiledExpression = result.first->second;
-            compiledExpression.register_symbol_table(symbolTable);
-            bool parsingOk = parser.compile(ToExprtkStringVisitor().toString(expression), compiledExpression);
-            STORM_LOG_THROW(parsingOk, storm::exceptions::UnexpectedException, "Expression was not properly parsed by ExprTk: " << expression << ". (Returned error: " << parser.error() << ")");
+            compiledExpression.register_symbol_table(*symbolTable);
+            bool parsingOk = parser->compile(ToExprtkStringVisitor().toString(expression), compiledExpression);
+            STORM_LOG_THROW(parsingOk, storm::exceptions::UnexpectedException, "Expression was not properly parsed by ExprTk: " << expression << ". (Returned error: " << parser->error() << ")");
             return compiledExpression;
         }
         
diff --git a/src/storm/storage/geometry/Polytope.h b/src/storm/storage/geometry/Polytope.h
index 96a446c0b..d9230b38e 100644
--- a/src/storm/storage/geometry/Polytope.h
+++ b/src/storm/storage/geometry/Polytope.h
@@ -129,12 +129,11 @@ namespace storm {
                 std::shared_ptr<Polytope<TargetType>> convertNumberRepresentation() const;
                 
                 /*
-                 * Returns a string repre/Users/tim/storm/src/storage/geometry/Polytope.h:129:17: 'virtual' cannot be specified on member function templatessentation of this polytope.
-                 * If the given flag is true, the occurring numbers are converted to double before printing to increase readability
+                 * Returns a string representation of this polytope.
+                 * @param numbersAsDouble If true, the occurring numbers are converted to double before printing to increase readability.
                  */
                 virtual std::string toString(bool numbersAsDouble = false) const;
                
-                
                 virtual bool isHyproPolytope() const;
                 
             protected:
diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp
index fdc2ca17d..148f666a4 100644
--- a/src/storm/storage/prism/Program.cpp
+++ b/src/storm/storage/prism/Program.cpp
@@ -23,6 +23,8 @@
 #include "storm/storage/prism/Compositions.h"
 #include "storm/storage/prism/ToJaniConverter.h"
 
+#include "storm/utility/macros.h"
+
 namespace storm {
     namespace prism {
         class CompositionValidityChecker : public CompositionVisitor {
@@ -1618,15 +1620,6 @@ namespace storm {
             return Command(newCommandIndex, false, actionIndex, actionName, newGuard, newUpdates, this->getFilename(), 0);
         }
         
-        uint_fast64_t Program::numberOfActions() const {
-            return this->actions.size();
-        }
-        
-        uint_fast64_t Program::largestActionIndex() const {
-            STORM_LOG_ASSERT(numberOfActions() != 0);
-            return this->indexToActionMap.rbegin()->first;
-        }
-        
         storm::jani::Model Program::toJani(bool allVariablesGlobal) const {
             ToJaniConverter converter;
             return converter.convert(*this, allVariablesGlobal);
diff --git a/src/storm/storage/prism/Program.h b/src/storm/storage/prism/Program.h
index 078431f02..a33484833 100644
--- a/src/storm/storage/prism/Program.h
+++ b/src/storm/storage/prism/Program.h
@@ -575,7 +575,7 @@ namespace storm {
              * @return The manager responsible for the expressions of this program.
              */
             storm::expressions::ExpressionManager& getManager() const;
-
+            
             std::unordered_map<uint_fast64_t, std::string> buildCommandIndexToActionNameMap() const;
 
             std::unordered_map<uint_fast64_t, uint_fast64_t> buildCommandIndexToActionIndex() const;
diff --git a/src/storm/utility/graph.h b/src/storm/utility/graph.h
index 7b1251f6b..a10fe8269 100644
--- a/src/storm/utility/graph.h
+++ b/src/storm/utility/graph.h
@@ -12,7 +12,7 @@
 #include "storm/models/sparse/DeterministicModel.h"
 #include "storm/storage/dd/DdType.h"
 
-#include "src/solver/OptimizationDirection.h"
+#include "storm/solver/OptimizationDirection.h"
 
 namespace storm {
     namespace storage {
diff --git a/src/utility/resources.h b/src/storm/utility/resources.h
similarity index 96%
rename from src/utility/resources.h
rename to src/storm/utility/resources.h
index 4dfc4a4d5..e843882ee 100644
--- a/src/utility/resources.h
+++ b/src/storm/utility/resources.h
@@ -9,9 +9,9 @@
 
 #include "storm-config.h"
 
-#include "src/utility/OsDetection.h"
+#include "storm/utility/OsDetection.h"
 
-#include "src/utility/macros.h"
+#include "storm/utility/macros.h"
 
 namespace storm {
     namespace utility {
@@ -92,4 +92,4 @@ namespace storm {
     }
 }
 
-#endif /* STORM_UTILITY_RESOURCES_H_ */
\ No newline at end of file
+#endif /* STORM_UTILITY_RESOURCES_H_ */
diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt
index eab0399c1..b3b5b5a1f 100644
--- a/src/test/CMakeLists.txt
+++ b/src/test/CMakeLists.txt
@@ -8,9 +8,9 @@ register_source_groups_from_filestructure("${ALL_FILES}" test)
 include_directories(${GTEST_INCLUDE_DIR})
 
 
-foreach (testsuite adapter builder logic modelchecker parser permissiveschedulers solver storage transformer utility)
+foreach (testsuite abstraction adapter builder logic modelchecker parser permissiveschedulers solver storage transformer utility)
 
-	  file(GLOB_RECURSE TEST_${testsuite}_FILES ${STORM_CPP_TESTS_BASE_PATH}/${testsuite}/*.h ${STORM_CPP_TESTS_BASE_PATH}/${testsuite}/*.cpp)
+file(GLOB_RECURSE TEST_${testsuite}_FILES ${STORM_CPP_TESTS_BASE_PATH}/${testsuite}/*.h ${STORM_CPP_TESTS_BASE_PATH}/${testsuite}/*.cpp)
       add_executable (test-${testsuite} ${TEST_${testsuite}_FILES} ${PROJECT_SOURCE_DIR}/src/test/storm-test.cpp)
 	  target_link_libraries(test-${testsuite} storm)
 	  target_link_libraries(test-${testsuite} ${STORM_TEST_LINK_LIBRARIES})
@@ -19,11 +19,3 @@ foreach (testsuite adapter builder logic modelchecker parser permissivescheduler
 	  add_test(run-test-${testsuite} test-${testsuite})
 	
 endforeach ()
-
-
-
-#INSTALL(TARGETS storm-functional-tests
-#	RUNTIME DESTINATION bin
-#	LIBRARY DESTINATION lib
-#	ARCHIVE DESTINATION lib
-#)
diff --git a/test/functional/abstraction/PrismMenuGameTest.cpp b/src/test/abstraction/PrismMenuGameTest.cpp
similarity index 96%
rename from test/functional/abstraction/PrismMenuGameTest.cpp
rename to src/test/abstraction/PrismMenuGameTest.cpp
index 92c581ecf..7ac1a19a7 100644
--- a/test/functional/abstraction/PrismMenuGameTest.cpp
+++ b/src/test/abstraction/PrismMenuGameTest.cpp
@@ -3,23 +3,23 @@
 
 #ifdef STORM_HAVE_MSAT
 
-#include "src/parser/PrismParser.h"
+#include "storm/parser/PrismParser.h"
 
-#include "src/abstraction/prism/AbstractProgram.h"
+#include "storm/abstraction/prism/AbstractProgram.h"
 
-#include "src/storage/expressions/Expression.h"
+#include "storm/storage/expressions/Expression.h"
 
-#include "src/storage/dd/Add.h"
-#include "src/storage/dd/Bdd.h"
+#include "storm/storage/dd/Add.h"
+#include "storm/storage/dd/Bdd.h"
 
-#include "src/models/symbolic/StandardRewardModel.h"
+#include "storm/models/symbolic/StandardRewardModel.h"
 
-#include "src/utility/solver.h"
+#include "storm/utility/solver.h"
 
-#include "src/adapters/CarlAdapter.h"
+#include "storm/adapters/CarlAdapter.h"
 
 TEST(PrismMenuGame, DieAbstractionTest_Cudd) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/die.pm");
 
     std::vector<storm::expressions::Expression> initialPredicates;
     storm::expressions::ExpressionManager& manager = program.getManager();
@@ -36,7 +36,7 @@ TEST(PrismMenuGame, DieAbstractionTest_Cudd) {
 }
 
 TEST(PrismMenuGame, DieAbstractionTest_Sylvan) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/die.pm");
     
     std::vector<storm::expressions::Expression> initialPredicates;
     storm::expressions::ExpressionManager& manager = program.getManager();
@@ -54,7 +54,7 @@ TEST(PrismMenuGame, DieAbstractionTest_Sylvan) {
 
 #ifdef STORM_HAVE_CARL
 TEST(PrismMenuGame, DieAbstractionTest_SylvanWithRationalFunction) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/die.pm");
     
     std::vector<storm::expressions::Expression> initialPredicates;
     storm::expressions::ExpressionManager& manager = program.getManager();
@@ -72,7 +72,7 @@ TEST(PrismMenuGame, DieAbstractionTest_SylvanWithRationalFunction) {
 #endif
 
 TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Cudd) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/die.pm");
     
     std::vector<storm::expressions::Expression> initialPredicates;
     storm::expressions::ExpressionManager& manager = program.getManager();
@@ -91,7 +91,7 @@ TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Cudd) {
 }
 
 TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Sylvan) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/die.pm");
     
     std::vector<storm::expressions::Expression> initialPredicates;
     storm::expressions::ExpressionManager& manager = program.getManager();
@@ -110,7 +110,7 @@ TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Sylvan) {
 }
 
 TEST(PrismMenuGame, DieFullAbstractionTest_Cudd) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/die.pm");
     
     std::vector<storm::expressions::Expression> initialPredicates;
     storm::expressions::ExpressionManager& manager = program.getManager();
@@ -142,7 +142,7 @@ TEST(PrismMenuGame, DieFullAbstractionTest_Cudd) {
 }
 
 TEST(PrismMenuGame, DieFullAbstractionTest_Sylvan) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/die.pm");
     
     std::vector<storm::expressions::Expression> initialPredicates;
     storm::expressions::ExpressionManager& manager = program.getManager();
@@ -174,7 +174,7 @@ TEST(PrismMenuGame, DieFullAbstractionTest_Sylvan) {
 }
 
 TEST(PrismMenuGame, CrowdsAbstractionTest_Cudd) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/crowds-5-5.pm");
     program = program.substituteConstants();
     
     std::vector<storm::expressions::Expression> initialPredicates;
@@ -192,7 +192,7 @@ TEST(PrismMenuGame, CrowdsAbstractionTest_Cudd) {
 }
 
 TEST(PrismMenuGame, CrowdsAbstractionTest_Sylvan) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/crowds-5-5.pm");
     program = program.substituteConstants();
     
     std::vector<storm::expressions::Expression> initialPredicates;
@@ -210,7 +210,7 @@ TEST(PrismMenuGame, CrowdsAbstractionTest_Sylvan) {
 }
 
 TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Cudd) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/crowds-5-5.pm");
     program = program.substituteConstants();
     
     std::vector<storm::expressions::Expression> initialPredicates;
@@ -230,7 +230,7 @@ TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Cudd) {
 }
 
 TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Sylvan) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/crowds-5-5.pm");
     program = program.substituteConstants();
     
     std::vector<storm::expressions::Expression> initialPredicates;
@@ -250,7 +250,7 @@ TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Sylvan) {
 }
 
 TEST(PrismMenuGame, CrowdsFullAbstractionTest_Cudd) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/crowds-5-5.pm");
     program = program.substituteConstants();
     
     std::vector<storm::expressions::Expression> initialPredicates;
@@ -322,7 +322,7 @@ TEST(PrismMenuGame, CrowdsFullAbstractionTest_Cudd) {
 }
 
 TEST(PrismMenuGame, CrowdsFullAbstractionTest_Sylvan) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/crowds-5-5.pm");
     program = program.substituteConstants();
     
     std::vector<storm::expressions::Expression> initialPredicates;
@@ -394,7 +394,7 @@ TEST(PrismMenuGame, CrowdsFullAbstractionTest_Sylvan) {
 }
 
 TEST(PrismMenuGame, TwoDiceAbstractionTest_Cudd) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/two_dice.nm");
     program = program.substituteConstants();
     program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
     
@@ -414,7 +414,7 @@ TEST(PrismMenuGame, TwoDiceAbstractionTest_Cudd) {
 }
 
 TEST(PrismMenuGame, TwoDiceAbstractionTest_Sylvan) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/two_dice.nm");
     program = program.substituteConstants();
     program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
     
@@ -434,7 +434,7 @@ TEST(PrismMenuGame, TwoDiceAbstractionTest_Sylvan) {
 }
 
 TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Cudd) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/two_dice.nm");
     program = program.substituteConstants();
     program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
     
@@ -456,7 +456,7 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Cudd) {
 }
 
 TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Sylvan) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/two_dice.nm");
     program = program.substituteConstants();
     program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
     
@@ -478,7 +478,7 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Sylvan) {
 }
 
 TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Cudd) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/two_dice.nm");
     program = program.substituteConstants();
     program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
     
@@ -529,7 +529,7 @@ TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Cudd) {
 }
 
 TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Sylvan) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/two_dice.nm");
     program = program.substituteConstants();
     program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
     
@@ -580,7 +580,7 @@ TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Sylvan) {
 }
 
 TEST(PrismMenuGame, WlanAbstractionTest_Cudd) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-4.nm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/wlan0-2-4.nm");
     program = program.substituteConstants();
     program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
     
@@ -601,7 +601,7 @@ TEST(PrismMenuGame, WlanAbstractionTest_Cudd) {
 }
 
 TEST(PrismMenuGame, WlanAbstractionTest_Sylvan) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-4.nm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/wlan0-2-4.nm");
     program = program.substituteConstants();
     program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
     
@@ -622,7 +622,7 @@ TEST(PrismMenuGame, WlanAbstractionTest_Sylvan) {
 }
 
 TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Cudd) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-4.nm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/wlan0-2-4.nm");
     program = program.substituteConstants();
     program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
     
@@ -645,7 +645,7 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Cudd) {
 }
 
 TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Sylvan) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-4.nm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/wlan0-2-4.nm");
     program = program.substituteConstants();
     program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
     
@@ -668,7 +668,7 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Sylvan) {
 }
 
 TEST(PrismMenuGame, WlanFullAbstractionTest_Cudd) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-4.nm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/wlan0-2-4.nm");
     program = program.substituteConstants();
     program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
     
@@ -787,7 +787,7 @@ TEST(PrismMenuGame, WlanFullAbstractionTest_Cudd) {
 }
 
 TEST(PrismMenuGame, WlanFullAbstractionTest_Sylvan) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-4.nm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/wlan0-2-4.nm");
     program = program.substituteConstants();
     program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
     
diff --git a/test/functional/modelchecker/GameBasedDtmcModelCheckerTest.cpp b/src/test/modelchecker/GameBasedDtmcModelCheckerTest.cpp
similarity index 94%
rename from test/functional/modelchecker/GameBasedDtmcModelCheckerTest.cpp
rename to src/test/modelchecker/GameBasedDtmcModelCheckerTest.cpp
index 0485ef9f1..c7589eb3e 100644
--- a/test/functional/modelchecker/GameBasedDtmcModelCheckerTest.cpp
+++ b/src/test/modelchecker/GameBasedDtmcModelCheckerTest.cpp
@@ -1,24 +1,24 @@
 #include "gtest/gtest.h"
 #include "storm-config.h"
 
-#include "src/parser/FormulaParser.h"
-#include "src/logic/Formulas.h"
-#include "src/utility/solver.h"
-#include "src/modelchecker/abstraction/GameBasedMdpModelChecker.h"
-#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
-#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
-#include "src/parser/PrismParser.h"
-#include "src/builder/DdPrismModelBuilder.h"
-#include "src/models/symbolic/StandardRewardModel.h"
-#include "src/models/symbolic/Dtmc.h"
-#include "src/settings/SettingsManager.h"
+#include "storm/parser/FormulaParser.h"
+#include "storm/logic/Formulas.h"
+#include "storm/utility/solver.h"
+#include "storm/modelchecker/abstraction/GameBasedMdpModelChecker.h"
+#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
+#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
+#include "storm/parser/PrismParser.h"
+#include "storm/builder/DdPrismModelBuilder.h"
+#include "storm/models/symbolic/StandardRewardModel.h"
+#include "storm/models/symbolic/Dtmc.h"
+#include "storm/settings/SettingsManager.h"
 
-#include "src/settings/modules/NativeEquationSolverSettings.h"
+#include "storm/settings/modules/NativeEquationSolverSettings.h"
 
-#include "src/settings/modules/GeneralSettings.h"
+#include "storm/settings/modules/GeneralSettings.h"
 
 TEST(GameBasedDtmcModelCheckerTest, Die_Cudd) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/die.pm");
     
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
@@ -67,7 +67,7 @@ TEST(GameBasedDtmcModelCheckerTest, Die_Cudd) {
 }
 
 TEST(GameBasedDtmcModelCheckerTest, Die_Sylvan) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/die.pm");
     
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
@@ -116,7 +116,7 @@ TEST(GameBasedDtmcModelCheckerTest, Die_Sylvan) {
 }
 
 TEST(GameBasedDtmcModelCheckerTest, Crowds_Cudd) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/crowds-5-5.pm");
     
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
@@ -159,7 +159,7 @@ TEST(GameBasedDtmcModelCheckerTest, Crowds_Cudd) {
 }
 
 TEST(GameBasedDtmcModelCheckerTest, Crowds_Sylvan) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/crowds-5-5.pm");
     
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
@@ -205,7 +205,7 @@ TEST(GameBasedDtmcModelCheckerTest, Crowds_Sylvan) {
 }
 
 TEST(GameBasedDtmcModelCheckerTest, SynchronousLeader_Cudd) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/leader-3-5.pm");
     
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
@@ -245,7 +245,7 @@ TEST(GameBasedDtmcModelCheckerTest, SynchronousLeader_Cudd) {
 }
 
 TEST(GameBasedDtmcModelCheckerTest, SynchronousLeader_Sylvan) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/leader-3-5.pm");
     
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
diff --git a/test/functional/modelchecker/GameBasedMdpModelCheckerTest.cpp b/src/test/modelchecker/GameBasedMdpModelCheckerTest.cpp
similarity index 89%
rename from test/functional/modelchecker/GameBasedMdpModelCheckerTest.cpp
rename to src/test/modelchecker/GameBasedMdpModelCheckerTest.cpp
index ff07a208a..18eaff017 100644
--- a/test/functional/modelchecker/GameBasedMdpModelCheckerTest.cpp
+++ b/src/test/modelchecker/GameBasedMdpModelCheckerTest.cpp
@@ -1,24 +1,24 @@
 #include "gtest/gtest.h"
 #include "storm-config.h"
 
-#include "src/parser/FormulaParser.h"
-#include "src/logic/Formulas.h"
-#include "src/models/sparse/StandardRewardModel.h"
-#include "src/models/sparse/Model.h"
-#include "src/modelchecker/abstraction/GameBasedMdpModelChecker.h"
-#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
-#include "src/settings/SettingsManager.h"
-#include "src/settings/modules/GeneralSettings.h"
-#include "src/settings/modules/NativeEquationSolverSettings.h"
-
-#include "src/parser/AutoParser.h"
-#include "src/parser/PrismParser.h"
+#include "storm/parser/FormulaParser.h"
+#include "storm/logic/Formulas.h"
+#include "storm/models/sparse/StandardRewardModel.h"
+#include "storm/models/sparse/Model.h"
+#include "storm/modelchecker/abstraction/GameBasedMdpModelChecker.h"
+#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/GeneralSettings.h"
+#include "storm/settings/modules/NativeEquationSolverSettings.h"
+
+#include "storm/parser/AutoParser.h"
+#include "storm/parser/PrismParser.h"
 
 #include "utility/storm.h"
 
 TEST(GameBasedMdpModelCheckerTest, Dice_Cudd) {
-    std::string programFile = STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.nm";
-    std::string formulaFile = STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.prctl";
+    std::string programFile = STORM_CPP_BASE_PATH "/builder/two_dice.nm";
+    std::string formulaFile = STORM_CPP_BASE_PATH "/builder/two_dice.prctl";
 
     storm::prism::Program program = storm::parseProgram(programFile);
 	
@@ -89,8 +89,8 @@ TEST(GameBasedMdpModelCheckerTest, Dice_Cudd) {
 }
 
 TEST(GameBasedMdpModelCheckerTest, AsynchronousLeader_Cudd) {
-    std::string programFile = STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.nm";
-    std::string formulaFile = STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader.prctl";
+    std::string programFile = STORM_CPP_BASE_PATH "/builder/leader4.nm";
+    std::string formulaFile = STORM_CPP_BASE_PATH "/builder/leader.prctl";
 
     storm::prism::Program program = storm::parseProgram(programFile);
 	// Build the die model