Merge branch 'python_api' of https://sselab.de/lab9/private/git/storm into python_api

Former-commit-id: 0c32a6f8ca
9 years ago · d09bd92ddf
42 changed files with 195 additions and 162 deletions
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@ -194,7 +194,15 @@ if(CUSTOM_BOOST_ROOT)
 endif(CUSTOM_BOOST_ROOT)

 if(STORM_PYTHON)
-find_package(Boost REQUIRED COMPONENTS python3)
+	find_package(Boost REQUIRED COMPONENTS python3)
+	#HACK for DEBIAN
+	if(NOT Boost_PYTHON3_FOUND)
+	set(PYVERSION 34)
+	load_library(pycarl Boost 1.55 COMPONENTS python-py${PYVERSION})
+	if(NOT Boost_PYTHON-PY${PYVERSION}_FOUND)
+		message(FATAL_ERROR "Could not find Boost Python")
+	endif()
+endif()
 else()
 find_package(Boost REQUIRED)
 endif()
--- a/src/builder/DdPrismModelBuilder.cpp
+++ b/src/builder/DdPrismModelBuilder.cpp
@ -201,7 +201,7 @@ namespace storm {
        }
        
        template <storm::dd::DdType Type, typename ValueType>
-        DdPrismModelBuilder<Type, ValueType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), terminalStates(), negatedTerminalStates() {
+        DdPrismModelBuilder<Type, ValueType>::Options::Options(std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), terminalStates(), negatedTerminalStates() {
            if (formulas.empty()) {
                this->buildAllRewardModels = true;
                this->buildAllLabels = true;
--- a/src/builder/DdPrismModelBuilder.h
+++ b/src/builder/DdPrismModelBuilder.h
@ -48,7 +48,7 @@ namespace storm {
                 *
                 * @param formula Thes formula based on which to choose the building options.
                 */
-                Options(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas);
+                Options(std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas);
                
                /*!
                 * Sets the constants definitions from the given string. The string must be of the form 'X=a,Y=b,Z=c',
--- a/src/builder/ExplicitPrismModelBuilder.cpp
+++ b/src/builder/ExplicitPrismModelBuilder.cpp
@ -129,7 +129,7 @@ namespace storm {
        }
        
        template <typename ValueType, typename RewardModelType, typename IndexType>
-        ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) : buildCommandLabels(false), buildAllRewardModels(false), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
+        ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::Options::Options(std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) : buildCommandLabels(false), buildAllRewardModels(false), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
            if (formulas.empty()) {
                this->buildAllRewardModels = true;
                this->buildAllLabels = true;
--- a/src/builder/ExplicitPrismModelBuilder.h
+++ b/src/builder/ExplicitPrismModelBuilder.h
@ -163,7 +163,7 @@ namespace storm {
                 *
                 * @param formula Thes formula based on which to choose the building options.
                 */
-                Options(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas);
+                Options(std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas);
                
                /*!
                 * Sets the constants definitions from the given string. The string must be of the form 'X=a,Y=b,Z=c',
--- a/src/cli/cli.cpp
+++ b/src/cli/cli.cpp
@ -220,17 +220,18 @@ namespace storm {
                }
                
                // Then proceed to parsing the property (if given), since the model we are building may depend on the property.
-                std::vector<std::shared_ptr<storm::logic::Formula>> formulas;
+                std::vector<std::shared_ptr<storm::logic::Formula>> parsedFormulas;
                if (settings.isPropertySet()) {
                    std::string properties = settings.getProperty();
                    
                    if(program) {
-                        formulas = storm::parseFormulasForProgram(properties, program.get());
+                        parsedFormulas = storm::parseFormulasForProgram(properties, program.get());
                    } else {
-                        formulas = storm::parseFormulasForExplicit(properties);
+                        parsedFormulas = storm::parseFormulasForExplicit(properties);
                    }
                    
                }
+                std::vector<std::shared_ptr<const storm::logic::Formula>> formulas(parsedFormulas.begin(), parsedFormulas.end());
                
                if (settings.isSymbolicSet()) {
 #ifdef STORM_HAVE_CARL
--- a/src/cli/entrypoints.h
+++ b/src/cli/entrypoints.h
@ -9,7 +9,7 @@ namespace storm {
    namespace cli {

        template<typename ValueType>
-        void verifySparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
+        void verifySparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) {
            for (auto const& formula : formulas) {
                std::cout << std::endl << "Model checking property: " << *formula << " ...";
                std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, formula));
@ -26,7 +26,7 @@ namespace storm {

 #ifdef STORM_HAVE_CARL
        template<>
-        inline void verifySparseModel(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
+        inline void verifySparseModel(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) {

            for (auto const& formula : formulas) {
                STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc, storm::exceptions::InvalidSettingsException, "Currently parametric verification is only available for DTMCs.");
@ -50,12 +50,12 @@ namespace storm {
 #endif

        template<storm::dd::DdType DdType>
-        void verifySymbolicModelWithAbstractionRefinementEngine(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
+        void verifySymbolicModelWithAbstractionRefinementEngine(storm::prism::Program const& program, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) {
            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Abstraction Refinement is not yet implemented.");
        }

        template<storm::dd::DdType DdType>
-        void verifySymbolicModelWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
+        void verifySymbolicModelWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) {
            for (auto const& formula : formulas) {
                std::cout << std::endl << "Model checking property: " << *formula << " ...";
                std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithHybridEngine(model, formula));
@ -72,7 +72,7 @@ namespace storm {
        }

        template<storm::dd::DdType DdType>
-        void verifySymbolicModelWithSymbolicEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
+        void verifySymbolicModelWithSymbolicEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) {
            for (auto const& formula : formulas) {
                std::cout << std::endl << "Model checking property: " << *formula << " ...";
                std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithDdEngine(model, formula));
@ -114,7 +114,7 @@ namespace storm {
    }
    
        template<typename ValueType, storm::dd::DdType LibraryType>
-        void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
+        void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) {

            storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();

@ -159,7 +159,7 @@ namespace storm {
        }
        
        template<typename ValueType>
-        void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
+        void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) {
            if (storm::settings::generalSettings().getDdLibraryType() == storm::dd::DdType::CUDD) {
                buildAndCheckSymbolicModel<ValueType, storm::dd::DdType::CUDD>(program, formulas);
            } else if (storm::settings::generalSettings().getDdLibraryType() == storm::dd::DdType::Sylvan) {
@ -168,7 +168,7 @@ namespace storm {
        }

        template<typename ValueType>
-        void buildAndCheckExplicitModel(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
+        void buildAndCheckExplicitModel(std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) {
            storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();

            STORM_LOG_THROW(settings.isExplicitSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files.");
--- a/src/counterexamples/MILPMinimalLabelSetGenerator.h
+++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h
@ -977,7 +977,7 @@ namespace storm {
             * @param formulaPtr A pointer to a safety formula. The outermost operator must be a probabilistic bound operator with a strict upper bound. The nested
             * formula can be either an unbounded until formula or an eventually formula.
             */
-            static void computeCounterexample(storm::prism::Program const& program, storm::models::sparse::Mdp<T> const& labeledMdp, std::shared_ptr<storm::logic::Formula> const& formula) {
+            static void computeCounterexample(storm::prism::Program const& program, storm::models::sparse::Mdp<T> const& labeledMdp, std::shared_ptr<const storm::logic::Formula> const& formula) {
                std::cout << std::endl << "Generating minimal label counterexample for formula " << *formula << std::endl;
                
                STORM_LOG_THROW(formula->isProbabilityOperatorFormula(), storm::exceptions::InvalidPropertyException, "Counterexample generation does not support this kind of formula. Expecting a probability operator as the outermost formula element.");
--- a/src/counterexamples/SMTMinimalCommandSetGenerator.h
+++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h
@ -1751,7 +1751,7 @@ namespace storm {
 #endif
            }
            
-            static void computeCounterexample(storm::prism::Program program, std::string const& constantDefinitionString, storm::models::sparse::Mdp<T> const& labeledMdp, std::shared_ptr<storm::logic::Formula> const& formula) {
+            static void computeCounterexample(storm::prism::Program program, std::string const& constantDefinitionString, storm::models::sparse::Mdp<T> const& labeledMdp, std::shared_ptr<const storm::logic::Formula> const& formula) {
 #ifdef STORM_HAVE_Z3
                std::cout << std::endl << "Generating minimal label counterexample for formula " << *formula << std::endl;
                
--- a/src/logic/ComparisonType.h
+++ b/src/logic/ComparisonType.h
@ -5,16 +5,17 @@

 namespace storm {
 	namespace logic {
-		enum class ComparisonType { Less, LessEqual, Greater, GreaterEqual };
-         
-                inline bool isStrict(ComparisonType t) {
-                    return (t == ComparisonType::Less || t == ComparisonType::Greater);
-                }
-                
-                inline bool isLowerBound(ComparisonType t) {
-                    return (t == ComparisonType::Greater || t == ComparisonType::GreaterEqual);
-                }
-        std::ostream& operator<<(std::ostream& out, ComparisonType const& comparisonType);
+            enum class ComparisonType { Less, LessEqual, Greater, GreaterEqual };
+
+            inline bool isStrict(ComparisonType t) {
+                return (t == ComparisonType::Less || t == ComparisonType::Greater);
+            }
+
+            inline bool isLowerBound(ComparisonType t) {
+                return (t == ComparisonType::Greater || t == ComparisonType::GreaterEqual);
+            }
+            
+            std::ostream& operator<<(std::ostream& out, ComparisonType const& comparisonType);
 	}
 }

--- a/src/logic/OperatorFormula.cpp
+++ b/src/logic/OperatorFormula.cpp
@ -10,14 +10,22 @@ namespace storm {
            return static_cast<bool>(bound);
        }
        
-        ComparisonType const& OperatorFormula::getComparisonType() const {
+        ComparisonType OperatorFormula::getComparisonType() const {
            return comparisonType.get();
        }
        
+        void OperatorFormula::setComparisonType(ComparisonType t) {
+            comparisonType = boost::optional<ComparisonType>(t);
+        }
+        
        double OperatorFormula::getBound() const {
            return bound.get();
        }
        
+        void OperatorFormula::setBound(double b) {
+            bound = boost::optional<double>(b);
+        }
+        
        bool OperatorFormula::hasOptimalityType() const {
            return static_cast<bool>(optimalityType);
        }
--- a/src/logic/OperatorFormula.h
+++ b/src/logic/OperatorFormula.h
@ -18,8 +18,10 @@ namespace storm {
            }
            
            bool hasBound() const;
-            ComparisonType const& getComparisonType() const;
+            ComparisonType getComparisonType() const;
+            void setComparisonType(ComparisonType);
            double getBound() const;
+            void setBound(double);
            bool hasOptimalityType() const;
            OptimizationDirection const& getOptimalityType() const;
            
--- a/src/python/helpers.h
+++ b/src/python/helpers.h
@ -7,10 +7,11 @@ void shared_ptr_implicitly_convertible() {
    boost::python::implicitly_convertible<std::shared_ptr<Source>, std::shared_ptr<Target>>();
 }

-
 template<typename T>
 void register_shared_ptr() {
    boost::python::register_ptr_to_python<std::shared_ptr<T>>();
+    boost::python::register_ptr_to_python<std::shared_ptr<const T>>();
+    
 }


--- a/src/python/storm-core.cpp
+++ b/src/python/storm-core.cpp
@ -18,7 +18,7 @@ public:

 // Thin wrapper for model building
 std::shared_ptr<storm::models::ModelBase> buildModel(storm::prism::Program const& program, std::shared_ptr<storm::logic::Formula> const& formula) {
-    return storm::buildSymbolicModel<storm::RationalFunction>(program, std::vector<std::shared_ptr<storm::logic::Formula>>(1,formula)).model;
+    return storm::buildSymbolicModel<storm::RationalFunction>(program, std::vector<std::shared_ptr<const storm::logic::Formula>>(1,formula)).model;
 }

 // Thin wrapper for parametric state elimination
@ -98,9 +98,6 @@ BOOST_PYTHON_MODULE(_core)
    defineClass<storm::models::sparse::Dtmc<storm::RationalFunction>,  storm::models::sparse::Model<storm::RationalFunction>>("SparseParametricDtmc", "");
    defineClass<storm::models::sparse::Mdp<storm::RationalFunction>, storm::models::sparse::Model<storm::RationalFunction>>("SparseParametricMdp", "");

-    defineClass<std::vector<std::shared_ptr<storm::logic::Formula>>, void, void>("FormulaVec", "Vector of formulas")
-        .def(vector_indexing_suite<std::vector<std::shared_ptr<storm::logic::Formula>>, true>())
-    ;
    
    ////////////////////////////////////////////
    // Bisimulation
@ -109,7 +106,7 @@ BOOST_PYTHON_MODULE(_core)
        .value("STRONG", storm::storage::BisimulationType::Strong)
        .value("WEAK", storm::storage::BisimulationType::Weak)
    ;
-    def("perform_bisimulation_parametric", static_cast<std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> (*)(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> const&, std::shared_ptr<storm::logic::Formula> const&, storm::storage::BisimulationType)>(&storm::performBisimulationMinimization<storm::models::sparse::Model<storm::RationalFunction>>));
+    def("perform_bisimulation_parametric", static_cast<std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> (*)(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> const&, std::shared_ptr<const storm::logic::Formula> const&, storm::storage::BisimulationType)>(&storm::performBisimulationMinimization<storm::models::sparse::Model<storm::RationalFunction>>));
    
    

--- a/src/python/storm-logic.cpp
+++ b/src/python/storm-logic.cpp
@ -5,13 +5,24 @@

 #include "helpers.h"
 #include "boostPyExtension.h"
-
+//  Less, LessEqual, Greater, GreaterEqual


 BOOST_PYTHON_MODULE(_logic)
 {
    using namespace boost::python;

+    enum_<storm::logic::ComparisonType>("ComparisonType")
+        .value("LESS", storm::logic::ComparisonType::Less)
+        .value("LEQ", storm::logic::ComparisonType::LessEqual)
+        .value("GREATER", storm::logic::ComparisonType::Greater)
+        .value("GEQ", storm::logic::ComparisonType::GreaterEqual)
+    ;
+    
+    defineClass<std::vector<std::shared_ptr<storm::logic::Formula>>, void, void>("FormulaVec", "Vector of formulas")
+        .def(vector_indexing_suite<std::vector<std::shared_ptr<storm::logic::Formula>>, true>())
+    ;
+    
    ////////////////////////////////////////////
    // Formula
    ////////////////////////////////////////////
@ -72,7 +83,11 @@ BOOST_PYTHON_MODULE(_logic)
    defineClass<storm::logic::UnaryBooleanStateFormula, storm::logic::UnaryStateFormula>("UnaryBooleanStateFormula",
    "");
    defineClass<storm::logic::OperatorFormula, storm::logic::UnaryStateFormula, boost::noncopyable>("OperatorFormula",
-    "");
+    "")
+        .add_property("has_bound", &storm::logic::OperatorFormula::hasBound)
+        .add_property("bound", &storm::logic::OperatorFormula::getBound, &storm::logic::OperatorFormula::setBound)
+        .add_property("comparison_type", &storm::logic::OperatorFormula::getComparisonType, &storm::logic::OperatorFormula::setComparisonType)
+    ;
    defineClass<storm::logic::ExpectedTimeOperatorFormula, storm::logic::OperatorFormula>("ExpectedTimeOperator",
    "The expected time between two events");
    defineClass<storm::logic::LongRunAverageOperatorFormula, storm::logic::OperatorFormula>("LongRunAvarageOperator",
--- a/src/storage/ModelFormulasPair.h
+++ b/src/storage/ModelFormulasPair.h
@ -10,7 +10,7 @@ namespace storm {
    namespace storage {
        struct ModelFormulasPair {
            std::shared_ptr<storm::models::ModelBase> model;
-            std::vector<std::shared_ptr<storm::logic::Formula>> formulas;
+            std::vector<std::shared_ptr<const storm::logic::Formula>> formulas;
        };
    }
 }
--- a/src/storage/bisimulation/BisimulationDecomposition.cpp
+++ b/src/storage/bisimulation/BisimulationDecomposition.cpp
@ -30,7 +30,7 @@ namespace storm {
        }
        
        template<typename ModelType, typename BlockDataType>
-        BisimulationDecomposition<ModelType, BlockDataType>::Options::Options(ModelType const& model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) : Options() {
+        BisimulationDecomposition<ModelType, BlockDataType>::Options::Options(ModelType const& model, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) : Options() {
            if (formulas.empty()) {
                this->respectedAtomicPropositions = model.getStateLabeling().getLabels();
                this->keepRewards = true;
--- a/src/storage/bisimulation/BisimulationDecomposition.h
+++ b/src/storage/bisimulation/BisimulationDecomposition.h
@ -79,7 +79,7 @@ namespace storm {
                 * derive a suitable initial partition.
                 * @param formulas The formulas that need to be preserved.
                 */
-                Options(ModelType const& model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas);
+                Options(ModelType const& model, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas);
                
                /*!
                 * Changes the options in a way that the given formula is preserved.
--- a/src/utility/storm.h
+++ b/src/utility/storm.h
@ -86,7 +86,7 @@ namespace storm {


    template<typename ValueType, storm::dd::DdType LibraryType = storm::dd::DdType::CUDD>
-    storm::storage::ModelFormulasPair buildSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
+    storm::storage::ModelFormulasPair buildSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) {
        storm::storage::ModelFormulasPair result;
        storm::prism::Program translatedProgram;

@ -136,7 +136,7 @@ namespace storm {
    }
    
    template<typename ModelType>
-    std::shared_ptr<ModelType> performDeterministicSparseBisimulationMinimization(std::shared_ptr<ModelType> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas, storm::storage::BisimulationType type) {
+    std::shared_ptr<ModelType> performDeterministicSparseBisimulationMinimization(std::shared_ptr<ModelType> model, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas, storm::storage::BisimulationType type) {
        std::cout << "Performing bisimulation minimization... ";
        typename storm::storage::DeterministicModelBisimulationDecomposition<ModelType>::Options options;
        if (!formulas.empty()) {
@ -152,7 +152,7 @@ namespace storm {
    }
    
    template<typename ModelType>
-    std::shared_ptr<ModelType> performNondeterministicSparseBisimulationMinimization(std::shared_ptr<ModelType> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas, storm::storage::BisimulationType type) {
+    std::shared_ptr<ModelType> performNondeterministicSparseBisimulationMinimization(std::shared_ptr<ModelType> model, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas, storm::storage::BisimulationType type) {
        std::cout << "Performing bisimulation minimization... ";
        typename storm::storage::DeterministicModelBisimulationDecomposition<ModelType>::Options options;
        if (!formulas.empty()) {
@ -169,7 +169,7 @@ namespace storm {
    }
    
    template<typename ModelType>
-    std::shared_ptr<storm::models::sparse::Model<typename ModelType::ValueType>> performBisimulationMinimization(std::shared_ptr<storm::models::sparse::Model<typename ModelType::ValueType>> const& model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas, storm::storage::BisimulationType type) {
+    std::shared_ptr<storm::models::sparse::Model<typename ModelType::ValueType>> performBisimulationMinimization(std::shared_ptr<storm::models::sparse::Model<typename ModelType::ValueType>> const& model, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas, storm::storage::BisimulationType type) {
        using ValueType = typename ModelType::ValueType;
        
        STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Dtmc) || model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::Mdp), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for DTMCs, CTMCs and MDPs.");
@ -185,14 +185,14 @@ namespace storm {
    }
        
    template<typename ModelType>
-    std::shared_ptr<storm::models::sparse::Model<typename ModelType::ValueType>> performBisimulationMinimization(std::shared_ptr<storm::models::sparse::Model<typename ModelType::ValueType>> const& model, std::shared_ptr<storm::logic::Formula> const& formula, storm::storage::BisimulationType type) {
-        std::vector<std::shared_ptr<storm::logic::Formula>> formulas = { formula };
+    std::shared_ptr<storm::models::sparse::Model<typename ModelType::ValueType>> performBisimulationMinimization(std::shared_ptr<storm::models::sparse::Model<typename ModelType::ValueType>> const& model, std::shared_ptr<const storm::logic::Formula> const& formula, storm::storage::BisimulationType type) {
+        std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = { formula };
        return performBisimulationMinimization<ModelType>(model, formulas , type);
    }
    
    
    template<typename ModelType>
-    std::shared_ptr<storm::models::ModelBase> preprocessModel(std::shared_ptr<storm::models::ModelBase> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
+    std::shared_ptr<storm::models::ModelBase> preprocessModel(std::shared_ptr<storm::models::ModelBase> model, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) {
        if (model->isSparseModel() && storm::settings::generalSettings().isBisimulationSet()) {
            storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong;
            if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) {
@ -207,7 +207,7 @@ namespace storm {
    
    
    template<typename ValueType>
-    void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::shared_ptr<storm::logic::Formula> const& formula) {
+    void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::shared_ptr<const storm::logic::Formula> const& formula) {
        if (storm::settings::counterexampleGeneratorSettings().isMinimalCommandSetGenerationSet()) {
            STORM_LOG_THROW(model->getType() == storm::models::ModelType::Mdp, storm::exceptions::InvalidTypeException, "Minimal command set generation is only available for MDPs.");
            STORM_LOG_THROW(storm::settings::generalSettings().isSymbolicSet(), storm::exceptions::InvalidSettingsException, "Minimal command set generation is only available for symbolic models.");
@ -230,13 +230,13 @@ namespace storm {
            
 #ifdef STORM_HAVE_CARL
    template<>
-    inline void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::shared_ptr<storm::logic::Formula> const& formula) {
+    inline void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::shared_ptr<const storm::logic::Formula> const& formula) {
        STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for parametric model.");
    }
 #endif

    template<typename ValueType, storm::dd::DdType DdType>
-    std::unique_ptr<storm::modelchecker::CheckResult> verifyModel(std::shared_ptr<storm::models::ModelBase> model, std::shared_ptr<storm::logic::Formula> const& formula) {
+    std::unique_ptr<storm::modelchecker::CheckResult> verifyModel(std::shared_ptr<storm::models::ModelBase> model, std::shared_ptr<const storm::logic::Formula> const& formula) {
        storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();
        switch(settings.getEngine()) {
            case storm::settings::modules::GeneralSettings::Engine::Sparse: {
@ -261,7 +261,7 @@ namespace storm {
    }

    template<typename ValueType>
-    std::unique_ptr<storm::modelchecker::CheckResult> verifySparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::shared_ptr<storm::logic::Formula> const& formula) {
+    std::unique_ptr<storm::modelchecker::CheckResult> verifySparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::shared_ptr<const storm::logic::Formula> const& formula) {

        std::unique_ptr<storm::modelchecker::CheckResult> result;
        if (model->getType() == storm::models::ModelType::Dtmc) {
@ -317,7 +317,7 @@ namespace storm {
    }

    template<>
-    inline std::unique_ptr<storm::modelchecker::CheckResult> verifySparseModel(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::shared_ptr<storm::logic::Formula> const& formula) {
+    inline std::unique_ptr<storm::modelchecker::CheckResult> verifySparseModel(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::shared_ptr<const storm::logic::Formula> const& formula) {
        std::unique_ptr<storm::modelchecker::CheckResult> result;
        std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();

@ -333,7 +333,7 @@ namespace storm {
 #endif

    template<storm::dd::DdType DdType>
-    std::unique_ptr<storm::modelchecker::CheckResult> verifySymbolicModelWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::shared_ptr<storm::logic::Formula> const& formula) {
+    std::unique_ptr<storm::modelchecker::CheckResult> verifySymbolicModelWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::shared_ptr<const storm::logic::Formula> const& formula) {
        std::unique_ptr<storm::modelchecker::CheckResult> result;
        if (model->getType() == storm::models::ModelType::Dtmc) {
            std::shared_ptr<storm::models::symbolic::Dtmc<DdType>> dtmc = model->template as<storm::models::symbolic::Dtmc<DdType>>();
@ -361,7 +361,7 @@ namespace storm {


    template<storm::dd::DdType DdType>
-    std::unique_ptr<storm::modelchecker::CheckResult> verifySymbolicModelWithDdEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::shared_ptr<storm::logic::Formula> const& formula) {
+    std::unique_ptr<storm::modelchecker::CheckResult> verifySymbolicModelWithDdEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::shared_ptr<const storm::logic::Formula> const& formula) {
        std::unique_ptr<storm::modelchecker::CheckResult> result;
        if (model->getType() == storm::models::ModelType::Dtmc) {
            std::shared_ptr<storm::models::symbolic::Dtmc<DdType>> dtmc = model->template as<storm::models::symbolic::Dtmc<DdType>>();
--- a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
@ -24,7 +24,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Cluster) {
    // Parse the model description.
    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
    storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
-    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    std::shared_ptr<const storm::logic::Formula> formula(nullptr);
    
    // Build the model.
 #ifdef WINDOWS
@ -107,7 +107,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Embedded) {
    // Parse the model description.
    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
    storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
-    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    std::shared_ptr<const storm::logic::Formula> formula(nullptr);
    
    // Build the model.
 #ifdef WINDOWS
@ -176,7 +176,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Polling) {
    // Parse the model description.
    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
    storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
-    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    std::shared_ptr<const storm::logic::Formula> formula(nullptr);
    
    // Build the model.
    std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
@ -217,7 +217,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Tandem) {
    // Parse the model description.
    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
    storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
-    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    std::shared_ptr<const storm::logic::Formula> formula(nullptr);
    
    // Build the model.
 #ifdef WINDOWS
--- a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
@ -29,7 +29,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Die) {

    storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));

-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");

    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
@ -73,7 +73,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {

    storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));

-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");

    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
@ -110,7 +110,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {

    storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));

-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");

    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
@ -153,7 +153,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) {

        storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));

-        std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
+        std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");

        std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
        storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
@ -177,7 +177,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) {

        storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));

-        std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
+        std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");

        std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
        storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
@ -201,7 +201,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) {

        storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));

-        std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
+        std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");

        std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
        storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
@ -264,7 +264,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRA) {

        storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));

-        std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
+        std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");

        std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
        storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
--- a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp
@ -27,7 +27,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Cudd) {
    // Parse the model description.
    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
    storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
-    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    std::shared_ptr<const storm::logic::Formula> formula(nullptr);
    
    // Build the model.
 #ifdef WINDOWS
@ -124,7 +124,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Sylvan) {
    // Parse the model description.
    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
    storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
-    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    std::shared_ptr<const storm::logic::Formula> formula(nullptr);
    
    // Build the model.
 #ifdef WINDOWS
@ -221,7 +221,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded_Cudd) {
    // Parse the model description.
    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
    storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
-    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    std::shared_ptr<const storm::logic::Formula> formula(nullptr);
    
    // Build the model.
 #ifdef WINDOWS
@ -300,7 +300,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded_Sylvan) {
    // Parse the model description.
    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
    storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
-    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    std::shared_ptr<const storm::logic::Formula> formula(nullptr);
    
    // Build the model.
 #ifdef WINDOWS
@ -379,7 +379,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling_Cudd) {
    // Parse the model description.
    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
    storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
-    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    std::shared_ptr<const storm::logic::Formula> formula(nullptr);
    
    // Build the model.
    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
@ -415,7 +415,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling_Sylvan) {
    // Parse the model description.
    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
    storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
-    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    std::shared_ptr<const storm::logic::Formula> formula(nullptr);
    
    // Build the model.
    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
@ -458,7 +458,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem_Cudd) {
    // Parse the model description.
    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
    storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
-    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    std::shared_ptr<const storm::logic::Formula> formula(nullptr);
    
    // Build the model with the customers reward structure.
 #ifdef WINDOWS
@ -546,7 +546,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem_Sylvan) {
    // Parse the model description.
    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
    storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
-    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    std::shared_ptr<const storm::logic::Formula> formula(nullptr);
    
    // Build the model with the customers reward structure.
 #ifdef WINDOWS
--- a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
@ -42,7 +42,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die_Cudd) {
    
    storm::modelchecker::HybridDtmcPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -103,7 +103,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die_Sylvan) {
    
    storm::modelchecker::HybridDtmcPrctlModelChecker<storm::dd::DdType::Sylvan, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
@ -156,7 +156,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds_Cudd) {
    
    storm::modelchecker::HybridDtmcPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -200,7 +200,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds_Sylvan) {
    
    storm::modelchecker::HybridDtmcPrctlModelChecker<storm::dd::DdType::Sylvan, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
@ -252,7 +252,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) {
    
    storm::modelchecker::HybridDtmcPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -304,7 +304,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) {
    
    storm::modelchecker::HybridDtmcPrctlModelChecker<storm::dd::DdType::Sylvan, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
--- a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
@ -44,7 +44,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Cudd) {
    
    storm::modelchecker::HybridMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Gmmxx)));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -141,7 +141,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Sylvan) {
    
    storm::modelchecker::HybridMdpPrctlModelChecker<storm::dd::DdType::Sylvan, double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Gmmxx)));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
@ -238,7 +238,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) {
    
    storm::modelchecker::HybridMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Gmmxx)));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -317,7 +317,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) {
    
    storm::modelchecker::HybridMdpPrctlModelChecker<storm::dd::DdType::Sylvan, double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Gmmxx)));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
--- a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
@ -30,7 +30,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {

    storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Gmmxx)));

-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");

    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
@ -146,7 +146,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {

    storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Gmmxx)));

-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");

    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
--- a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp
+++ b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp
@ -22,7 +22,7 @@ TEST(NativeCtmcCslModelCheckerTest, Cluster) {
    // Parse the model description.
    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
    storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
-    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    std::shared_ptr<const storm::logic::Formula> formula(nullptr);
    
    // Build the model.
 #ifdef WINDOWS
@ -98,7 +98,7 @@ TEST(NativeCtmcCslModelCheckerTest, Embedded) {
    // Parse the model description.
    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
    storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
-    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    std::shared_ptr<const storm::logic::Formula> formula(nullptr);
    
    // Build the model.
 #ifdef WINDOWS
@ -160,7 +160,7 @@ TEST(NativeCtmcCslModelCheckerTest, Polling) {
    // Parse the model description.
    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
    storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
-    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    std::shared_ptr<const storm::logic::Formula> formula(nullptr);
    
    // Build the model.
    std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
@ -194,7 +194,7 @@ TEST(NativeCtmcCslModelCheckerTest, Tandem) {
    // Parse the model description.
    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
    storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
-    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    std::shared_ptr<const storm::logic::Formula> formula(nullptr);
    
    // Build the model with the customers reward structure.
 #ifdef WINDOWS
--- a/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
@ -31,7 +31,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, Die) {
    
    storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
@ -75,7 +75,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, Crowds) {
    
    storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
@ -112,7 +112,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, SynchronousLeader) {
    
    storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
@ -155,7 +155,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) {

        storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>(storm::solver::NativeLinearEquationSolverSolutionMethod::SOR, 0.9)));

-        std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
+        std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
        
        std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
 		storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
@ -179,7 +179,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) {

        storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>(storm::solver::NativeLinearEquationSolverSolutionMethod::SOR, 0.9)));

-        std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
+        std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
        
        std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
 		storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
@ -203,7 +203,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) {

        storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>(storm::solver::NativeLinearEquationSolverSolutionMethod::SOR, 0.9)));

-        std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
+        std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
        
        std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
 		storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
@ -266,7 +266,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRA) {

        storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>(storm::solver::NativeLinearEquationSolverSolutionMethod::SOR, 0.9)));

-        std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
+        std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
        
        std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
 		storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
--- a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp
+++ b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp
@ -26,7 +26,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Cudd) {
    // Parse the model description.
    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
    storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
-    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    std::shared_ptr<const storm::logic::Formula> formula(nullptr);
    
    // Build the model.
 #ifdef WINDOWS
@ -123,7 +123,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Sylvan) {
    // Parse the model description.
    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
    storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
-    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    std::shared_ptr<const storm::logic::Formula> formula(nullptr);
    
    // Build the model.
 #ifdef WINDOWS
@ -220,7 +220,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Cudd) {
    // Parse the model description.
    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
    storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
-    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    std::shared_ptr<const storm::logic::Formula> formula(nullptr);
    
    // Build the model.
 #ifdef WINDOWS
@ -299,7 +299,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Sylvan) {
    // Parse the model description.
    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
    storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
-    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    std::shared_ptr<const storm::logic::Formula> formula(nullptr);
    
    // Build the model.
 #ifdef WINDOWS
@ -378,7 +378,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Cudd) {
    // Parse the model description.
    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
    storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
-    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    std::shared_ptr<const storm::logic::Formula> formula(nullptr);
    
    // Build the model.
    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
@ -414,7 +414,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Sylvan) {
    // Parse the model description.
    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
    storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
-    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    std::shared_ptr<const storm::logic::Formula> formula(nullptr);
    
    // Build the model.
    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
@ -457,7 +457,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Cudd) {
    // Parse the model description.
    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
    storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
-    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    std::shared_ptr<const storm::logic::Formula> formula(nullptr);
    
    // Build the model with the customers reward structure.
 #ifdef WINDOWS
@ -547,7 +547,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Sylvan) {
    // Parse the model description.
    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
    storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
-    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    std::shared_ptr<const storm::logic::Formula> formula(nullptr);
    
    // Build the model with the customers reward structure.
 #ifdef WINDOWS
--- a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp
@ -43,7 +43,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die_Cudd) {
    
    storm::modelchecker::HybridDtmcPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -104,7 +104,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die_Sylvan) {
    
    storm::modelchecker::HybridDtmcPrctlModelChecker<storm::dd::DdType::Sylvan, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
@ -157,7 +157,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds_Cudd) {
    
    storm::modelchecker::HybridDtmcPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -201,7 +201,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds_Sylvan) {
    
    storm::modelchecker::HybridDtmcPrctlModelChecker<storm::dd::DdType::Sylvan, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
@ -253,7 +253,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) {
    
    storm::modelchecker::HybridDtmcPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -305,7 +305,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) {
    
    storm::modelchecker::HybridDtmcPrctlModelChecker<storm::dd::DdType::Sylvan, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
--- a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
@ -41,7 +41,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Cudd) {
    std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
    
    storm::modelchecker::HybridMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native)));
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -137,7 +137,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Sylvan) {
    std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
    
    storm::modelchecker::HybridMdpPrctlModelChecker<storm::dd::DdType::Sylvan, double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native)));
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
@ -234,7 +234,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) {
    
    storm::modelchecker::HybridMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native)));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -313,7 +313,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) {
    
    storm::modelchecker::HybridMdpPrctlModelChecker<storm::dd::DdType::Sylvan, double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native)));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
--- a/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
@ -29,7 +29,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {

    storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native)));

-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");

    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
@ -145,7 +145,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {

    storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native)));

-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");

    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
@ -209,7 +209,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {

        storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native)));

-        std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
+        std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");

        std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
        storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
@ -241,7 +241,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {

        storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native)));

-        std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
+        std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");

        std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
        storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
@ -282,7 +282,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {

        storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native)));

-        std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
+        std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");

        std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
        storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
@ -368,7 +368,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) {

        storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native)));

-        std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
+        std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");

        std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
        storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
@ -490,7 +490,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) {

        storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native)));

-        std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
+        std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");

        std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
        storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
--- a/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp
+++ b/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp
@ -27,7 +27,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, Die) {

    storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc);

-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");

    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
@ -71,7 +71,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, Crowds) {

    storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc);

-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");

    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
@ -121,7 +121,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, SynchronousLeader) {

    storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc);

-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");

    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
--- a/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
@ -41,7 +41,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Cudd) {
    
    storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>()));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -102,7 +102,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Sylvan) {
    
    storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::dd::DdType::Sylvan, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>(new storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>()));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
@ -156,7 +156,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Cudd) {
    
    storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>()));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -200,7 +200,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Sylvan) {
    
    storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::dd::DdType::Sylvan, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>(new storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>()));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
@ -255,7 +255,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) {
    
    storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>()));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -307,7 +307,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) {
    
    storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::dd::DdType::Sylvan, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>(new storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>()));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
--- a/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp
@ -41,7 +41,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Cudd) {
    
    storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>()));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -138,7 +138,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Sylvan) {
    
    storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::dd::DdType::Sylvan, double> checker(*mdp, std::unique_ptr<storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>()));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
@ -235,7 +235,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) {
    
    storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>()));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -314,7 +314,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) {
    
    storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::dd::DdType::Sylvan, double> checker(*mdp, std::unique_ptr<storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>()));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
--- a/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp
@ -28,7 +28,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) {

    storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> mc(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Topological)));

-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");

    std::unique_ptr<storm::modelchecker::CheckResult> result = mc.check(*formula);

@ -145,7 +145,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) {

    storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> mc(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Topological)));

-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");

    std::unique_ptr<storm::modelchecker::CheckResult> result = mc.check(*formula);

--- a/test/functional/parser/FormulaParserTest.cpp
+++ b/test/functional/parser/FormulaParserTest.cpp
@ -7,7 +7,7 @@ TEST(FormulaParserTest, LabelTest) {
    storm::parser::FormulaParser formulaParser;

    std::string input = "\"label\"";
-    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    std::shared_ptr<const storm::logic::Formula> formula(nullptr);
 	ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));

    EXPECT_TRUE(formula->isAtomicLabelFormula());
@ -17,7 +17,7 @@ TEST(FormulaParserTest, ComplexLabelTest) {
    storm::parser::FormulaParser formulaParser;

    std::string input = "!(\"a\" & \"b\") | \"a\" & !\"c\"";
-    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    std::shared_ptr<const storm::logic::Formula> formula(nullptr);
 	ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));

    EXPECT_TRUE(formula->isPropositionalFormula());
@ -32,7 +32,7 @@ TEST(FormulaParserTest, ExpressionTest) {
    storm::parser::FormulaParser formulaParser(manager);
    
    std::string input = "!(x | y > 3)";
-    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    std::shared_ptr<const storm::logic::Formula> formula(nullptr);
    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
    
    EXPECT_TRUE(formula->isPropositionalFormula());
@ -47,7 +47,7 @@ TEST(FormulaParserTest, LabelAndExpressionTest) {
    storm::parser::FormulaParser formulaParser(manager);
    
    std::string input = "!\"a\" | x | y > 3";
-    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    std::shared_ptr<const storm::logic::Formula> formula(nullptr);
    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
    
    EXPECT_TRUE(formula->isPropositionalFormula());
@ -61,7 +61,7 @@ TEST(FormulaParserTest, ProbabilityOperatorTest) {
    storm::parser::FormulaParser formulaParser;

    std::string input = "P<0.9 [\"a\" U \"b\"]";
-    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    std::shared_ptr<const storm::logic::Formula> formula(nullptr);
 	ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));

    EXPECT_TRUE(formula->isProbabilityOperatorFormula());
@ -73,7 +73,7 @@ TEST(FormulaParserTest, RewardOperatorTest) {
    storm::parser::FormulaParser formulaParser;
    
    std::string input = "Rmin<0.9 [F \"a\"]";
-    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    std::shared_ptr<const storm::logic::Formula> formula(nullptr);
    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
    
    EXPECT_TRUE(formula->isRewardOperatorFormula());
@ -93,7 +93,7 @@ TEST(FormulaParserTest, ConditionalProbabilityTest) {
    storm::parser::FormulaParser formulaParser;
    
    std::string input = "P<0.9 [F \"a\" || F \"b\"]";
-    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    std::shared_ptr<const storm::logic::Formula> formula(nullptr);
    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
    
    EXPECT_TRUE(formula->isProbabilityOperatorFormula());
@ -105,7 +105,7 @@ TEST(FormulaParserTest, NestedPathFormulaTest) {
    storm::parser::FormulaParser formulaParser;
    
    std::string input = "P<0.9 [F X \"a\"]";
-    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    std::shared_ptr<const storm::logic::Formula> formula(nullptr);
    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
    
    EXPECT_TRUE(formula->isProbabilityOperatorFormula());
@ -117,7 +117,7 @@ TEST(FormulaParserTest, CommentTest) {
    storm::parser::FormulaParser formulaParser;

    std::string input = "// This is a comment. And this is a commented out formula: P<=0.5 [ F \"a\" ] The next line contains the actual formula. \n P<=0.5 [ X \"b\" ] // Another comment \n // And again: another comment.";
-    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    std::shared_ptr<const storm::logic::Formula> formula(nullptr);
 	ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
    EXPECT_TRUE(formula->isProbabilityOperatorFormula());
    ASSERT_TRUE(formula->asProbabilityOperatorFormula().getSubformula().isNextFormula());
@ -132,7 +132,7 @@ TEST(FormulaParserTest, WrongFormatTest) {
    
    storm::parser::FormulaParser formulaParser(manager);
    std::string input = "P>0.5 [ a ]";
-    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    std::shared_ptr<const storm::logic::Formula> formula(nullptr);
 	EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
    
    input = "P=0.5 [F \"a\"]";
--- a/test/functional/storage/NondeterministicModelBisimulationDecompositionTest.cpp
+++ b/test/functional/storage/NondeterministicModelBisimulationDecompositionTest.cpp
@ -43,7 +43,7 @@ TEST(NondeterministicModelBisimulationDecomposition, TwoDice) {

    // A parser that we use for conveniently constructing the formulas.
    storm::parser::FormulaParser formulaParser;
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");

    typename storm::storage::NondeterministicModelBisimulationDecomposition<storm::models::sparse::Mdp<double>>::Options options2(*mdp, *formula);
    
--- a/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
+++ b/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
@ -26,7 +26,7 @@ TEST(GmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
    
    storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Gmmxx)));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
@ -84,7 +84,7 @@ TEST(GmxxMdpPrctlModelCheckerTest, Consensus) {
    
    storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Gmmxx)));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
--- a/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
+++ b/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
@ -27,7 +27,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {

    storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native)));

-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
@ -85,7 +85,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
    
 	storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native)));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
--- a/test/performance/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
+++ b/test/performance/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
@ -41,7 +41,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) {
    
    storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>()));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -93,7 +93,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) {
    
    storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::dd::DdType::Sylvan, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>(new storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>()));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
@ -137,7 +137,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Cudd) {
    
    storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>()));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -181,7 +181,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Sylvan) {
    
    storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::dd::DdType::Sylvan, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>(new storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>()));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
--- a/test/performance/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp
+++ b/test/performance/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp
@ -41,7 +41,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) {
    
    storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>()));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -93,7 +93,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) {
    
    storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::dd::DdType::Sylvan, double> checker(*mdp, std::unique_ptr<storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>()));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
@ -149,7 +149,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, CSMA_Cudd) {
    
    storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>()));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [ !\"collision_max_backoff\" U \"all_delivered\" ]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [ !\"collision_max_backoff\" U \"all_delivered\" ]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -206,7 +206,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, CSMA_Sylvan) {
    
    storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::dd::DdType::Sylvan, double> checker(*mdp, std::unique_ptr<storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>()));
    
-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [ !\"collision_max_backoff\" U \"all_delivered\" ]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [ !\"collision_max_backoff\" U \"all_delivered\" ]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
--- a/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp
+++ b/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp
@ -22,7 +22,7 @@ TEST(DISABLED_TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLea

    storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Topological)));

-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);

@ -69,7 +69,7 @@ TEST(DISABLED_TopologicalValueIterationMdpPrctlModelCheckerTest, Consensus) {
    
 	storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Topological)));

-    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]");
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]");
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);