storm-dft is using settings now

Former-commit-id: 65a1456651

src/modelchecker/DFTAnalyser.h

@@ -159,7 +159,7 @@ private:
             explorationTime += explorationEnd -buildingEnd;
 
             // Bisimulation
-            if (model->isOfType(storm::models::ModelType::Ctmc)) {
+            if (model->isOfType(storm::models::ModelType::Ctmc) && storm::settings::getModule<storm::settings::modules::GeneralSettings>().isBisimulationSet()) {
                 std::cout << "Bisimulation..." << std::endl;
                 model =  storm::performDeterministicSparseBisimulationMinimization<storm::models::sparse::Ctmc<ValueType>>(model->template as<storm::models::sparse::Ctmc<ValueType>>(), {formula}, storm::storage::BisimulationType::Weak)->template as<storm::models::sparse::Ctmc<ValueType>>();
                 //model->printModelInformationToStream(std::cout);

src/settings/ArgumentValidators.h

@@ -46,6 +46,26 @@ namespace storm {
 				return rangeValidatorExcluding<int_fast64_t>(lowerBound, upperBound);
 			}
 
+            /*!
+             * Creates a validation function that checks whether an integer is greater than or equal to the given threshold.
+             *
+             * @param threshold The threshold.
+             * @return The resulting validation function.
+             */
+            static std::function<bool (int_fast64_t const&)> integerGreaterValidatorIncluding(int_fast64_t threshold) {
+                return greaterValidatorIncluding<int_fast64_t>(threshold);
+            }
+            
+            /*!
+             * Creates a validation function that checks whether an integer is greater than the given threshold.
+             *
+             * @param threshold The threshold.
+             * @return The resulting validation function.
+             */
+            static std::function<bool (int_fast64_t const&)> integerGreaterValidatorExcluding(int_fast64_t threshold) {
+                return greaterValidatorExcluding<int_fast64_t>(threshold);
+            }
+            
 			/*!
              * Creates a validation function that checks whether an unsigned integer is in the given range (including the bounds).
              *
@@ -67,6 +87,26 @@ namespace storm {
 			static std::function<bool (uint_fast64_t const&)> unsignedIntegerRangeValidatorExcluding(uint_fast64_t lowerBound, uint_fast64_t upperBound) {
 				return rangeValidatorExcluding<uint_fast64_t>(lowerBound, upperBound);
 			}
+            
+            /*!
+             * Creates a validation function that checks whether an unsigned integer is greater than or equal to the given threshold.
+             *
+             * @param threshold The threshold.
+             * @return The resulting validation function.
+             */
+            static std::function<bool (uint_fast64_t const&)> unsignedIntegerGreaterValidatorIncluding(uint_fast64_t threshold) {
+                return greaterValidatorIncluding<uint_fast64_t>(threshold);
+            }
+            
+            /*!
+             * Creates a validation function that checks whether an unsigned integer is greater than the given threshold.
+             *
+             * @param threshold The threshold.
+             * @return The resulting validation function.
+             */
+            static std::function<bool (uint_fast64_t const&)> unsignedIntegerGreaterValidatorExcluding(uint_fast64_t threshold) {
+                return greaterValidatorExcluding<uint_fast64_t>(threshold);
+            }
 
 			/*!
              * Creates a validation function that checks whether a double is in the given range (including the bounds).
@@ -89,6 +129,26 @@ namespace storm {
 			static std::function<bool (double const&)> doubleRangeValidatorExcluding(double lowerBound, double upperBound) {
 				return rangeValidatorExcluding<double>(lowerBound, upperBound);
 			}
+            
+            /*!
+             * Creates a validation function that checks whether a double is greater than or equal to the given threshold.
+             *
+             * @param threshold The threshold.
+             * @return The resulting validation function.
+             */
+            static std::function<bool (double const&)> doubleGreaterValidatorIncluding(double threshold) {
+                return greaterValidatorIncluding<double>(threshold);
+            }
+            
+            /*!
+             * Creates a validation function that checks whether a double is greater than the given threshold.
+             *
+             * @param threshold The threshold.
+             * @return The resulting validation function.
+             */
+            static std::function<bool (double const&)> doubleGreaterValidatorExcluding(double threshold) {
+                return greaterValidatorExcluding<double>(threshold);
+            }
 
             /*!
              * Creates a validation function that checks whether a given string corresponds to an existing and readable
@@ -141,7 +201,7 @@ namespace storm {
 			template<typename T>
 			static std::function<bool (T const&)> rangeValidatorIncluding(T lowerBound, T upperBound) {
 				return std::bind([](T lowerBound, T upperBound, T value) -> bool {
-                    STORM_LOG_THROW(lowerBound <= value && value <= upperBound, storm::exceptions::InvalidArgumentException, "Value " << value << " is out range.");
+                    STORM_LOG_THROW(lowerBound <= value && value <= upperBound, storm::exceptions::InvalidArgumentException, "Value " << value << " is out of range.");
                     return true;
                 }, lowerBound, upperBound, std::placeholders::_1);
 			}
@@ -156,10 +216,38 @@ namespace storm {
 			template<typename T>
 			static std::function<bool (T const&)> rangeValidatorExcluding(T lowerBound, T upperBound) {
 				return std::bind([](T lowerBound, T upperBound, T value) -> bool {
-                    STORM_LOG_THROW(lowerBound < value && value < upperBound, storm::exceptions::InvalidArgumentException, "Value " << value << " is out range.");
+                    STORM_LOG_THROW(lowerBound < value && value < upperBound, storm::exceptions::InvalidArgumentException, "Value " << value << " is out of range.");
                     return true;
 				}, lowerBound, upperBound, std::placeholders::_1);
 			}
+            
+            /*!
+             * Creates a validation function that checks whether its argument is greater than the given threshold.
+             *
+             * @param threshold The threshold.
+             * @return The resulting validation function.
+             */
+            template<typename T>
+            static std::function<bool (T const&)> greaterValidatorExcluding(T threshold) {
+                return std::bind([](T threshold, T value) -> bool {
+                    STORM_LOG_THROW(threshold < value, storm::exceptions::InvalidArgumentException, "Value " << value << " is out of range.");
+                    return true;
+                }, threshold, std::placeholders::_1);
+            }
+            
+            /*!
+             * Creates a validation function that checks whether its argument is greater than or equal to the given threshold.
+             *
+             * @param threshold The threshold.
+             * @return The resulting validation function.
+             */
+            template<typename T>
+            static std::function<bool (T const&)> greaterValidatorIncluding(T threshold) {
+                return std::bind([](T threshold, T value) -> bool {
+                    STORM_LOG_THROW(threshold <= value, storm::exceptions::InvalidArgumentException, "Value " << value << " is out of range.");
+                    return true;
+                }, threshold, std::placeholders::_1);
+            }
 		};
 	}
 }

src/settings/SettingsManager.cpp

@@ -499,8 +499,8 @@ namespace storm {
             
             // Register all known settings modules.
             storm::settings::addModule<storm::settings::modules::GeneralSettings>();
-            storm::settings::addModule<storm::settings::modules::MarkovChainSettings>();
             storm::settings::addModule<storm::settings::modules::IOSettings>();
+            storm::settings::addModule<storm::settings::modules::MarkovChainSettings>();
             storm::settings::addModule<storm::settings::modules::DebugSettings>();
             storm::settings::addModule<storm::settings::modules::CounterexampleGeneratorSettings>();
             storm::settings::addModule<storm::settings::modules::CuddSettings>();

src/settings/modules/DFTSettings.cpp

@@ -0,0 +1,107 @@
+#include "src/settings/modules/DFTSettings.h"
+
+#include "src/settings/SettingsManager.h"
+#include "src/settings/SettingMemento.h"
+#include "src/settings/Option.h"
+#include "src/settings/OptionBuilder.h"
+#include "src/settings/ArgumentBuilder.h"
+#include "src/settings/Argument.h"
+
+#include "src/exceptions/InvalidSettingsException.h"
+
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            
+            const std::string DFTSettings::moduleName = "dft";
+            const std::string DFTSettings::dftFileOptionName = "dftfile";
+            const std::string DFTSettings::dftFileOptionShortName = "dft";
+            const std::string DFTSettings::symmetryReductionOptionName = "symmetryreduction";
+            const std::string DFTSettings::symmetryReductionOptionShortName = "symred";
+            const std::string DFTSettings::modularisationOptionName = "modularisation";
+            const std::string DFTSettings::disableDCOptionName = "disabledc";
+            const std::string DFTSettings::propExpectedTimeOptionName = "expectedtime";
+            const std::string DFTSettings::propExpectedTimeOptionShortName = "mttf";
+            const std::string DFTSettings::propProbabilityOptionName = "probability";
+            const std::string DFTSettings::propTimeBoundOptionName = "timebound";
+            const std::string DFTSettings::minValueOptionName = "min";
+            const std::string DFTSettings::maxValueOptionName = "max";
+
+            DFTSettings::DFTSettings() : ModuleSettings(moduleName) {
+                this->addOption(storm::settings::OptionBuilder(moduleName, dftFileOptionName, false, "Parses the model given in the Galileo format.").setShortName(dftFileOptionShortName)
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the DFT model.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, symmetryReductionOptionName, false, "Exploit symmetric structure of model.").setShortName(symmetryReductionOptionShortName).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, modularisationOptionName, false, "Use modularisation (not applicable for expected time).").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, disableDCOptionName, false, "Disable Dont Care propagation.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, propExpectedTimeOptionName, false, "Compute expected time of system failure.").setShortName(propExpectedTimeOptionShortName).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, propProbabilityOptionName, false, "Compute probability of system failure.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, propTimeBoundOptionName, false, "Compute probability of system failure up to given timebound.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("time", "The timebound to use.").addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleGreaterValidatorExcluding(0.0)).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, minValueOptionName, false, "Compute minimal value in case of non-determinism.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, maxValueOptionName, false, "Compute maximal value in case of non-determinism.").build());
+            }
+            
+            bool DFTSettings::isDftFileSet() const {
+                return this->getOption(dftFileOptionName).getHasOptionBeenSet();
+            }
+            
+            std::string DFTSettings::getDftFilename() const {
+                return this->getOption(dftFileOptionName).getArgumentByName("filename").getValueAsString();
+            }
+            
+            bool DFTSettings::useSymmetryReduction() const {
+                return this->getOption(symmetryReductionOptionName).getHasOptionBeenSet();
+            }
+            
+            bool DFTSettings::useModularisation() const {
+                return this->getOption(modularisationOptionName).getHasOptionBeenSet();
+            }
+            
+            bool DFTSettings::isDisableDC() const {
+                return this->getOption(disableDCOptionName).getHasOptionBeenSet();
+            }
+            
+            bool DFTSettings::usePropExpectedTime() const {
+                return this->getOption(propExpectedTimeOptionName).getHasOptionBeenSet();
+            }
+            
+            bool DFTSettings::usePropProbability() const {
+                return this->getOption(propProbabilityOptionName).getHasOptionBeenSet();
+            }
+            
+            bool DFTSettings::usePropTimebound() const {
+                return this->getOption(propTimeBoundOptionName).getHasOptionBeenSet();
+            }
+            
+            double DFTSettings::getPropTimebound() const {
+                return this->getOption(propTimeBoundOptionName).getArgumentByName("time").getValueAsDouble();
+            }
+            
+            bool DFTSettings::isComputeMinimalValue() const {
+                return this->getOption(minValueOptionName).getHasOptionBeenSet();
+            }
+            
+            bool DFTSettings::isComputeMaximalValue() const {
+                return this->getOption(maxValueOptionName).getHasOptionBeenSet();
+            }
+            
+            void DFTSettings::finalize() {
+                
+            }
+
+            bool DFTSettings::check() const {
+                // Ensure that only one property is given.
+                if (usePropExpectedTime()) {
+                    STORM_LOG_THROW(!usePropProbability() && !usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given.");
+                } else if (usePropProbability()) {
+                    STORM_LOG_THROW(!usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given.");
+                }
+                
+                // Ensure that at most one of min or max is set
+                STORM_LOG_THROW(!isComputeMinimalValue() || !isComputeMaximalValue(), storm::exceptions::InvalidSettingsException, "Min and max can not both be set.");
+                return true;
+            }
+            
+        } // namespace modules
+    } // namespace settings
+} // namespace storm

src/settings/modules/DFTSettings.h

@@ -0,0 +1,129 @@
+#ifndef STORM_SETTINGS_MODULES_DFTSETTINGS_H_
+#define STORM_SETTINGS_MODULES_DFTSETTINGS_H_
+
+#include "storm-config.h"
+#include "src/settings/modules/ModuleSettings.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+
+            /*!
+             * This class represents the settings for DFT model checking.
+             */
+            class DFTSettings : public ModuleSettings {
+            public:
+
+                /*!
+                 * Creates a new set of DFT settings.
+                 */
+                DFTSettings();
+                
+                /*!
+                 * Retrieves whether the dft file option was set.
+                 *
+                 * @return True if the dft file option was set.
+                 */
+                bool isDftFileSet() const;
+                
+                /*!
+                 * Retrieves the name of the file that contains the dft specification.
+                 *
+                 * @return The name of the file that contains the dft specification.
+                 */
+                std::string getDftFilename() const;
+                
+                //expectedtime, probability, timebound, prob
+                //min, max
+                
+                /*!
+                 * Retrieves whether the option to use symmetry reduction is set.
+                 *
+                 * @return True iff the option was set.
+                 */
+                bool useSymmetryReduction() const;
+                
+                /*!
+                 * Retrieves whether the option to use modularisation is set.
+                 *
+                 * @return True iff the option was set.
+                 */
+                bool useModularisation() const;
+                
+                /*!
+                 * Retrieves whether the option to disable Dont Care propagation is set.
+                 *
+                 * @return True iff the option was set.
+                 */
+                bool isDisableDC() const;
+
+                /*!
+                 * Retrieves whether the property expected time should be used.
+                 *
+                 * @return True iff the option was set.
+                 */
+                bool usePropExpectedTime() const;
+                
+                /*!
+                 * Retrieves whether the property probability should be used.
+                 *
+                 * @return True iff the option was set.
+                 */
+                bool usePropProbability() const;
+                
+                /*!
+                 * Retrieves whether the property timebound should be used.
+                 *
+                 * @return True iff the option was set.
+                 */
+                bool usePropTimebound() const;
+                
+                /*!
+                 * Retrieves whether the minimal value should be computed for non-determinism.
+                 *
+                 * @return True iff the option was set.
+                 */
+                bool isComputeMinimalValue() const;
+
+                /*!
+                 * Retrieves whether the maximal value should be computed for non-determinism.
+                 *
+                 * @return True iff the option was set.
+                 */
+                bool isComputeMaximalValue() const;
+                
+                /*!
+                 * Retrieves the timebound for the timebound property.
+                 *
+                 * @return The timebound.
+                 */
+                double getPropTimebound() const;
+                
+                bool check() const override;
+                void finalize() override;
+
+                // The name of the module.
+                static const std::string moduleName;
+
+            private:
+               // Define the string names of the options as constants.
+                static const std::string dftFileOptionName;
+                static const std::string dftFileOptionShortName;
+                static const std::string symmetryReductionOptionName;
+                static const std::string symmetryReductionOptionShortName;
+                static const std::string modularisationOptionName;
+                static const std::string disableDCOptionName;
+                static const std::string propExpectedTimeOptionName;
+                static const std::string propExpectedTimeOptionShortName;
+                static const std::string propProbabilityOptionName;
+                static const std::string propTimeBoundOptionName;
+                static const std::string minValueOptionName;
+                static const std::string maxValueOptionName;
+                
+            };
+
+        } // namespace modules
+    } // namespace settings
+} // namespace storm
+
+#endif /* STORM_SETTINGS_MODULES_DFTSETTINGS_H_ */

src/storm-dyftee.cpp

@@ -2,8 +2,27 @@
 #include "utility/initialize.h"
 #include "utility/storm.h"
 #include "modelchecker/DFTAnalyser.h"
+#include "src/cli/cli.h"
+#include "src/exceptions/BaseException.h"
+#include "src/utility/macros.h"
 #include <boost/lexical_cast.hpp>
 
+#include "src/settings/modules/GeneralSettings.h"
+#include "src/settings/modules/DFTSettings.h"
+#include "src/settings/modules/MarkovChainSettings.h"
+#include "src/settings/modules/DebugSettings.h"
+//#include "src/settings/modules/CounterexampleGeneratorSettings.h"
+//#include "src/settings/modules/CuddSettings.h"
+//#include "src/settings/modules/SylvanSettings.h"
+#include "src/settings/modules/GmmxxEquationSolverSettings.h"
+#include "src/settings/modules/NativeEquationSolverSettings.h"
+//#include "src/settings/modules/BisimulationSettings.h"
+//#include "src/settings/modules/GlpkSettings.h"
+//#include "src/settings/modules/GurobiSettings.h"
+//#include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h"
+//#include "src/settings/modules/ParametricSettings.h"
+#include "src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h"
+
 /*!
  * Load DFT from filename, build corresponding Model and check against given property.
  *
@@ -12,8 +31,7 @@
  */
 template <typename ValueType>
 void analyzeDFT(std::string filename, std::string property, bool symred = false, bool allowModularisation = false, bool enableDC = true) {
-    storm::settings::SettingsManager& manager = storm::settings::mutableManager();
-    manager.setFromString("");
+    std::cout << "Running DFT analysis on file " << filename << " with property " << property << std::endl;
 
     storm::parser::DFTGalileoParser<ValueType> parser;
     storm::storage::DFT<ValueType> dft = parser.parseDFT(filename);
@@ -27,6 +45,30 @@ void analyzeDFT(std::string filename, std::string property, bool symred = false,
     analyser.printResult();
 }
 
+/*!
+ * Initialize the settings manager.
+ */
+void initializeSettings() {
+    storm::settings::mutableManager().setName("StoRM-DyFTeE", "storm-dft");
+    
+    // Register all known settings modules.
+    storm::settings::addModule<storm::settings::modules::GeneralSettings>();
+    storm::settings::addModule<storm::settings::modules::DFTSettings>();
+    storm::settings::addModule<storm::settings::modules::MarkovChainSettings>();
+    storm::settings::addModule<storm::settings::modules::DebugSettings>();
+    //storm::settings::addModule<storm::settings::modules::CounterexampleGeneratorSettings>();
+    //storm::settings::addModule<storm::settings::modules::CuddSettings>();
+    //storm::settings::addModule<storm::settings::modules::SylvanSettings>();
+    storm::settings::addModule<storm::settings::modules::GmmxxEquationSolverSettings>();
+    storm::settings::addModule<storm::settings::modules::NativeEquationSolverSettings>();
+    //storm::settings::addModule<storm::settings::modules::BisimulationSettings>();
+    //storm::settings::addModule<storm::settings::modules::GlpkSettings>();
+    //storm::settings::addModule<storm::settings::modules::GurobiSettings>();
+    //storm::settings::addModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>();
+    //storm::settings::addModule<storm::settings::modules::ParametricSettings>();
+    storm::settings::addModule<storm::settings::modules::SparseDtmcEliminationModelCheckerSettings>();
+}
+
 /*!
  * Entry point for the DyFTeE backend.
  *
@@ -34,91 +76,81 @@ void analyzeDFT(std::string filename, std::string property, bool symred = false,
  * @param argv The argv argument of main().
  * @return Return code, 0 if successfull, not 0 otherwise.
  */
-int main(int argc, char** argv) {
-    if(argc < 2) {
-        std::cout << "Storm-DyFTeE should be called with a filename as argument." << std::endl;
-        std::cout << "./storm-dft <filename> <--prop pctl-formula> <--parametric>" << std::endl;
-        return 1;
-    }
-
-    // Parse cli arguments
-    bool parametric = false;
-    bool symred = false;
-    bool minimal = true;
-    bool allowModular = true;
-    bool enableModularisation = false;
-    bool disableDC = false;
-    std::string filename = argv[1];
-    std::string operatorType = "";
-    std::string targetFormula = "";
-    std::string pctlFormula = "";
-    for (int i = 2; i < argc; ++i) {
-        std::string option = argv[i];
-        if (option == "--parametric") {
-            parametric = true;
-        } else if (option == "--expectedtime") {
-            assert(targetFormula.empty());
+int main(const int argc, const char** argv) {
+    try {
+        storm::utility::setUp();
+        storm::cli::printHeader("StoRM-DyFTeE", argc, argv);
+        initializeSettings();
+        
+        bool optionsCorrect = storm::cli::parseOptions(argc, argv);
+        if (!optionsCorrect) {
+            return -1;
+        }
+        
+        storm::settings::modules::DFTSettings const& dftSettings = storm::settings::getModule<storm::settings::modules::DFTSettings>();
+        storm::settings::modules::GeneralSettings const& generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
+        if (!dftSettings.isDftFileSet()) {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
+        }
+        
+        // Set min or max
+        bool minimal = true;
+        if (dftSettings.isComputeMaximalValue()) {
+            assert(!dftSettings.isComputeMinimalValue());
+            minimal = false;
+        }
+        
+        // Construct pctlFormula
+        std::string pctlFormula = "";
+        bool allowModular = true;
+        std::string operatorType = "";
+        std::string targetFormula = "";
+        
+        if (generalSettings.isPropertySet()) {
+            STORM_LOG_THROW(!dftSettings.usePropExpectedTime() && !dftSettings.usePropProbability() && !dftSettings.usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given.");
+            pctlFormula = generalSettings.getProperty();
+        } else if (dftSettings.usePropExpectedTime()) {
+            STORM_LOG_THROW(!dftSettings.usePropProbability() && !dftSettings.usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given.");
             operatorType = "T";
             targetFormula = "F \"failed\"";
             allowModular = false;
-        } else if (option == "--probability") {
-            assert(targetFormula.empty());
+        } else if (dftSettings.usePropProbability()) {
+            STORM_LOG_THROW(!dftSettings.usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given.");
             operatorType = "P";;
             targetFormula = "F \"failed\"";
-        } else if (option == "--timebound") {
-            assert(targetFormula.empty());
-            ++i;
-            assert(i < argc);
-            double timeBound;
-            try {
-                timeBound = boost::lexical_cast<double>(argv[i]);
-            } catch (boost::bad_lexical_cast e) {
-                std::cerr << "The time bound '" << argv[i] << "' is not valid." << std::endl;
-                return 2;
-            }
+        } else {
+            STORM_LOG_THROW(dftSettings.usePropTimebound(), storm::exceptions::InvalidSettingsException, "No property given.");
             std::stringstream stream;
-            stream << "F<=" << timeBound << " \"failed\"";
+            stream << "F<=" << dftSettings.getPropTimebound() << " \"failed\"";
             operatorType = "P";
             targetFormula = stream.str();
-        } else if (option == "--trace") {
-            STORM_GLOBAL_LOGLEVEL_TRACE();
-        } else if (option == "--debug") {
-            STORM_GLOBAL_LOGLEVEL_DEBUG();
-        } else if (option == "--prop") {
+        }
+        
+        if (!targetFormula.empty()) {
             assert(pctlFormula.empty());
-            ++i;
-            assert(i < argc);
-            pctlFormula = argv[i];
-        } else if (option == "--symred") {
-            symred = true;
-        } else if (option == "--modularisation") {
-            enableModularisation = true;
-        } else if (option == "--disabledc") {
-            disableDC = true;
-        } else if (option == "--min") {
-            minimal = true;
-        } else if (option == "--max") {
-            minimal = false;
-        } else {
-            std::cout << "Option '" << option << "' not recognized." << std::endl;
-            return 1;
+            pctlFormula = operatorType + (minimal ? "min" : "max") + "=?[" + targetFormula + "]";
         }
-    }
-    
-    // Construct pctlFormula
-    if (!targetFormula.empty()) {
-        assert(pctlFormula.empty());
-        pctlFormula = operatorType + (minimal ? "min" : "max") + "=?[" + targetFormula + "]";
-    }
-    
-    assert(!pctlFormula.empty());
-
-    storm::utility::setUp();
-    std::cout << "Running " << (parametric ? "parametric " : "") << "DFT analysis on file " << filename << " with property " << pctlFormula << std::endl;
+        
+        assert(!pctlFormula.empty());
 
-    if (parametric) {
-        analyzeDFT<storm::RationalFunction>(filename, pctlFormula, symred, allowModular && enableModularisation, !disableDC );
-    } else {
-        analyzeDFT<double>(filename, pctlFormula, symred, allowModular && enableModularisation, !disableDC);
+        bool parametric = false;
+#ifdef STORM_HAVE_CARL
+        parametric = generalSettings.isParametricSet();
+#endif
+        
+        // From this point on we are ready to carry out the actual computations.
+        if (parametric) {
+            analyzeDFT<storm::RationalFunction>(dftSettings.getDftFilename(), pctlFormula, dftSettings.useSymmetryReduction(), allowModular && dftSettings.useModularisation(), !dftSettings.isDisableDC() );
+        } else {
+            analyzeDFT<double>(dftSettings.getDftFilename(), pctlFormula, dftSettings.useSymmetryReduction(), allowModular && dftSettings.useModularisation(), !dftSettings.isDisableDC());
+        }
+        
+        // All operations have now been performed, so we clean up everything and terminate.
+        storm::utility::cleanUp();
+        return 0;
+    } catch (storm::exceptions::BaseException const& exception) {
+        STORM_LOG_ERROR("An exception caused StoRM-DyFTeE to terminate. The message of the exception is: " << exception.what());
+    } catch (std::exception const& exception) {
+        STORM_LOG_ERROR("An unexpected exception occurred and caused StoRM-DyFTeE to terminate. The message of this exception is: " << exception.what());
     }
 }