post-merge fixes

9 years ago · bf5018b858
52 changed files with 247 additions and 264 deletions
--- a/resources/examples/testfiles/mdp/wlan0-2-4.nm
+++ b/resources/examples/testfiles/mdp/wlan0-2-4.nm
--- 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 {
--- 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 {
        };
        
    }
-}
+}
--- 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>;
    }
-}
+}
--- 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 {
        };
        
    }
-}
+}
--- 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 {
        }
        
    }
-}
+}
--- 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 {
--- 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 {
--- 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 {
--- 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 {
        };
        
    }
-}
+}
--- 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 {
--- 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 {
--- 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 {
--- 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.
                 *
--- 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 {
--- 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 {
--- 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

--- 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 {
--- 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>;
        }
    }
-}
+}
--- 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 {
            
        }
    }
-}
+}
--- 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 {
--- 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 {
--- 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.");
--- 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"

--- 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): ";
--- 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 {
--- 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

--- 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_ */
+#endif /* STORM_MODELCHECKER_GAMEBASEDMDPMODELCHECKER_H_ */
--- 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 {
--- 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 {
--- 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 {
--- 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 {
            
        }
    }
-}
+}
--- 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 {
            
        }
    }
-}
+}
--- 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 {
            
        }
    }
-}
+}
--- 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 {
--- 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 {
--- 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 {
--- 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 {
--- 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 {
--- 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 {
--- 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"

--- 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 {
--- 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;
        }
        
--- 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:
--- 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);
--- 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;
--- 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 {
--- a/src/storm/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_ */
+#endif /* STORM_UTILITY_RESOURCES_H_ */
--- 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
-#)
--- a/test/functional/abstraction/PrismMenuGameTest.cpp
+++ b/test/functional/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>());
    
--- a/test/functional/modelchecker/GameBasedDtmcModelCheckerTest.cpp
+++ b/test/functional/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;
--- a/test/functional/modelchecker/GameBasedMdpModelCheckerTest.cpp
+++ b/test/functional/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