From 8a74be1b72f429c0959aa351578438792f86d9ed Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Wed, 11 Oct 2017 17:57:15 +0200
Subject: [PATCH 1/7] Refactored DFT settings

---
 src/storm-dft-cli/storm-dft.cpp               | 124 ++++--------
 .../builder/ExplicitDFTModelBuilder.cpp       |   2 -
 .../builder/ExplicitDFTModelBuilderApprox.cpp |   4 +-
 .../generator/DftNextStateGenerator.cpp       |   4 +-
 .../modelchecker/dft/DFTModelChecker.cpp      |   4 +-
 src/storm-dft/settings/DftSettings.cpp        |  51 +++++
 src/storm-dft/settings/DftSettings.h          |  11 +
 .../settings/modules/DFTSettings.cpp          | 189 ------------------
 .../settings/modules/DftIOSettings.cpp        | 123 ++++++++++++
 .../{DFTSettings.h => DftIOSettings.h}        |  80 +-------
 .../settings/modules/FaultTreeSettings.cpp    |  93 +++++++++
 .../settings/modules/FaultTreeSettings.h      | 104 ++++++++++
 12 files changed, 432 insertions(+), 357 deletions(-)
 create mode 100644 src/storm-dft/settings/DftSettings.cpp
 create mode 100644 src/storm-dft/settings/DftSettings.h
 delete mode 100644 src/storm-dft/settings/modules/DFTSettings.cpp
 create mode 100644 src/storm-dft/settings/modules/DftIOSettings.cpp
 rename src/storm-dft/settings/modules/{DFTSettings.h => DftIOSettings.h} (63%)
 create mode 100644 src/storm-dft/settings/modules/FaultTreeSettings.cpp
 create mode 100644 src/storm-dft/settings/modules/FaultTreeSettings.h

diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp
index b6fb0c751..3e69fb217 100644
--- a/src/storm-dft-cli/storm-dft.cpp
+++ b/src/storm-dft-cli/storm-dft.cpp
@@ -1,20 +1,14 @@
-#include "storm/logic/Formula.h"
-#include "storm/utility/initialize.h"
-#include "storm/api/storm.h"
-#include "storm-cli-utilities/cli.h"
-#include "storm/exceptions/BaseException.h"
-
-#include "storm/logic/Formula.h"
+#include "storm-dft/settings/DftSettings.h"
 
+#include "storm-dft/settings/modules/DftIOSettings.h"
+#include "storm-dft/settings/modules/FaultTreeSettings.h"
 #include "storm/settings/modules/IOSettings.h"
-#include "storm/settings/modules/CoreSettings.h"
-#include "storm/settings/modules/DebugSettings.h"
-#include "storm/settings/modules/GmmxxEquationSolverSettings.h"
-#include "storm/settings/modules/MinMaxEquationSolverSettings.h"
-#include "storm/settings/modules/NativeEquationSolverSettings.h"
-#include "storm/settings/modules/EliminationSettings.h"
 #include "storm/settings/modules/ResourceSettings.h"
 
+#include "storm/utility/initialize.h"
+#include "storm/api/storm.h"
+#include "storm-cli-utilities/cli.h"
+
 #include "storm-dft/parser/DFTGalileoParser.h"
 #include "storm-dft/parser/DFTJsonParser.h"
 #include "storm-dft/modelchecker/dft/DFTModelChecker.h"
@@ -22,12 +16,8 @@
 #include "storm-dft/transformations/DftToGspnTransformator.h"
 #include "storm-dft/storage/dft/DftJsonExporter.h"
 
-#include "storm-dft/settings/modules/DFTSettings.h"
-
 #include "storm-gspn/storage/gspn/GSPN.h"
 #include "storm-gspn/storm-gspn.h"
-#include "storm/settings/modules/GSPNSettings.h"
-#include "storm/settings/modules/GSPNExportSettings.h"
 
 #include <boost/lexical_cast.hpp>
 #include <memory>
@@ -44,18 +34,18 @@
  */
 template <typename ValueType>
 void analyzeDFT(std::vector<std::string> const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError) {
-    storm::settings::modules::DFTSettings const& dftSettings = storm::settings::getModule<storm::settings::modules::DFTSettings>();
+    storm::settings::modules::DftIOSettings const& dftIOSettings = storm::settings::getModule<storm::settings::modules::DftIOSettings>();
     std::shared_ptr<storm::storage::DFT<ValueType>> dft;
 
     // Build DFT from given file.
-    if (dftSettings.isDftJsonFileSet()) {
+    if (dftIOSettings.isDftJsonFileSet()) {
         storm::parser::DFTJsonParser<ValueType> parser;
-        std::cout << "Loading DFT from file " << dftSettings.getDftJsonFilename() << std::endl;
-        dft = std::make_shared<storm::storage::DFT<ValueType>>(parser.parseJson(dftSettings.getDftJsonFilename()));
+        std::cout << "Loading DFT from file " << dftIOSettings.getDftJsonFilename() << std::endl;
+        dft = std::make_shared<storm::storage::DFT<ValueType>>(parser.parseJson(dftIOSettings.getDftJsonFilename()));
     } else {
         storm::parser::DFTGalileoParser<ValueType> parser;
-        std::cout << "Loading DFT from file " << dftSettings.getDftFilename() << std::endl;
-        dft = std::make_shared<storm::storage::DFT<ValueType>>(parser.parseDFT(dftSettings.getDftFilename()));
+        std::cout << "Loading DFT from file " << dftIOSettings.getDftFilename() << std::endl;
+        dft = std::make_shared<storm::storage::DFT<ValueType>>(parser.parseDFT(dftIOSettings.getDftFilename()));
     }
 
     // Build properties
@@ -91,72 +81,39 @@ void analyzeWithSMT(std::string filename) {
     //std::cout << "SMT result: " << sat << std::endl;
 }
 
-
-/*!
- * 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::CoreSettings>();
-    storm::settings::addModule<storm::settings::modules::DebugSettings>();
-    storm::settings::addModule<storm::settings::modules::IOSettings>();
-    //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::MinMaxEquationSolverSettings>();
-    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::EliminationSettings>();
-    storm::settings::addModule<storm::settings::modules::ResourceSettings>();
-    
-    // For translation into JANI via GSPN.
-    storm::settings::addModule<storm::settings::modules::GSPNSettings>();
-    storm::settings::addModule<storm::settings::modules::GSPNExportSettings>();
-    storm::settings::addModule<storm::settings::modules::JaniExportSettings>();
-}
-
-
 void processOptions() {
         // Start by setting some urgent options (log levels, resources, etc.)
         storm::cli::setUrgentOptions();
 
         storm::cli::processOptions();
         
-        storm::settings::modules::DFTSettings const& dftSettings = storm::settings::getModule<storm::settings::modules::DFTSettings>();
+        storm::settings::modules::DftIOSettings const& dftIOSettings = storm::settings::getModule<storm::settings::modules::DftIOSettings>();
+        storm::settings::modules::FaultTreeSettings const& faultTreeSettings = storm::settings::getModule<storm::settings::modules::FaultTreeSettings>();
         storm::settings::modules::GeneralSettings const& generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
         storm::settings::modules::IOSettings const& ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
-        if (!dftSettings.isDftFileSet() && !dftSettings.isDftJsonFileSet()) {
+        if (!dftIOSettings.isDftFileSet() && !dftIOSettings.isDftJsonFileSet()) {
             STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
         }
 
-        if (dftSettings.isExportToJson()) {
-            STORM_LOG_THROW(dftSettings.isDftFileSet(), storm::exceptions::InvalidSettingsException, "No input model in Galileo format given.");
+        if (dftIOSettings.isExportToJson()) {
+            STORM_LOG_THROW(dftIOSettings.isDftFileSet(), storm::exceptions::InvalidSettingsException, "No input model in Galileo format given.");
             storm::parser::DFTGalileoParser<double> parser;
-            storm::storage::DFT<double> dft = parser.parseDFT(dftSettings.getDftFilename());
+            storm::storage::DFT<double> dft = parser.parseDFT(dftIOSettings.getDftFilename());
             // Export to json
-            storm::storage::DftJsonExporter<double>::toFile(dft, dftSettings.getExportJsonFilename());
+            storm::storage::DftJsonExporter<double>::toFile(dft, dftIOSettings.getExportJsonFilename());
             storm::utility::cleanUp();
             return;
         }
 
         
-        if (dftSettings.isTransformToGspn()) {
+        if (dftIOSettings.isTransformToGspn()) {
             std::shared_ptr<storm::storage::DFT<double>> dft;
-            if (dftSettings.isDftJsonFileSet()) {
+            if (dftIOSettings.isDftJsonFileSet()) {
                 storm::parser::DFTJsonParser<double> parser;
-                dft = std::make_shared<storm::storage::DFT<double>>(parser.parseJson(dftSettings.getDftJsonFilename()));
+                dft = std::make_shared<storm::storage::DFT<double>>(parser.parseJson(dftIOSettings.getDftJsonFilename()));
             } else {
                 storm::parser::DFTGalileoParser<double> parser(true, false);
-                dft = std::make_shared<storm::storage::DFT<double>>(parser.parseDFT(dftSettings.getDftFilename()));
+                dft = std::make_shared<storm::storage::DFT<double>>(parser.parseDFT(dftIOSettings.getDftFilename()));
             }
             storm::transformations::dft::DftToGspnTransformator<double> gspnTransformator(*dft);
             gspnTransformator.transform();
@@ -196,12 +153,12 @@ void processOptions() {
 #endif
         
 #ifdef STORM_HAVE_Z3
-        if (dftSettings.solveWithSMT()) {
+        if (faultTreeSettings.solveWithSMT()) {
             // Solve with SMT
             if (parametric) {
             //    analyzeWithSMT<storm::RationalFunction>(dftSettings.getDftFilename());
             } else {
-                analyzeWithSMT<double>(dftSettings.getDftFilename());
+                analyzeWithSMT<double>(dftIOSettings.getDftFilename());
             }
             storm::utility::cleanUp();
             return;
@@ -210,8 +167,8 @@ void processOptions() {
         
         // Set min or max
         std::string optimizationDirection = "min";
-        if (dftSettings.isComputeMaximalValue()) {
-            STORM_LOG_THROW(!dftSettings.isComputeMinimalValue(), storm::exceptions::InvalidSettingsException, "Cannot compute minimal and maximal values at the same time.");
+        if (dftIOSettings.isComputeMaximalValue()) {
+            STORM_LOG_THROW(!dftIOSettings.isComputeMinimalValue(), storm::exceptions::InvalidSettingsException, "Cannot compute minimal and maximal values at the same time.");
             optimizationDirection = "max";
         }
         
@@ -221,19 +178,19 @@ void processOptions() {
         if (ioSettings.isPropertySet()) {
             properties.push_back(ioSettings.getProperty());
         }
-        if (dftSettings.usePropExpectedTime()) {
+        if (dftIOSettings.usePropExpectedTime()) {
             properties.push_back("T" + optimizationDirection + "=? [F \"failed\"]");
         }
-        if (dftSettings.usePropProbability()) {
+        if (dftIOSettings.usePropProbability()) {
             properties.push_back("P" + optimizationDirection + "=? [F \"failed\"]");
         }
-        if (dftSettings.usePropTimebound()) {
+        if (dftIOSettings.usePropTimebound()) {
             std::stringstream stream;
-            stream << "P" << optimizationDirection << "=? [F<=" << dftSettings.getPropTimebound() << " \"failed\"]";
+            stream << "P" << optimizationDirection << "=? [F<=" << dftIOSettings.getPropTimebound() << " \"failed\"]";
             properties.push_back(stream.str());
         }
-        if (dftSettings.usePropTimepoints()) {
-            for (double timepoint : dftSettings.getPropTimepoints()) {
+        if (dftIOSettings.usePropTimepoints()) {
+            for (double timepoint : dftIOSettings.getPropTimepoints()) {
                 std::stringstream stream;
                 stream << "P" << optimizationDirection << "=? [F<=" << timepoint << " \"failed\"]";
                 properties.push_back(stream.str());
@@ -246,19 +203,19 @@ void processOptions() {
 
         // Set possible approximation error
         double approximationError = 0.0;
-        if (dftSettings.isApproximationErrorSet()) {
-            approximationError = dftSettings.getApproximationError();
+        if (faultTreeSettings.isApproximationErrorSet()) {
+            approximationError = faultTreeSettings.getApproximationError();
         }
 
         // From this point on we are ready to carry out the actual computations.
         if (parametric) {
 #ifdef STORM_HAVE_CARL
-            analyzeDFT<storm::RationalFunction>(properties, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError);
+            analyzeDFT<storm::RationalFunction>(properties, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), approximationError);
 #else
             STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameters are not supported in this build.");
 #endif
         } else {
-            analyzeDFT<double>(properties, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError);
+            analyzeDFT<double>(properties, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), approximationError);
         }
 }
 
@@ -275,9 +232,8 @@ void processOptions() {
 int main(const int argc, const char** argv) {
     try {
         storm::utility::setUp();
-        storm::cli::printHeader("Storm-DyFTeE", argc, argv);
-        //storm::settings::initializeParsSettings("Storm-pars", "storm-pars");
-        initializeSettings();
+        storm::cli::printHeader("Storm-dft", argc, argv);
+        storm::settings::initializeDftSettings("Storm-dft", "storm-dft");
 
         storm::utility::Stopwatch totalTimer(true);
         if (!storm::cli::parseOptions(argc, argv)) {
diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
index 4a29b0652..5ef6bd07e 100644
--- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
+++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
@@ -9,8 +9,6 @@
 #include "storm/exceptions/UnexpectedException.h"
 #include "storm/settings/SettingsManager.h"
 
-#include "storm-dft/settings/modules/DFTSettings.h"
-
 
 namespace storm {
     namespace builder {
diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
index 0c7d69628..f035b0a55 100644
--- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
+++ b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
@@ -10,7 +10,7 @@
 #include "storm/exceptions/UnexpectedException.h"
 #include "storm/settings/SettingsManager.h"
 #include "storm/logic/AtomicLabelFormula.h"
-#include "storm-dft/settings/modules/DFTSettings.h"
+#include "storm-dft/settings/modules/FaultTreeSettings.h"
 
 
 namespace storm {
@@ -55,7 +55,7 @@ namespace storm {
                 dft(dft),
                 stateGenerationInfo(std::make_shared<storm::storage::DFTStateGenerationInfo>(dft.buildStateGenerationInfo(symmetries))),
                 enableDC(enableDC),
-                usedHeuristic(storm::settings::getModule<storm::settings::modules::DFTSettings>().getApproximationHeuristic()),
+                usedHeuristic(storm::settings::getModule<storm::settings::modules::FaultTreeSettings>().getApproximationHeuristic()),
                 generator(dft, *stateGenerationInfo, enableDC, mergeFailedStates),
                 matrixBuilder(!generator.isDeterministicModel()),
                 stateStorage(((dft.stateVectorSize() / 64) + 1) * 64),
diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp
index 7b86d1faa..0002cd6a3 100644
--- a/src/storm-dft/generator/DftNextStateGenerator.cpp
+++ b/src/storm-dft/generator/DftNextStateGenerator.cpp
@@ -4,7 +4,7 @@
 #include "storm/utility/macros.h"
 #include "storm/exceptions/NotImplementedException.h"
 #include "storm/settings/SettingsManager.h"
-#include "storm-dft/settings/modules/DFTSettings.h"
+#include "storm-dft/settings/modules/FaultTreeSettings.h"
 
 namespace storm {
     namespace generator {
@@ -71,7 +71,7 @@ namespace storm {
 
             // Let BE fail
             while (currentFailable < failableCount) {
-                if (storm::settings::getModule<storm::settings::modules::DFTSettings>().isTakeFirstDependency() && hasDependencies && currentFailable > 0) {
+                if (storm::settings::getModule<storm::settings::modules::FaultTreeSettings>().isTakeFirstDependency() && hasDependencies && currentFailable > 0) {
                     // We discard further exploration as we already chose one dependent event
                     break;
                 }
diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
index d6b7e9138..45d97baa6 100644
--- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
+++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
@@ -8,7 +8,7 @@
 #include "storm-dft/builder/ExplicitDFTModelBuilder.h"
 #include "storm-dft/builder/ExplicitDFTModelBuilderApprox.h"
 #include "storm-dft/storage/dft/DFTIsomorphism.h"
-#include "storm-dft/settings/modules/DFTSettings.h"
+#include "storm-dft/settings/modules/FaultTreeSettings.h"
 
 
 namespace storm {
@@ -344,7 +344,7 @@ namespace storm {
                 STORM_LOG_INFO("Building Model...");
                 std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
                 // TODO Matthias: use only one builder if everything works again
-                if (storm::settings::getModule<storm::settings::modules::DFTSettings>().isApproximationErrorSet()) {
+                if (storm::settings::getModule<storm::settings::modules::FaultTreeSettings>().isApproximationErrorSet()) {
                     storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(dft, symmetries, enableDC);
                     typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions(properties, storm::settings::getModule<storm::settings::modules::IOSettings>().isExportExplicitSet());
                     builder.buildModel(labeloptions, 0, 0.0);
diff --git a/src/storm-dft/settings/DftSettings.cpp b/src/storm-dft/settings/DftSettings.cpp
new file mode 100644
index 000000000..ce48c6fd9
--- /dev/null
+++ b/src/storm-dft/settings/DftSettings.cpp
@@ -0,0 +1,51 @@
+#include "storm-dft/settings/DftSettings.h"
+
+#include "storm-dft/settings/modules/DftIOSettings.h"
+#include "storm-dft/settings/modules/FaultTreeSettings.h"
+
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/GeneralSettings.h"
+#include "storm/settings/modules/CoreSettings.h"
+#include "storm/settings/modules/IOSettings.h"
+#include "storm/settings/modules/DebugSettings.h"
+#include "storm/settings/modules/EigenEquationSolverSettings.h"
+#include "storm/settings/modules/GmmxxEquationSolverSettings.h"
+#include "storm/settings/modules/NativeEquationSolverSettings.h"
+#include "storm/settings/modules/EliminationSettings.h"
+#include "storm/settings/modules/MinMaxEquationSolverSettings.h"
+#include "storm/settings/modules/BisimulationSettings.h"
+#include "storm/settings/modules/ResourceSettings.h"
+#include "storm/settings/modules/JaniExportSettings.h"
+#include "storm/settings/modules/GSPNSettings.h"
+#include "storm/settings/modules/GSPNExportSettings.h"
+
+
+namespace storm {
+    namespace settings {
+        void initializeDftSettings(std::string const& name, std::string const& executableName) {
+            storm::settings::mutableManager().setName(name, executableName);
+        
+            // Register relevant settings modules.
+            storm::settings::addModule<storm::settings::modules::GeneralSettings>();
+            storm::settings::addModule<storm::settings::modules::DftIOSettings>();
+            storm::settings::addModule<storm::settings::modules::FaultTreeSettings>();
+            storm::settings::addModule<storm::settings::modules::IOSettings>();
+            storm::settings::addModule<storm::settings::modules::CoreSettings>();
+
+            storm::settings::addModule<storm::settings::modules::DebugSettings>();
+            storm::settings::addModule<storm::settings::modules::NativeEquationSolverSettings>();
+            storm::settings::addModule<storm::settings::modules::GmmxxEquationSolverSettings>();
+            storm::settings::addModule<storm::settings::modules::EigenEquationSolverSettings>();
+            storm::settings::addModule<storm::settings::modules::EliminationSettings>();
+            storm::settings::addModule<storm::settings::modules::MinMaxEquationSolverSettings>();
+            // storm::settings::addModule<storm::settings::modules::BisimulationSettings>();
+            storm::settings::addModule<storm::settings::modules::ResourceSettings>();
+
+            // For translation into JANI via GSPN.
+            storm::settings::addModule<storm::settings::modules::JaniExportSettings>();
+            storm::settings::addModule<storm::settings::modules::GSPNSettings>();
+            storm::settings::addModule<storm::settings::modules::GSPNExportSettings>();
+        }
+    
+    }
+}
diff --git a/src/storm-dft/settings/DftSettings.h b/src/storm-dft/settings/DftSettings.h
new file mode 100644
index 000000000..8f67ec0b7
--- /dev/null
+++ b/src/storm-dft/settings/DftSettings.h
@@ -0,0 +1,11 @@
+#pragma once
+
+#include <string>
+
+namespace storm {
+    namespace settings {
+        
+        void initializeDftSettings(std::string const& name, std::string const& executableName);
+        
+    }
+}
diff --git a/src/storm-dft/settings/modules/DFTSettings.cpp b/src/storm-dft/settings/modules/DFTSettings.cpp
deleted file mode 100644
index 1a8d59d70..000000000
--- a/src/storm-dft/settings/modules/DFTSettings.cpp
+++ /dev/null
@@ -1,189 +0,0 @@
-#include "DFTSettings.h"
-
-#include "storm/settings/SettingsManager.h"
-#include "storm/settings/SettingMemento.h"
-#include "storm/settings/Option.h"
-#include "storm/settings/OptionBuilder.h"
-#include "storm/settings/ArgumentBuilder.h"
-#include "storm/settings/Argument.h"
-
-#include "storm/exceptions/InvalidSettingsException.h"
-#include "storm/exceptions/IllegalArgumentValueException.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::dftJsonFileOptionName = "dftfile-json";
-            const std::string DFTSettings::dftJsonFileOptionShortName = "dftjson";
-            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::approximationErrorOptionName = "approximation";
-            const std::string DFTSettings::approximationErrorOptionShortName = "approx";
-            const std::string DFTSettings::approximationHeuristicOptionName = "approximationheuristic";
-            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::propTimepointsOptionName = "timepoints";
-            const std::string DFTSettings::minValueOptionName = "min";
-            const std::string DFTSettings::maxValueOptionName = "max";
-            const std::string DFTSettings::firstDependencyOptionName = "firstdep";
-            const std::string DFTSettings::transformToGspnOptionName = "gspn";
-            const std::string DFTSettings::exportToJsonOptionName = "export-json";
-#ifdef STORM_HAVE_Z3
-            const std::string DFTSettings::solveWithSmtOptionName = "smt";
-#endif
-
-            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.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, dftJsonFileOptionName, false, "Parses the model given in the Cytoscape JSON format.").setShortName(dftJsonFileOptionShortName)
-                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file from which to read the DFT model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).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, firstDependencyOptionName, false, "Avoid non-determinism by always taking the first possible dependency.").build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, approximationErrorOptionName, false, "Approximation error allowed.").setShortName(approximationErrorOptionShortName).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("error", "The relative approximation error to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, approximationHeuristicOptionName, false, "Set the heuristic used for approximation.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("heuristic", "Sets which heuristic is used for approximation. Must be in {depth, probability}. Default is").setDefaultValueString("depth").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator({"depth", "rateratio"})).build()).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.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterValidator(0.0)).build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, propTimepointsOptionName, false, "Compute probability of system failure up to given timebound for a set of given timepoints [starttime, starttime+inc, starttime+2inc, ... ,endtime]").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("starttime", "The timebound to start from.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("endtime", "The timebound to end with.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("inc", "The value to increment with to get the next timepoint.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(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());
-#ifdef STORM_HAVE_Z3
-                this->addOption(storm::settings::OptionBuilder(moduleName, solveWithSmtOptionName, true, "Solve the DFT with SMT.").build());
-#endif
-                this->addOption(storm::settings::OptionBuilder(moduleName, transformToGspnOptionName, false, "Transform DFT to GSPN.").build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, exportToJsonOptionName, false,  "Export the model to the Cytoscape JSON format.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file to export to.").build()).build());
-            }
-
-            bool DFTSettings::isDftFileSet() const {
-                return this->getOption(dftFileOptionName).getHasOptionBeenSet();
-            }
-            
-            std::string DFTSettings::getDftFilename() const {
-                return this->getOption(dftFileOptionName).getArgumentByName("filename").getValueAsString();
-            }
-
-            bool DFTSettings::isDftJsonFileSet() const {
-                return this->getOption(dftJsonFileOptionName).getHasOptionBeenSet();
-            }
-
-            std::string DFTSettings::getDftJsonFilename() const {
-                return this->getOption(dftJsonFileOptionName).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::isApproximationErrorSet() const {
-                return this->getOption(approximationErrorOptionName).getHasOptionBeenSet();
-            }
-
-            double DFTSettings::getApproximationError() const {
-                return this->getOption(approximationErrorOptionName).getArgumentByName("error").getValueAsDouble();
-            }
-
-            storm::builder::ApproximationHeuristic DFTSettings::getApproximationHeuristic() const {
-                if (!isApproximationErrorSet() || getApproximationError() == 0.0) {
-                    // No approximation is done
-                    return storm::builder::ApproximationHeuristic::NONE;
-                }
-                std::string heuristicAsString = this->getOption(approximationHeuristicOptionName).getArgumentByName("heuristic").getValueAsString();
-                if (heuristicAsString == "depth") {
-                    return storm::builder::ApproximationHeuristic::DEPTH;
-                } else if (heuristicAsString == "probability") {
-                    return storm::builder::ApproximationHeuristic::PROBABILITY;
-                }
-                STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal value '" << heuristicAsString << "' set as heuristic for approximation.");
-            }
-
-            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::usePropTimepoints() const {
-                return this->getOption(propTimepointsOptionName).getHasOptionBeenSet();
-            }
-
-            std::vector<double> DFTSettings::getPropTimepoints() const {
-                double starttime = this->getOption(propTimepointsOptionName).getArgumentByName("starttime").getValueAsDouble();
-                double endtime = this->getOption(propTimepointsOptionName).getArgumentByName("endtime").getValueAsDouble();
-                double inc = this->getOption(propTimepointsOptionName).getArgumentByName("inc").getValueAsDouble();
-                std::vector<double> timepoints;
-                for (double time = starttime; time <= endtime; time += inc) {
-                    timepoints.push_back(time);
-                }
-                return timepoints;
-            }
-
-            bool DFTSettings::isComputeMinimalValue() const {
-                return this->getOption(minValueOptionName).getHasOptionBeenSet();
-            }
-            
-            bool DFTSettings::isComputeMaximalValue() const {
-                return this->getOption(maxValueOptionName).getHasOptionBeenSet();
-            }
-            
-            bool DFTSettings::isTakeFirstDependency() const {
-                return this->getOption(firstDependencyOptionName).getHasOptionBeenSet();
-            }
-
-#ifdef STORM_HAVE_Z3
-            bool DFTSettings::solveWithSMT() const {
-                return this->getOption(solveWithSmtOptionName).getHasOptionBeenSet();
-            }
-#endif
-            
-            bool DFTSettings::isTransformToGspn() const {
-                return this->getOption(transformToGspnOptionName).getHasOptionBeenSet();
-            }
-
-            bool DFTSettings::isExportToJson() const {
-                return this->getOption(exportToJsonOptionName).getHasOptionBeenSet();
-            }
-
-            std::string DFTSettings::getExportJsonFilename() const {
-                return this->getOption(exportToJsonOptionName).getArgumentByName("filename").getValueAsString();
-            }
-
-            void DFTSettings::finalize() {
-            }
-
-            bool DFTSettings::check() const {
-                // 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
diff --git a/src/storm-dft/settings/modules/DftIOSettings.cpp b/src/storm-dft/settings/modules/DftIOSettings.cpp
new file mode 100644
index 000000000..cf656333d
--- /dev/null
+++ b/src/storm-dft/settings/modules/DftIOSettings.cpp
@@ -0,0 +1,123 @@
+#include "DftIOSettings.h"
+
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/SettingMemento.h"
+#include "storm/settings/Option.h"
+#include "storm/settings/OptionBuilder.h"
+#include "storm/settings/ArgumentBuilder.h"
+#include "storm/settings/Argument.h"
+#include "storm/exceptions/InvalidSettingsException.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            
+            const std::string DftIOSettings::moduleName = "dftIO";
+            const std::string DftIOSettings::dftFileOptionName = "dftfile";
+            const std::string DftIOSettings::dftFileOptionShortName = "dft";
+            const std::string DftIOSettings::dftJsonFileOptionName = "dftfile-json";
+            const std::string DftIOSettings::dftJsonFileOptionShortName = "dftjson";
+            const std::string DftIOSettings::propExpectedTimeOptionName = "expectedtime";
+            const std::string DftIOSettings::propExpectedTimeOptionShortName = "mttf";
+            const std::string DftIOSettings::propProbabilityOptionName = "probability";
+            const std::string DftIOSettings::propTimeboundOptionName = "timebound";
+            const std::string DftIOSettings::propTimepointsOptionName = "timepoints";
+            const std::string DftIOSettings::minValueOptionName = "min";
+            const std::string DftIOSettings::maxValueOptionName = "max";
+            const std::string DftIOSettings::transformToGspnOptionName = "gspn";
+            const std::string DftIOSettings::exportToJsonOptionName = "export-json";
+
+            DftIOSettings::DftIOSettings() : 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.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, dftJsonFileOptionName, false, "Parses the model given in the Cytoscape JSON format.").setShortName(dftJsonFileOptionShortName)
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file from which to read the DFT model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).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.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterValidator(0.0)).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, propTimepointsOptionName, false, "Compute probability of system failure up to given timebound for a set of given timepoints [starttime, starttime+inc, starttime+2inc, ... ,endtime]").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("starttime", "The timebound to start from.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("endtime", "The timebound to end with.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("inc", "The value to increment with to get the next timepoint.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(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());
+                this->addOption(storm::settings::OptionBuilder(moduleName, transformToGspnOptionName, false, "Transform DFT to GSPN.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, exportToJsonOptionName, false,  "Export the model to the Cytoscape JSON format.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file to export to.").build()).build());
+            }
+
+            bool DftIOSettings::isDftFileSet() const {
+                return this->getOption(dftFileOptionName).getHasOptionBeenSet();
+            }
+            
+            std::string DftIOSettings::getDftFilename() const {
+                return this->getOption(dftFileOptionName).getArgumentByName("filename").getValueAsString();
+            }
+
+            bool DftIOSettings::isDftJsonFileSet() const {
+                return this->getOption(dftJsonFileOptionName).getHasOptionBeenSet();
+            }
+
+            std::string DftIOSettings::getDftJsonFilename() const {
+                return this->getOption(dftJsonFileOptionName).getArgumentByName("filename").getValueAsString();
+            }
+
+            bool DftIOSettings::usePropExpectedTime() const {
+                return this->getOption(propExpectedTimeOptionName).getHasOptionBeenSet();
+            }
+            
+            bool DftIOSettings::usePropProbability() const {
+                return this->getOption(propProbabilityOptionName).getHasOptionBeenSet();
+            }
+            
+            bool DftIOSettings::usePropTimebound() const {
+                return this->getOption(propTimeboundOptionName).getHasOptionBeenSet();
+            }
+
+            double DftIOSettings::getPropTimebound() const {
+                return this->getOption(propTimeboundOptionName).getArgumentByName("time").getValueAsDouble();
+            }
+
+            bool DftIOSettings::usePropTimepoints() const {
+                return this->getOption(propTimepointsOptionName).getHasOptionBeenSet();
+            }
+
+            std::vector<double> DftIOSettings::getPropTimepoints() const {
+                double starttime = this->getOption(propTimepointsOptionName).getArgumentByName("starttime").getValueAsDouble();
+                double endtime = this->getOption(propTimepointsOptionName).getArgumentByName("endtime").getValueAsDouble();
+                double inc = this->getOption(propTimepointsOptionName).getArgumentByName("inc").getValueAsDouble();
+                std::vector<double> timepoints;
+                for (double time = starttime; time <= endtime; time += inc) {
+                    timepoints.push_back(time);
+                }
+                return timepoints;
+            }
+
+            bool DftIOSettings::isComputeMinimalValue() const {
+                return this->getOption(minValueOptionName).getHasOptionBeenSet();
+            }
+            
+            bool DftIOSettings::isComputeMaximalValue() const {
+                return this->getOption(maxValueOptionName).getHasOptionBeenSet();
+            }
+            
+            bool DftIOSettings::isTransformToGspn() const {
+                return this->getOption(transformToGspnOptionName).getHasOptionBeenSet();
+            }
+
+            bool DftIOSettings::isExportToJson() const {
+                return this->getOption(exportToJsonOptionName).getHasOptionBeenSet();
+            }
+
+            std::string DftIOSettings::getExportJsonFilename() const {
+                return this->getOption(exportToJsonOptionName).getArgumentByName("filename").getValueAsString();
+            }
+
+            void DftIOSettings::finalize() {
+            }
+
+            bool DftIOSettings::check() const {
+                // 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
diff --git a/src/storm-dft/settings/modules/DFTSettings.h b/src/storm-dft/settings/modules/DftIOSettings.h
similarity index 63%
rename from src/storm-dft/settings/modules/DFTSettings.h
rename to src/storm-dft/settings/modules/DftIOSettings.h
index c04ef1a23..8a8fbcdd1 100644
--- a/src/storm-dft/settings/modules/DFTSettings.h
+++ b/src/storm-dft/settings/modules/DftIOSettings.h
@@ -1,24 +1,21 @@
 #pragma once
 
-#include "storm-config.h"
 #include "storm/settings/modules/ModuleSettings.h"
 
-#include "storm-dft/builder/DftExplorationHeuristic.h"
-
 namespace storm {
     namespace settings {
         namespace modules {
 
             /*!
-             * This class represents the settings for DFT model checking.
+             * This class represents the settings for IO operations concerning DFTs.
              */
-            class DFTSettings : public ModuleSettings {
+            class DftIOSettings : public ModuleSettings {
             public:
 
                 /*!
-                 * Creates a new set of DFT settings.
+                 * Creates a new set of IO settings for DFTs.
                  */
-                DFTSettings();
+                DftIOSettings();
                 
                 /*!
                  * Retrieves whether the dft file option was set.
@@ -48,48 +45,6 @@ namespace storm {
                  */
                 std::string getDftJsonFilename() const;
 
-                /*!
-                 * 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 option to compute an approximation is set.
-                 *
-                 * @return True iff the option was set.
-                 */
-                bool isApproximationErrorSet() const;
-
-                /*!
-                 * Retrieves the relative error allowed for approximating the model checking result.
-                 *
-                 * @return The allowed errorbound.
-                 */
-                double getApproximationError() const;
-
-                /*!
-                 * Retrieves the heuristic used for approximation.
-                 *
-                 * @return The heuristic to use.
-                 */
-                storm::builder::ApproximationHeuristic getApproximationHeuristic() const;
-
                 /*!
                  * Retrieves whether the property expected time should be used.
                  *
@@ -146,13 +101,6 @@ namespace storm {
                  */
                 bool isComputeMaximalValue() const;
 
-                /*!
-                 * Retrieves whether the non-determinism should be avoided by always taking the first possible dependency.
-                 *
-                 * @return True iff the option was set.
-                 */
-                bool isTakeFirstDependency() const;
-
                 /*!
                  * Retrieves whether the DFT should be transformed into a GSPN.
                  *
@@ -174,15 +122,6 @@ namespace storm {
                  */
                 std::string getExportJsonFilename() const;
                 
-#ifdef STORM_HAVE_Z3
-                /*!
-                 * Retrieves whether the DFT should be checked via SMT.
-                 *
-                 * @return True iff the option was set.
-                 */
-                bool solveWithSMT() const;
-#endif
-                
                 bool check() const override;
                 void finalize() override;
 
@@ -195,13 +134,6 @@ namespace storm {
                 static const std::string dftFileOptionShortName;
                 static const std::string dftJsonFileOptionName;
                 static const std::string dftJsonFileOptionShortName;
-                static const std::string symmetryReductionOptionName;
-                static const std::string symmetryReductionOptionShortName;
-                static const std::string modularisationOptionName;
-                static const std::string disableDCOptionName;
-                static const std::string approximationErrorOptionName;
-                static const std::string approximationErrorOptionShortName;
-                static const std::string approximationHeuristicOptionName;
                 static const std::string propExpectedTimeOptionName;
                 static const std::string propExpectedTimeOptionShortName;
                 static const std::string propProbabilityOptionName;
@@ -209,10 +141,6 @@ namespace storm {
                 static const std::string propTimepointsOptionName;
                 static const std::string minValueOptionName;
                 static const std::string maxValueOptionName;
-                static const std::string firstDependencyOptionName;
-#ifdef STORM_HAVE_Z3
-                static const std::string solveWithSmtOptionName;
-#endif
                 static const std::string transformToGspnOptionName;
                 static const std::string exportToJsonOptionName;
                 
diff --git a/src/storm-dft/settings/modules/FaultTreeSettings.cpp b/src/storm-dft/settings/modules/FaultTreeSettings.cpp
new file mode 100644
index 000000000..7c9ef14af
--- /dev/null
+++ b/src/storm-dft/settings/modules/FaultTreeSettings.cpp
@@ -0,0 +1,93 @@
+#include "FaultTreeSettings.h"
+
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/SettingMemento.h"
+#include "storm/settings/Option.h"
+#include "storm/settings/OptionBuilder.h"
+#include "storm/settings/ArgumentBuilder.h"
+#include "storm/settings/Argument.h"
+#include "storm/exceptions/IllegalArgumentValueException.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            
+            const std::string FaultTreeSettings::moduleName = "dft";
+            const std::string FaultTreeSettings::symmetryReductionOptionName = "symmetryreduction";
+            const std::string FaultTreeSettings::symmetryReductionOptionShortName = "symred";
+            const std::string FaultTreeSettings::modularisationOptionName = "modularisation";
+            const std::string FaultTreeSettings::disableDCOptionName = "disabledc";
+            const std::string FaultTreeSettings::approximationErrorOptionName = "approximation";
+            const std::string FaultTreeSettings::approximationErrorOptionShortName = "approx";
+            const std::string FaultTreeSettings::approximationHeuristicOptionName = "approximationheuristic";
+            const std::string FaultTreeSettings::firstDependencyOptionName = "firstdep";
+#ifdef STORM_HAVE_Z3
+            const std::string FaultTreeSettings::solveWithSmtOptionName = "smt";
+#endif
+
+            FaultTreeSettings::FaultTreeSettings() : ModuleSettings(moduleName) {
+                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, firstDependencyOptionName, false, "Avoid non-determinism by always taking the first possible dependency.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, approximationErrorOptionName, false, "Approximation error allowed.").setShortName(approximationErrorOptionShortName).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("error", "The relative approximation error to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, approximationHeuristicOptionName, false, "Set the heuristic used for approximation.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("heuristic", "Sets which heuristic is used for approximation. Must be in {depth, probability}. Default is").setDefaultValueString("depth").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator({"depth", "rateratio"})).build()).build());
+#ifdef STORM_HAVE_Z3
+                this->addOption(storm::settings::OptionBuilder(moduleName, solveWithSmtOptionName, true, "Solve the DFT with SMT.").build());
+#endif
+            }
+
+            bool FaultTreeSettings::useSymmetryReduction() const {
+                return this->getOption(symmetryReductionOptionName).getHasOptionBeenSet();
+            }
+            
+            bool FaultTreeSettings::useModularisation() const {
+                return this->getOption(modularisationOptionName).getHasOptionBeenSet();
+            }
+            
+            bool FaultTreeSettings::isDisableDC() const {
+                return this->getOption(disableDCOptionName).getHasOptionBeenSet();
+            }
+
+            bool FaultTreeSettings::isApproximationErrorSet() const {
+                return this->getOption(approximationErrorOptionName).getHasOptionBeenSet();
+            }
+
+            double FaultTreeSettings::getApproximationError() const {
+                return this->getOption(approximationErrorOptionName).getArgumentByName("error").getValueAsDouble();
+            }
+
+            storm::builder::ApproximationHeuristic FaultTreeSettings::getApproximationHeuristic() const {
+                if (!isApproximationErrorSet() || getApproximationError() == 0.0) {
+                    // No approximation is done
+                    return storm::builder::ApproximationHeuristic::NONE;
+                }
+                std::string heuristicAsString = this->getOption(approximationHeuristicOptionName).getArgumentByName("heuristic").getValueAsString();
+                if (heuristicAsString == "depth") {
+                    return storm::builder::ApproximationHeuristic::DEPTH;
+                } else if (heuristicAsString == "probability") {
+                    return storm::builder::ApproximationHeuristic::PROBABILITY;
+                }
+                STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal value '" << heuristicAsString << "' set as heuristic for approximation.");
+            }
+
+            bool FaultTreeSettings::isTakeFirstDependency() const {
+                return this->getOption(firstDependencyOptionName).getHasOptionBeenSet();
+            }
+
+#ifdef STORM_HAVE_Z3
+            bool FaultTreeSettings::solveWithSMT() const {
+                return this->getOption(solveWithSmtOptionName).getHasOptionBeenSet();
+            }
+#endif
+            
+            void FaultTreeSettings::finalize() {
+            }
+
+            bool FaultTreeSettings::check() const {
+                return true;
+            }
+            
+        } // namespace modules
+    } // namespace settings
+} // namespace storm
diff --git a/src/storm-dft/settings/modules/FaultTreeSettings.h b/src/storm-dft/settings/modules/FaultTreeSettings.h
new file mode 100644
index 000000000..171d5c38e
--- /dev/null
+++ b/src/storm-dft/settings/modules/FaultTreeSettings.h
@@ -0,0 +1,104 @@
+#pragma once
+
+#include "storm/settings/modules/ModuleSettings.h"
+#include "storm-dft/builder/DftExplorationHeuristic.h"
+#include "storm-config.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+
+            /*!
+             * This class represents the settings for DFT model checking.
+             */
+            class FaultTreeSettings : public ModuleSettings {
+            public:
+
+                /*!
+                 * Creates a new set of DFT settings.
+                 */
+                FaultTreeSettings();
+
+                /*!
+                 * 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 option to compute an approximation is set.
+                 *
+                 * @return True iff the option was set.
+                 */
+                bool isApproximationErrorSet() const;
+
+                /*!
+                 * Retrieves the relative error allowed for approximating the model checking result.
+                 *
+                 * @return The allowed errorbound.
+                 */
+                double getApproximationError() const;
+
+                /*!
+                 * Retrieves the heuristic used for approximation.
+                 *
+                 * @return The heuristic to use.
+                 */
+                storm::builder::ApproximationHeuristic getApproximationHeuristic() const;
+
+                /*!
+                 * Retrieves whether the non-determinism should be avoided by always taking the first possible dependency.
+                 *
+                 * @return True iff the option was set.
+                 */
+                bool isTakeFirstDependency() const;
+                
+#ifdef STORM_HAVE_Z3
+                /*!
+                 * Retrieves whether the DFT should be checked via SMT.
+                 *
+                 * @return True iff the option was set.
+                 */
+                bool solveWithSMT() const;
+#endif
+                
+                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 symmetryReductionOptionName;
+                static const std::string symmetryReductionOptionShortName;
+                static const std::string modularisationOptionName;
+                static const std::string disableDCOptionName;
+                static const std::string approximationErrorOptionName;
+                static const std::string approximationErrorOptionShortName;
+                static const std::string approximationHeuristicOptionName;
+                static const std::string firstDependencyOptionName;
+#ifdef STORM_HAVE_Z3
+                static const std::string solveWithSmtOptionName;
+#endif
+
+            };
+
+        } // namespace modules
+    } // namespace settings
+} // namespace storm

From 91bd638c1876120132994acbb3200eaa4c815d33 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Thu, 12 Oct 2017 10:46:53 +0200
Subject: [PATCH 2/7] Fixed segfault

---
 src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
index f035b0a55..c7d6605f5 100644
--- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
+++ b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
@@ -581,13 +581,13 @@ namespace storm {
                     maComponents.rateTransitions = true;
                     maComponents.markovianStates = modelComponents.markovianStates;
                     maComponents.exitRates = modelComponents.exitRates;
-                    std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(maComponents));
+                    ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(maComponents));
                 } else {
                     storm::storage::sparse::ModelComponents<ValueType> maComponents(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling));
                     maComponents.rateTransitions = true;
                     maComponents.markovianStates = std::move(modelComponents.markovianStates);
                     maComponents.exitRates = std::move(modelComponents.exitRates);
-                    std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(maComponents));
+                    ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(maComponents));
                 }
                 if (ma->hasOnlyTrivialNondeterminism()) {
                     // Markov automaton can be converted into CTMC

From 983e09fd635b1911821e88b7373a1dd58e8bbc1b Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Thu, 12 Oct 2017 18:18:36 +0200
Subject: [PATCH 3/7] Fixed possible problem with rates and exit rates in MA

---
 src/storm/models/sparse/MarkovAutomaton.cpp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/storm/models/sparse/MarkovAutomaton.cpp b/src/storm/models/sparse/MarkovAutomaton.cpp
index 485aa8a64..8bc00fa99 100644
--- a/src/storm/models/sparse/MarkovAutomaton.cpp
+++ b/src/storm/models/sparse/MarkovAutomaton.cpp
@@ -50,7 +50,9 @@ namespace storm {
                 
                 if (components.exitRates) {
                     exitRates = std::move(components.exitRates.get());
-                } else {
+                }
+
+                if (components.rateTransitions) {
                     this->turnRatesToProbabilities();
                 }
                 closed = this->checkIsClosed();

From 88544a9ec79bf7a4613eaf05fba64895701951d3 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Thu, 12 Oct 2017 18:19:36 +0200
Subject: [PATCH 4/7] Added assertion for turnRatesToProbabilities in MA

---
 src/storm/models/sparse/MarkovAutomaton.cpp | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/storm/models/sparse/MarkovAutomaton.cpp b/src/storm/models/sparse/MarkovAutomaton.cpp
index 8bc00fa99..ca79ccfac 100644
--- a/src/storm/models/sparse/MarkovAutomaton.cpp
+++ b/src/storm/models/sparse/MarkovAutomaton.cpp
@@ -152,7 +152,7 @@ namespace storm {
                     uint_fast64_t row = this->getTransitionMatrix().getRowGroupIndices()[state];
                     if (this->markovianStates.get(state)) {
                         if (assertRates) {
-                        STORM_LOG_THROW(this->exitRates[state] == this->getTransitionMatrix().getRowSum(row), storm::exceptions::InvalidArgumentException, "The specified exit rate is inconsistent with the rate matrix. Difference is " << (this->exitRates[state] - this->getTransitionMatrix().getRowSum(row)) << ".");
+                            STORM_LOG_THROW(this->exitRates[state] == this->getTransitionMatrix().getRowSum(row), storm::exceptions::InvalidArgumentException, "The specified exit rate is inconsistent with the rate matrix. Difference is " << (this->exitRates[state] - this->getTransitionMatrix().getRowSum(row)) << ".");
                         } else {
                             this->exitRates.push_back(this->getTransitionMatrix().getRowSum(row));
                         }
@@ -161,7 +161,11 @@ namespace storm {
                         }
                         ++row;
                     } else {
-                        this->exitRates.push_back(storm::utility::zero<ValueType>());
+                        if (assertRates) {
+                            STORM_LOG_THROW(storm::utility::isZero<ValueType>(this->exitRates[state]), storm::exceptions::InvalidArgumentException, "The specified exit rate for (non-Markovian) choice should be 0.");
+                        } else {
+                            this->exitRates.push_back(storm::utility::zero<ValueType>());
+                        }
                     }
                     for (; row < this->getTransitionMatrix().getRowGroupIndices()[state+1]; ++row) {
                         STORM_LOG_THROW(storm::utility::isOne(this->getTransitionMatrix().getRowSum(row)), storm::exceptions::InvalidArgumentException, "Entries of transition matrix do not sum up to one for (non-Markovian) choice " << row << " of state " << state << " (sum is " << this->getTransitionMatrix().getRowSum(row) << ").");

From 4456069e81e995d844bb7e447832f5f258488da5 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Thu, 12 Oct 2017 18:19:52 +0200
Subject: [PATCH 5/7] Fixed typo

---
 src/storm/models/sparse/MarkovAutomaton.h | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/storm/models/sparse/MarkovAutomaton.h b/src/storm/models/sparse/MarkovAutomaton.h
index 249766b62..89c73f83c 100644
--- a/src/storm/models/sparse/MarkovAutomaton.h
+++ b/src/storm/models/sparse/MarkovAutomaton.h
@@ -22,7 +22,7 @@ namespace storm {
                  * For hybrid states (i.e., states with Markovian and probabilistic transitions), it is assumed that the first
                  * choice corresponds to the markovian transitions.
                  *
-                 * @param transitionMatrix The matrix representing the transitions in the model in terms of rates (markocian choices) and probabilities (probabilistic choices).
+                 * @param transitionMatrix The matrix representing the transitions in the model in terms of rates (Markovian choices) and probabilities (probabilistic choices).
                  * @param stateLabeling The labeling of the states.
                  * @param markovianStates A bit vector indicating the Markovian states of the automaton (i.e., states with at least one markovian transition).
                  * @param rewardModels A mapping of reward model names to reward models.
@@ -38,7 +38,7 @@ namespace storm {
                  * For hybrid states (i.e., states with Markovian and probabilistic transitions), it is assumed that the first
                  * choice corresponds to the markovian transitions.
                  *
-                 * @param transitionMatrix The matrix representing the transitions in the model in terms of rates (markocian choices) and probabilities (probabilistic choices).
+                 * @param transitionMatrix The matrix representing the transitions in the model in terms of rates (Markovian choices) and probabilities (probabilistic choices).
                  * @param stateLabeling The labeling of the states.
                  * @param markovianStates A bit vector indicating the Markovian states of the automaton (i.e., states with at least one markovian transition).
                  * @param rewardModels A mapping of reward model names to reward models.

From 87778a677526a11651a912601b35b45a9896edcf Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Thu, 12 Oct 2017 20:33:24 +0200
Subject: [PATCH 6/7] Finally removed old DFTModelBuilder

---
 .../builder/ExplicitDFTModelBuilder.cpp       | 471 ------------------
 .../builder/ExplicitDFTModelBuilder.h         | 102 ----
 .../modelchecker/dft/DFTModelChecker.cpp      |  17 +-
 3 files changed, 4 insertions(+), 586 deletions(-)
 delete mode 100644 src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
 delete mode 100644 src/storm-dft/builder/ExplicitDFTModelBuilder.h

diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
deleted file mode 100644
index 5ef6bd07e..000000000
--- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
+++ /dev/null
@@ -1,471 +0,0 @@
-#include "ExplicitDFTModelBuilder.h"
-
-#include <map>
-
-#include "storm/models/sparse/MarkovAutomaton.h"
-#include "storm/models/sparse/Ctmc.h"
-#include "storm/utility/constants.h"
-#include "storm/utility/vector.h"
-#include "storm/exceptions/UnexpectedException.h"
-#include "storm/settings/SettingsManager.h"
-
-
-namespace storm {
-    namespace builder {
-
-        template <typename ValueType>
-        ExplicitDFTModelBuilder<ValueType>::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), markovianStates(), exitRates(), choiceLabeling() {
-            // Intentionally left empty.
-        }
-        
-        template <typename ValueType>
-        ExplicitDFTModelBuilder<ValueType>::ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC) : mDft(dft), mStates(((mDft.stateVectorSize() / 64) + 1) * 64, INITIAL_BUCKETSIZE), enableDC(enableDC) {
-            // stateVectorSize is bound for size of bitvector
-
-            mStateGenerationInfo = std::make_shared<storm::storage::DFTStateGenerationInfo>(mDft.buildStateGenerationInfo(symmetries));
-        }
-
-
-        template <typename ValueType>
-        std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilder<ValueType>::buildModel(LabelOptions const& labelOpts) {
-            // Initialize
-            bool deterministicModel = false;
-            size_t rowOffset = 0;
-            ModelComponents modelComponents;
-            std::vector<uint_fast64_t> tmpMarkovianStates;
-            storm::storage::SparseMatrixBuilder<ValueType> transitionMatrixBuilder(0, 0, 0, false, !deterministicModel, 0);
-
-            if(mergeFailedStates) {
-                // Introduce explicit fail state
-                failedIndex = newIndex;
-                newIndex++;
-                transitionMatrixBuilder.newRowGroup(failedIndex);
-                transitionMatrixBuilder.addNextValue(failedIndex, failedIndex, storm::utility::one<ValueType>());
-                STORM_LOG_TRACE("Introduce fail state with id: " << failedIndex);
-                modelComponents.exitRates.push_back(storm::utility::one<ValueType>());
-                tmpMarkovianStates.push_back(failedIndex);        
-            }
-            
-            // Explore state space
-            DFTStatePointer state = std::make_shared<storm::storage::DFTState<ValueType>>(mDft, *mStateGenerationInfo, newIndex);
-            auto exploreResult = exploreStates(state, rowOffset, transitionMatrixBuilder, tmpMarkovianStates, modelComponents.exitRates);
-            initialStateIndex = exploreResult.first;
-            bool deterministic = exploreResult.second;
-        
-            // Before ending the exploration check for pseudo states which are not initialized yet
-            for (auto & pseudoStatePair : mPseudoStatesMapping) {
-                if (pseudoStatePair.first == 0) {
-                    // Create state from pseudo state and explore
-                    STORM_LOG_ASSERT(mStates.contains(pseudoStatePair.second), "Pseudo state not contained.");
-                    STORM_LOG_ASSERT(mStates.getValue(pseudoStatePair.second) >= OFFSET_PSEUDO_STATE, "State is no pseudo state.");
-                    STORM_LOG_TRACE("Create pseudo state from bit vector " << pseudoStatePair.second);
-                    DFTStatePointer pseudoState = std::make_shared<storm::storage::DFTState<ValueType>>(pseudoStatePair.second, mDft, *mStateGenerationInfo, newIndex);
-                    pseudoState->construct();
-                    STORM_LOG_ASSERT(pseudoStatePair.second == pseudoState->status(), "Pseudo states do not coincide.");
-                    STORM_LOG_TRACE("Explore pseudo state " << mDft.getStateString(pseudoState) << " with id " << pseudoState->getId());
-                    auto exploreResult = exploreStates(pseudoState, rowOffset, transitionMatrixBuilder, tmpMarkovianStates, modelComponents.exitRates);
-                    deterministic &= exploreResult.second;
-                    STORM_LOG_ASSERT(pseudoStatePair.first == pseudoState->getId(), "Pseudo state ids do not coincide");
-                    STORM_LOG_ASSERT(pseudoState->getId() == exploreResult.first, "Pseudo state ids do not coincide.");
-                }
-            }
-            
-            // Replace pseudo states in matrix
-            std::vector<uint_fast64_t> pseudoStatesVector;
-            for (auto const& pseudoStatePair : mPseudoStatesMapping) {
-                pseudoStatesVector.push_back(pseudoStatePair.first);
-            }
-            STORM_LOG_ASSERT(std::find(pseudoStatesVector.begin(), pseudoStatesVector.end(), 0) == pseudoStatesVector.end(), "Unexplored pseudo state still contained.");
-            transitionMatrixBuilder.replaceColumns(pseudoStatesVector, OFFSET_PSEUDO_STATE);
-            
-            STORM_LOG_DEBUG("Generated " << mStates.size() + (mergeFailedStates ? 1 : 0) << " states");
-            STORM_LOG_DEBUG("Model is " << (deterministic ? "deterministic" : "non-deterministic"));
-
-            size_t stateSize = mStates.size() + (mergeFailedStates ? 1 : 0);
-            // Build Markov Automaton
-            modelComponents.markovianStates = storm::storage::BitVector(stateSize, tmpMarkovianStates);
-            // Build transition matrix
-            modelComponents.transitionMatrix = transitionMatrixBuilder.build(stateSize, stateSize);
-            if (stateSize <= 15) {
-                STORM_LOG_TRACE("Transition matrix: " << std::endl << modelComponents.transitionMatrix);
-            } else {
-                STORM_LOG_TRACE("Transition matrix: too big to print");
-            }
-            STORM_LOG_TRACE("Exit rates: " << storm::utility::vector::toString<ValueType>(modelComponents.exitRates));
-            STORM_LOG_TRACE("Markovian states: " << modelComponents.markovianStates);
-            
-            // Build state labeling
-            modelComponents.stateLabeling = storm::models::sparse::StateLabeling(mStates.size() + (mergeFailedStates ? 1 : 0));
-            // Initial state is always first state without any failure
-            modelComponents.stateLabeling.addLabel("init");
-            modelComponents.stateLabeling.addLabelToState("init", initialStateIndex);
-            // Label all states corresponding to their status (failed, failsafe, failed BE)
-            if(labelOpts.buildFailLabel) {
-                modelComponents.stateLabeling.addLabel("failed");
-            } 
-            if(labelOpts.buildFailSafeLabel) {
-                modelComponents.stateLabeling.addLabel("failsafe");
-            }
-            
-            // Collect labels for all BE
-            std::vector<std::shared_ptr<storage::DFTBE<ValueType>>> basicElements = mDft.getBasicElements();
-            for (std::shared_ptr<storage::DFTBE<ValueType>> elem : basicElements) {
-                if(labelOpts.beLabels.count(elem->name()) > 0) {
-                    modelComponents.stateLabeling.addLabel(elem->name() + "_fail");
-                }
-            }
-
-            if(mergeFailedStates) {
-                modelComponents.stateLabeling.addLabelToState("failed", failedIndex);
-            }
-            for (auto const& stateIdPair : mStates) {
-                storm::storage::BitVector state = stateIdPair.first;
-                size_t stateId = stateIdPair.second;
-                if (!mergeFailedStates && labelOpts.buildFailLabel && mDft.hasFailed(state, *mStateGenerationInfo)) {
-                    modelComponents.stateLabeling.addLabelToState("failed", stateId);
-                }
-                if (labelOpts.buildFailSafeLabel && mDft.isFailsafe(state, *mStateGenerationInfo)) {
-                    modelComponents.stateLabeling.addLabelToState("failsafe", stateId);
-                };
-                // Set fail status for each BE
-                for (std::shared_ptr<storage::DFTBE<ValueType>> elem : basicElements) {
-                    if (labelOpts.beLabels.count(elem->name()) > 0 && storm::storage::DFTState<ValueType>::hasFailed(state, mStateGenerationInfo->getStateIndex(elem->id())) ) {
-                        modelComponents.stateLabeling.addLabelToState(elem->name() + "_fail", stateId);
-                    }
-                }
-            }
-
-            std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
-            storm::storage::sparse::ModelComponents<ValueType> components(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling));
-                    components.exitRates = std::move(modelComponents.exitRates);
-            if (deterministic) {
-                components.transitionMatrix.makeRowGroupingTrivial();
-                model = std::make_shared<storm::models::sparse::Ctmc<ValueType>>(std::move(components));
-            } else {
-                    components.markovianStates = std::move(modelComponents.markovianStates);
-                    std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(components));
-                if (ma->hasOnlyTrivialNondeterminism()) {
-                    // Markov automaton can be converted into CTMC
-                    model = ma->convertToCTMC();
-                } else {
-                    model = ma;
-                }
-            }
-            
-            return model;
-        }
-        
-        template <typename ValueType>
-        std::pair<uint_fast64_t, bool> ExplicitDFTModelBuilder<ValueType>::exploreStates(DFTStatePointer const& state, size_t& rowOffset, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<uint_fast64_t>& markovianStates, std::vector<ValueType>& exitRates) {
-            STORM_LOG_TRACE("Explore state: " << mDft.getStateString(state));
-
-            auto explorePair = checkForExploration(state);
-            if (!explorePair.first) {
-                // State does not need any exploration
-                return std::make_pair(explorePair.second, true);
-            }
-
-            
-            // Initialization
-            // TODO Matthias: set Markovian states directly as bitvector?
-            std::map<uint_fast64_t, ValueType> outgoingRates;
-            std::vector<std::map<uint_fast64_t, ValueType>> outgoingProbabilities;
-            bool hasDependencies = state->nrFailableDependencies() > 0;
-            size_t failableCount = hasDependencies ? state->nrFailableDependencies() : state->nrFailableBEs();
-            size_t smallest = 0;
-            ValueType exitRate = storm::utility::zero<ValueType>();
-            bool deterministic = !hasDependencies;
-
-            // Absorbing state
-            if (mDft.hasFailed(state) || mDft.isFailsafe(state) || state->nrFailableBEs() == 0) {
-                uint_fast64_t stateId = addState(state);
-                STORM_LOG_ASSERT(stateId == state->getId(), "Ids do not coincide.");
-
-                // Add self loop
-                transitionMatrixBuilder.newRowGroup(stateId + rowOffset);
-                transitionMatrixBuilder.addNextValue(stateId + rowOffset, stateId, storm::utility::one<ValueType>());
-                STORM_LOG_TRACE("Added self loop for " << stateId);
-                exitRates.push_back(storm::utility::one<ValueType>());
-                STORM_LOG_ASSERT(exitRates.size()-1 == stateId, "No. of considered states does not match state id.");
-                markovianStates.push_back(stateId);
-                // No further exploration required
-                return std::make_pair(stateId, true);
-            }
-
-            // Let BE fail
-            while (smallest < failableCount) {
-                STORM_LOG_ASSERT(!mDft.hasFailed(state), "Dft has failed.");
-
-                // Construct new state as copy from original one
-                DFTStatePointer newState = std::make_shared<storm::storage::DFTState<ValueType>>(*state);
-                std::pair<std::shared_ptr<storm::storage::DFTBE<ValueType> const>, bool> nextBEPair = newState->letNextBEFail(smallest++);
-                std::shared_ptr<storm::storage::DFTBE<ValueType> const>& nextBE = nextBEPair.first;
-                STORM_LOG_ASSERT(nextBE, "NextBE is null.");
-                STORM_LOG_ASSERT(nextBEPair.second == hasDependencies, "Failure due to dependencies does not match.");
-                STORM_LOG_TRACE("With the failure of: " << nextBE->name() << " [" << nextBE->id() << "] in " << mDft.getStateString(state));
-
-                // Propagate failures
-                storm::storage::DFTStateSpaceGenerationQueues<ValueType> queues;
-
-                for (DFTGatePointer parent : nextBE->parents()) {
-                    if (newState->isOperational(parent->id())) {
-                        queues.propagateFailure(parent);
-                    }
-                }
-                for (DFTRestrictionPointer restr : nextBE->restrictions()) {
-                    queues.checkRestrictionLater(restr);
-                }
-
-                while (!queues.failurePropagationDone()) {
-                    DFTGatePointer next = queues.nextFailurePropagation();
-                    next->checkFails(*newState, queues);
-                    newState->updateFailableDependencies(next->id());
-                }
-                
-                while(!queues.restrictionChecksDone()) {
-                    DFTRestrictionPointer next = queues.nextRestrictionCheck();
-                    next->checkFails(*newState, queues);
-                    newState->updateFailableDependencies(next->id());
-                }
-                
-                if(newState->isInvalid()) {
-                    continue;
-                }
-                bool dftFailed = newState->hasFailed(mDft.getTopLevelIndex());
-                
-                while (!dftFailed && !queues.failsafePropagationDone()) {
-                    DFTGatePointer next = queues.nextFailsafePropagation();
-                    next->checkFailsafe(*newState, queues);
-                }
-
-                while (!dftFailed && enableDC && !queues.dontCarePropagationDone()) {
-                    DFTElementPointer next = queues.nextDontCarePropagation();
-                    next->checkDontCareAnymore(*newState, queues);
-                }
-                
-                // Update failable dependencies
-                if (!dftFailed) {
-                    newState->updateFailableDependencies(nextBE->id());
-                    newState->updateDontCareDependencies(nextBE->id());
-                }
-                
-                uint_fast64_t newStateId;
-                if(dftFailed && mergeFailedStates) {
-                    newStateId = failedIndex;
-                } else {
-                    // Explore new state recursively
-                    auto explorePair = exploreStates(newState, rowOffset, transitionMatrixBuilder, markovianStates, exitRates);
-                    newStateId = explorePair.first;
-                    deterministic &= explorePair.second;
-                }
-
-                // Set transitions
-                if (hasDependencies) {
-                    // Failure is due to dependency -> add non-deterministic choice
-                    std::map<uint_fast64_t, ValueType> choiceProbabilities;
-                    std::shared_ptr<storm::storage::DFTDependency<ValueType> const> dependency = mDft.getDependency(state->getDependencyId(smallest-1));
-                    choiceProbabilities.insert(std::make_pair(newStateId, dependency->probability()));
-                    STORM_LOG_TRACE("Added transition to " << newStateId << " with probability " << dependency->probability());
-
-                    if (!storm::utility::isOne(dependency->probability())) {
-                        // Add transition to state where dependency was unsuccessful
-                        DFTStatePointer unsuccessfulState = std::make_shared<storm::storage::DFTState<ValueType>>(*state);
-                        unsuccessfulState->letDependencyBeUnsuccessful(smallest-1);
-                        auto explorePair = exploreStates(unsuccessfulState, rowOffset, transitionMatrixBuilder, markovianStates, exitRates);
-                        uint_fast64_t unsuccessfulStateId = explorePair.first;
-                        deterministic &= explorePair.second;
-                        ValueType remainingProbability = storm::utility::one<ValueType>() - dependency->probability();
-                        choiceProbabilities.insert(std::make_pair(unsuccessfulStateId, remainingProbability));
-                        STORM_LOG_TRACE("Added transition to " << unsuccessfulStateId << " with remaining probability " << remainingProbability);
-                    }
-                    outgoingProbabilities.push_back(choiceProbabilities);
-                } else {
-                    // Set failure rate according to activation
-                    bool isActive = true;
-                    if (mDft.hasRepresentant(nextBE->id())) {
-                        // Active must be checked for the state we are coming from as this state is responsible for the
-                        // rate and not the new state we are going to
-                        isActive = state->isActive(mDft.getRepresentant(nextBE->id()));
-                    }
-                    ValueType rate = isActive ? nextBE->activeFailureRate() : nextBE->passiveFailureRate();
-                    STORM_LOG_ASSERT(!storm::utility::isZero(rate), "Rate is 0.");
-                    auto resultFind = outgoingRates.find(newStateId);
-                    if (resultFind != outgoingRates.end()) {
-                        // Add to existing transition
-                        resultFind->second += rate;
-                        STORM_LOG_TRACE("Updated transition to " << resultFind->first << " with " << (isActive ? "active" : "passive") << " rate " << rate << " to new rate " << resultFind->second);
-                    } else {
-                        // Insert new transition
-                        outgoingRates.insert(std::make_pair(newStateId, rate));
-                        STORM_LOG_TRACE("Added transition to " << newStateId << " with " << (isActive ? "active" : "passive") << " rate " << rate);
-                    }
-                    exitRate += rate;
-                }
-
-            } // end while failing BE
-            
-            // Add state
-            uint_fast64_t stateId = addState(state);
-            STORM_LOG_ASSERT(stateId == state->getId(), "Ids do not match.");
-            STORM_LOG_ASSERT(stateId == newIndex-1, "Id does not match no. of states.");
-            
-            if (hasDependencies) {
-                // Add all probability transitions
-                STORM_LOG_ASSERT(outgoingRates.empty(), "Outgoing transitions not empty.");
-                transitionMatrixBuilder.newRowGroup(stateId + rowOffset);
-                for (size_t i = 0; i < outgoingProbabilities.size(); ++i, ++rowOffset) {
-                    STORM_LOG_ASSERT(outgoingProbabilities[i].size() == 1 || outgoingProbabilities[i].size() == 2, "No. of outgoing transitions is not valid.");
-                    for (auto it = outgoingProbabilities[i].begin(); it != outgoingProbabilities[i].end(); ++it)
-                    {
-                        STORM_LOG_TRACE("Set transition from " << stateId << " to " << it->first << " with probability " << it->second);
-                        transitionMatrixBuilder.addNextValue(stateId + rowOffset, it->first, it->second);
-                    }
-                }
-                rowOffset--; // One increment too many
-            } else {
-                // Try to merge pseudo states with their instantiation
-                // TODO Matthias: improve?
-                for (auto it = outgoingRates.begin(); it != outgoingRates.end(); ) {
-                    if (it->first >= OFFSET_PSEUDO_STATE) {
-                        uint_fast64_t newId = it->first - OFFSET_PSEUDO_STATE;
-                        STORM_LOG_ASSERT(newId < mPseudoStatesMapping.size(), "Id is not valid.");
-                        if (mPseudoStatesMapping[newId].first > 0) {
-                            // State exists already
-                            newId = mPseudoStatesMapping[newId].first;
-                            auto itFind = outgoingRates.find(newId);
-                            if (itFind != outgoingRates.end()) {
-                                // Add probability from pseudo state to instantiation
-                                itFind->second += it->second;
-                                STORM_LOG_TRACE("Merged pseudo state " << newId << " adding rate " << it->second << " to total rate of " << itFind->second);
-                            } else {
-                                // Only change id
-                                outgoingRates.emplace(newId, it->second);
-                                STORM_LOG_TRACE("Instantiated pseudo state " << newId << " with rate " << it->second);
-                            }
-                            // Remove pseudo state
-                            it = outgoingRates.erase(it);
-                        } else {
-                            ++it;
-                        }
-                    } else {
-                        ++it;
-                    }
-                }
-                
-                // Add all rate transitions
-                STORM_LOG_ASSERT(outgoingProbabilities.empty(), "Outgoing probabilities not empty.");
-                transitionMatrixBuilder.newRowGroup(state->getId() + rowOffset);
-                STORM_LOG_TRACE("Exit rate for " << state->getId() << ": " << exitRate);
-                for (auto it = outgoingRates.begin(); it != outgoingRates.end(); ++it)
-                {
-                    ValueType probability = it->second / exitRate; // Transform rate to probability
-                    STORM_LOG_TRACE("Set transition from " << state->getId() << " to " << it->first << " with rate " << it->second);
-                    transitionMatrixBuilder.addNextValue(state->getId() + rowOffset, it->first, probability);
-                }
-
-                markovianStates.push_back(state->getId());
-            }
-            
-            STORM_LOG_TRACE("Finished exploring state: " << mDft.getStateString(state));
-            exitRates.push_back(exitRate);
-            STORM_LOG_ASSERT(exitRates.size()-1 == state->getId(), "Id does not match no. of states.");
-            return std::make_pair(state->getId(), deterministic);
-        }
-        
-        template <typename ValueType>
-        std::pair<bool, uint_fast64_t> ExplicitDFTModelBuilder<ValueType>::checkForExploration(DFTStatePointer const& state) {
-            bool changed = false;
-            if (mStateGenerationInfo->hasSymmetries()) {
-                // Order state by symmetry
-                STORM_LOG_TRACE("Check for symmetry: " << mDft.getStateString(state));
-                changed = state->orderBySymmetry();
-                STORM_LOG_TRACE("State " << (changed ? "changed to " : "did not change") << (changed ? mDft.getStateString(state) : ""));
-            }
-            
-            if (mStates.contains(state->status())) {
-                // State already exists
-                uint_fast64_t stateId = mStates.getValue(state->status());
-                STORM_LOG_TRACE("State " << mDft.getStateString(state) << " with id " << stateId << " already exists");
-                
-                if (changed || stateId < OFFSET_PSEUDO_STATE) {
-                    // State is changed or an explored "normal" state
-                    return std::make_pair(false, stateId);
-                }
-                
-                stateId -= OFFSET_PSEUDO_STATE;
-                STORM_LOG_ASSERT(stateId < mPseudoStatesMapping.size(), "Id not valid.");
-                if (mPseudoStatesMapping[stateId].first > 0) {
-                    // Pseudo state already explored
-                    return std::make_pair(false, mPseudoStatesMapping[stateId].first);
-                }
-                
-                STORM_LOG_ASSERT(mPseudoStatesMapping[stateId].second == state->status(), "States do not coincide.");
-                STORM_LOG_TRACE("Pseudo state " << mDft.getStateString(state) << " can be explored now");
-                return std::make_pair(true, stateId);
-            } else {
-                // State does not exists
-                if (changed) {
-                    // Remember state for later creation
-                    state->setId(mPseudoStatesMapping.size() + OFFSET_PSEUDO_STATE);
-                    mPseudoStatesMapping.push_back(std::make_pair(0, state->status()));
-                    mStates.findOrAdd(state->status(), state->getId());
-                    STORM_LOG_TRACE("Remember state for later creation: " << mDft.getStateString(state));
-                    return std::make_pair(false, state->getId());
-                } else {
-                    // State needs exploration
-                    return std::make_pair(true, 0);
-                }
-            }
-        }
-
-        template <typename ValueType>
-        uint_fast64_t ExplicitDFTModelBuilder<ValueType>::addState(DFTStatePointer const& state) {
-            uint_fast64_t stateId;
-            // TODO remove
-            bool changed = state->orderBySymmetry();
-            STORM_LOG_ASSERT(!changed, "State to add has changed by applying symmetry.");
-            
-            // Check if state already exists
-            if (mStates.contains(state->status())) {
-                // State already exists
-                stateId = mStates.getValue(state->status());
-                STORM_LOG_TRACE("State " << mDft.getStateString(state) << " with id " << stateId << " already exists");
-                
-                // Check if possible pseudo state can be created now
-                STORM_LOG_ASSERT(stateId >= OFFSET_PSEUDO_STATE, "State is no pseudo state.");
-                stateId -= OFFSET_PSEUDO_STATE;
-                STORM_LOG_ASSERT(stateId < mPseudoStatesMapping.size(), "Pseudo state not known.");
-                if (mPseudoStatesMapping[stateId].first == 0) {
-                    // Create pseudo state now
-                    STORM_LOG_ASSERT(mPseudoStatesMapping[stateId].second == state->status(), "Pseudo states do not coincide.");
-                    state->setId(newIndex++);
-                    mPseudoStatesMapping[stateId].first = state->getId();
-                    stateId = state->getId();
-                    mStates.setOrAdd(state->status(), stateId);
-                    STORM_LOG_TRACE("Now create state " << mDft.getStateString(state) << " with id " << stateId);
-                    return stateId;
-                } else {
-                    STORM_LOG_ASSERT(false, "Pseudo state already created.");
-                    return 0;
-                }
-            } else {
-                // Create new state
-                state->setId(newIndex++);
-                stateId = mStates.findOrAdd(state->status(), state->getId());
-                STORM_LOG_TRACE("New state: " << mDft.getStateString(state));
-                return stateId;
-            }
-        }
-
-
-        // Explicitly instantiate the class.
-        template class ExplicitDFTModelBuilder<double>;
-
-#ifdef STORM_HAVE_CARL
-        template class ExplicitDFTModelBuilder<storm::RationalFunction>;
-#endif
-
-    } // namespace builder
-} // namespace storm
-
-
diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.h b/src/storm-dft/builder/ExplicitDFTModelBuilder.h
deleted file mode 100644
index 2913a78fa..000000000
--- a/src/storm-dft/builder/ExplicitDFTModelBuilder.h
+++ /dev/null
@@ -1,102 +0,0 @@
-#pragma  once
-
-#include <boost/container/flat_set.hpp>
-#include <boost/optional/optional.hpp>
-#include <stack>
-#include <unordered_set>
-
-
-#include "storm/models/sparse/StateLabeling.h"
-#include "storm/models/sparse/ChoiceLabeling.h"
-#include "storm/models/sparse/StandardRewardModel.h"
-#include "storm/models/sparse/Model.h"
-#include "storm/storage/SparseMatrix.h"
-#include "storm/storage/BitVectorHashMap.h"
-
-#include "storm-dft/storage/dft/DFT.h"
-#include "storm-dft/storage/dft/SymmetricUnits.h"
-
-
-
-
-
-namespace storm {
-    namespace builder {
-
-        template<typename ValueType>
-        class ExplicitDFTModelBuilder {
-
-            using DFTElementPointer = std::shared_ptr<storm::storage::DFTElement<ValueType>>;
-            using DFTElementCPointer = std::shared_ptr<storm::storage::DFTElement<ValueType> const>;
-            using DFTGatePointer = std::shared_ptr<storm::storage::DFTGate<ValueType>>;
-            using DFTStatePointer = std::shared_ptr<storm::storage::DFTState<ValueType>>;
-            using DFTRestrictionPointer = std::shared_ptr<storm::storage::DFTRestriction<ValueType>>;
-
-
-            // A structure holding the individual components of a model.
-            struct ModelComponents {
-                ModelComponents();
-
-                // The transition matrix.
-                storm::storage::SparseMatrix<ValueType> transitionMatrix;
-
-                // The state labeling.
-                storm::models::sparse::StateLabeling stateLabeling;
-
-                // The Markovian states.
-                storm::storage::BitVector markovianStates;
-
-                // The exit rates.
-                std::vector<ValueType> exitRates;
-
-                // A vector that stores a labeling for each choice.
-                boost::optional<storm::models::sparse::ChoiceLabeling> choiceLabeling;
-            };
-            
-            const size_t INITIAL_BUCKETSIZE = 20000;
-            const uint_fast64_t OFFSET_PSEUDO_STATE = UINT_FAST64_MAX / 2;
-            
-            storm::storage::DFT<ValueType> const& mDft;
-            std::shared_ptr<storm::storage::DFTStateGenerationInfo> mStateGenerationInfo;
-            storm::storage::BitVectorHashMap<uint_fast64_t> mStates;
-            std::vector<std::pair<uint_fast64_t, storm::storage::BitVector>> mPseudoStatesMapping; // vector of (id to concrete state, bitvector)
-            size_t newIndex = 0;
-            bool mergeFailedStates = false;
-            bool enableDC = true;
-            size_t failedIndex = 0;
-            size_t initialStateIndex = 0;
-
-        public:
-            struct LabelOptions {
-                bool buildFailLabel = true;
-                bool buildFailSafeLabel = false;
-                std::set<std::string> beLabels = {};
-            };
-            
-            ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC);
-
-            std::shared_ptr<storm::models::sparse::Model<ValueType>> buildModel(LabelOptions const& labelOpts);
-
-        private:
-            std::pair<uint_fast64_t, bool> exploreStates(DFTStatePointer const& state, size_t& rowOffset, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<uint_fast64_t>& markovianStates, std::vector<ValueType>& exitRates);
-            
-            /*!
-             * Adds a state to the explored states and handles pseudo states.
-             *
-             * @param state The state to add.
-             * @return Id of added state.
-             */
-            uint_fast64_t addState(DFTStatePointer const& state);
-            
-            /*!
-             * Check if state needs an exploration and remember pseudo states for later creation.
-             *
-             * @param state State which might need exploration.
-             * @return Pair of flag indicating whether the state needs exploration now and the state id if the state already
-             * exists.
-             */
-            std::pair<bool, uint_fast64_t> checkForExploration(DFTStatePointer const& state);
-
-        };
-    }
-}
diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
index 45d97baa6..3a69cb5e4 100644
--- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
+++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
@@ -5,7 +5,6 @@
 #include "storm/utility/bitoperations.h"
 #include "storm/utility/DirectEncodingExporter.h"
 
-#include "storm-dft/builder/ExplicitDFTModelBuilder.h"
 #include "storm-dft/builder/ExplicitDFTModelBuilderApprox.h"
 #include "storm-dft/storage/dft/DFTIsomorphism.h"
 #include "storm-dft/settings/modules/FaultTreeSettings.h"
@@ -342,18 +341,10 @@ namespace storm {
             } else {
                 // Build a single Markov Automaton
                 STORM_LOG_INFO("Building Model...");
-                std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
-                // TODO Matthias: use only one builder if everything works again
-                if (storm::settings::getModule<storm::settings::modules::FaultTreeSettings>().isApproximationErrorSet()) {
-                    storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(dft, symmetries, enableDC);
-                    typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions(properties, storm::settings::getModule<storm::settings::modules::IOSettings>().isExportExplicitSet());
-                    builder.buildModel(labeloptions, 0, 0.0);
-                    model = builder.getModel();
-                } else {
-                    storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, enableDC);
-                    typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions;
-                    model = builder.buildModel(labeloptions);
-                }
+                storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(dft, symmetries, enableDC);
+                typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions(properties, storm::settings::getModule<storm::settings::modules::IOSettings>().isExportExplicitSet());
+                builder.buildModel(labeloptions, 0, 0.0);
+                std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
                 model->printModelInformationToStream(std::cout);
                 explorationTimer.stop();
 

From 0913388cd3cb7952d43b37661547efc7abf64072 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Fri, 13 Oct 2017 18:11:05 +0200
Subject: [PATCH 7/7] Renamed ExplicitDFTModelBuilderApprox to
 ExplicitDFTModelBuilder

---
 ...Approx.cpp => ExplicitDFTModelBuilder.cpp} | 46 +++++++++----------
 ...lderApprox.h => ExplicitDFTModelBuilder.h} |  4 +-
 .../modelchecker/dft/DFTModelChecker.cpp      | 19 ++++----
 3 files changed, 34 insertions(+), 35 deletions(-)
 rename src/storm-dft/builder/{ExplicitDFTModelBuilderApprox.cpp => ExplicitDFTModelBuilder.cpp} (94%)
 rename src/storm-dft/builder/{ExplicitDFTModelBuilderApprox.h => ExplicitDFTModelBuilder.h} (98%)

diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
similarity index 94%
rename from src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
rename to src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
index c7d6605f5..2b74432ad 100644
--- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
+++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
@@ -1,4 +1,4 @@
-#include "ExplicitDFTModelBuilderApprox.h"
+#include "ExplicitDFTModelBuilder.h"
 
 #include <map>
 
@@ -17,18 +17,18 @@ namespace storm {
     namespace builder {
 
         template<typename ValueType, typename StateType>
-        ExplicitDFTModelBuilderApprox<ValueType, StateType>::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), markovianStates(), exitRates(), choiceLabeling() {
+        ExplicitDFTModelBuilder<ValueType, StateType>::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), markovianStates(), exitRates(), choiceLabeling() {
             // Intentionally left empty.
         }
 
         template<typename ValueType, typename StateType>
-        ExplicitDFTModelBuilderApprox<ValueType, StateType>::MatrixBuilder::MatrixBuilder(bool canHaveNondeterminism) : mappingOffset(0), stateRemapping(), currentRowGroup(0), currentRow(0), canHaveNondeterminism((canHaveNondeterminism)) {
+        ExplicitDFTModelBuilder<ValueType, StateType>::MatrixBuilder::MatrixBuilder(bool canHaveNondeterminism) : mappingOffset(0), stateRemapping(), currentRowGroup(0), currentRow(0), canHaveNondeterminism((canHaveNondeterminism)) {
             // Create matrix builder
             builder = storm::storage::SparseMatrixBuilder<ValueType>(0, 0, 0, false, canHaveNondeterminism, 0);
         }
 
         template<typename ValueType, typename StateType>
-        ExplicitDFTModelBuilderApprox<ValueType, StateType>::LabelOptions::LabelOptions(std::vector<std::shared_ptr<const storm::logic::Formula>> properties, bool buildAllLabels) : buildFailLabel(true), buildFailSafeLabel(false), buildAllLabels(buildAllLabels) {
+        ExplicitDFTModelBuilder<ValueType, StateType>::LabelOptions::LabelOptions(std::vector<std::shared_ptr<const storm::logic::Formula>> properties, bool buildAllLabels) : buildFailLabel(true), buildFailSafeLabel(false), buildAllLabels(buildAllLabels) {
             // Get necessary labels from properties
             std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> atomicLabels;
             for (auto property : properties) {
@@ -51,7 +51,7 @@ namespace storm {
         }
 
         template<typename ValueType, typename StateType>
-        ExplicitDFTModelBuilderApprox<ValueType, StateType>::ExplicitDFTModelBuilderApprox(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC) :
+        ExplicitDFTModelBuilder<ValueType, StateType>::ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC) :
                 dft(dft),
                 stateGenerationInfo(std::make_shared<storm::storage::DFTStateGenerationInfo>(dft.buildStateGenerationInfo(symmetries))),
                 enableDC(enableDC),
@@ -124,7 +124,7 @@ namespace storm {
         }
 
         template<typename ValueType, typename StateType>
-        void ExplicitDFTModelBuilderApprox<ValueType, StateType>::buildModel(LabelOptions const& labelOpts, size_t iteration, double approximationThreshold) {
+        void ExplicitDFTModelBuilder<ValueType, StateType>::buildModel(LabelOptions const& labelOpts, size_t iteration, double approximationThreshold) {
             STORM_LOG_TRACE("Generating DFT state space");
 
             if (iteration < 1) {
@@ -156,7 +156,7 @@ namespace storm {
                 }
 
                 // Build initial state
-                this->stateStorage.initialStateIndices = generator.getInitialStates(std::bind(&ExplicitDFTModelBuilderApprox::getOrAddStateIndex, this, std::placeholders::_1));
+                this->stateStorage.initialStateIndices = generator.getInitialStates(std::bind(&ExplicitDFTModelBuilder::getOrAddStateIndex, this, std::placeholders::_1));
                 STORM_LOG_ASSERT(stateStorage.initialStateIndices.size() == 1, "Only one initial state assumed.");
                 initialStateIndex = stateStorage.initialStateIndices[0];
                 STORM_LOG_TRACE("Initial state: " << initialStateIndex);
@@ -214,7 +214,7 @@ namespace storm {
         }
 
         template<typename ValueType, typename StateType>
-        void ExplicitDFTModelBuilderApprox<ValueType, StateType>::initializeNextIteration() {
+        void ExplicitDFTModelBuilder<ValueType, StateType>::initializeNextIteration() {
             STORM_LOG_TRACE("Refining DFT state space");
 
             // TODO Matthias: should be easier now as skipped states all are at the end of the matrix
@@ -316,7 +316,7 @@ namespace storm {
         }
 
         template<typename ValueType, typename StateType>
-        void ExplicitDFTModelBuilderApprox<ValueType, StateType>::exploreStateSpace(double approximationThreshold) {
+        void ExplicitDFTModelBuilder<ValueType, StateType>::exploreStateSpace(double approximationThreshold) {
             size_t nrExpandedStates = 0;
             size_t nrSkippedStates = 0;
             // TODO Matthias: do not empty queue every time but break before
@@ -364,7 +364,7 @@ namespace storm {
                 } else {
                     // Explore the current state
                     ++nrExpandedStates;
-                    storm::generator::StateBehavior<ValueType, StateType> behavior = generator.expand(std::bind(&ExplicitDFTModelBuilderApprox::getOrAddStateIndex, this, std::placeholders::_1));
+                    storm::generator::StateBehavior<ValueType, StateType> behavior = generator.expand(std::bind(&ExplicitDFTModelBuilder::getOrAddStateIndex, this, std::placeholders::_1));
                     STORM_LOG_ASSERT(!behavior.empty(), "Behavior is empty.");
                     setMarkovian(behavior.begin()->isMarkovian());
 
@@ -424,7 +424,7 @@ namespace storm {
         }
 
         template<typename ValueType, typename StateType>
-        void ExplicitDFTModelBuilderApprox<ValueType, StateType>::buildLabeling(LabelOptions const& labelOpts) {
+        void ExplicitDFTModelBuilder<ValueType, StateType>::buildLabeling(LabelOptions const& labelOpts) {
             // Build state labeling
             modelComponents.stateLabeling = storm::models::sparse::StateLabeling(modelComponents.transitionMatrix.getRowGroupCount());
             // Initial state
@@ -473,13 +473,13 @@ namespace storm {
         }
 
         template<typename ValueType, typename StateType>
-        std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilderApprox<ValueType, StateType>::getModel() {
+        std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilder<ValueType, StateType>::getModel() {
             STORM_LOG_ASSERT(skippedStates.size() == 0, "Concrete model has skipped states");
             return createModel(false);
         }
 
         template<typename ValueType, typename StateType>
-        std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilderApprox<ValueType, StateType>::getModelApproximation(bool lowerBound, bool expectedTime) {
+        std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilder<ValueType, StateType>::getModelApproximation(bool lowerBound, bool expectedTime) {
             if (expectedTime) {
                 // TODO Matthias: handle case with no skipped states
                 changeMatrixBound(modelComponents.transitionMatrix, lowerBound);
@@ -550,7 +550,7 @@ namespace storm {
         }
 
         template<typename ValueType, typename StateType>
-        std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilderApprox<ValueType, StateType>::createModel(bool copy) {
+        std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilder<ValueType, StateType>::createModel(bool copy) {
             std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
 
             if (modelComponents.deterministicModel) {
@@ -607,7 +607,7 @@ namespace storm {
         }
 
         template<typename ValueType, typename StateType>
-        void ExplicitDFTModelBuilderApprox<ValueType, StateType>::changeMatrixBound(storm::storage::SparseMatrix<ValueType> & matrix, bool lowerBound) const {
+        void ExplicitDFTModelBuilder<ValueType, StateType>::changeMatrixBound(storm::storage::SparseMatrix<ValueType> & matrix, bool lowerBound) const {
             // Set lower bound for skipped states
             for (auto it = skippedStates.begin(); it != skippedStates.end(); ++it) {
                 auto matrixEntry = matrix.getRow(it->first, 0).begin();
@@ -632,7 +632,7 @@ namespace storm {
         }
 
         template<typename ValueType, typename StateType>
-        ValueType ExplicitDFTModelBuilderApprox<ValueType, StateType>::getLowerBound(DFTStatePointer const& state) const {
+        ValueType ExplicitDFTModelBuilder<ValueType, StateType>::getLowerBound(DFTStatePointer const& state) const {
             // Get the lower bound by considering the failure of all possible BEs
             ValueType lowerBound = storm::utility::zero<ValueType>();
             for (size_t index = 0; index < state->nrFailableBEs(); ++index) {
@@ -642,7 +642,7 @@ namespace storm {
         }
 
         template<typename ValueType, typename StateType>
-        ValueType ExplicitDFTModelBuilderApprox<ValueType, StateType>::getUpperBound(DFTStatePointer const& state) const {
+        ValueType ExplicitDFTModelBuilder<ValueType, StateType>::getUpperBound(DFTStatePointer const& state) const {
             if (state->hasFailed(dft.getTopLevelIndex())) {
                 return storm::utility::zero<ValueType>();
             }
@@ -709,7 +709,7 @@ namespace storm {
         }
 
         template<typename ValueType, typename StateType>
-        ValueType ExplicitDFTModelBuilderApprox<ValueType, StateType>::computeMTTFAnd(std::vector<ValueType> const& rates, size_t size) const {
+        ValueType ExplicitDFTModelBuilder<ValueType, StateType>::computeMTTFAnd(std::vector<ValueType> const& rates, size_t size) const {
             ValueType result = storm::utility::zero<ValueType>();
             if (size == 0) {
                 return result;
@@ -762,7 +762,7 @@ namespace storm {
         }
 
         template<typename ValueType, typename StateType>
-        StateType ExplicitDFTModelBuilderApprox<ValueType, StateType>::getOrAddStateIndex(DFTStatePointer const& state) {
+        StateType ExplicitDFTModelBuilder<ValueType, StateType>::getOrAddStateIndex(DFTStatePointer const& state) {
             StateType stateId;
             bool changed = false;
 
@@ -811,7 +811,7 @@ namespace storm {
         }
 
         template<typename ValueType, typename StateType>
-        void ExplicitDFTModelBuilderApprox<ValueType, StateType>::setMarkovian(bool markovian) {
+        void ExplicitDFTModelBuilder<ValueType, StateType>::setMarkovian(bool markovian) {
             if (matrixBuilder.getCurrentRowGroup() > modelComponents.markovianStates.size()) {
                 // Resize BitVector
                 modelComponents.markovianStates.resize(modelComponents.markovianStates.size() + INITIAL_BITVECTOR_SIZE);
@@ -820,7 +820,7 @@ namespace storm {
         }
 
         template<typename ValueType, typename StateType>
-        void ExplicitDFTModelBuilderApprox<ValueType, StateType>::printNotExplored() const {
+        void ExplicitDFTModelBuilder<ValueType, StateType>::printNotExplored() const {
             std::cout << "states not explored:" << std::endl;
             for (auto it : statesNotExplored) {
                 std::cout << it.first << " -> " << dft.getStateString(it.second.first) << std::endl;
@@ -829,10 +829,10 @@ namespace storm {
 
 
         // Explicitly instantiate the class.
-        template class ExplicitDFTModelBuilderApprox<double>;
+        template class ExplicitDFTModelBuilder<double>;
 
 #ifdef STORM_HAVE_CARL
-        template class ExplicitDFTModelBuilderApprox<storm::RationalFunction>;
+        template class ExplicitDFTModelBuilder<storm::RationalFunction>;
 #endif
 
     } // namespace builder
diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h b/src/storm-dft/builder/ExplicitDFTModelBuilder.h
similarity index 98%
rename from src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h
rename to src/storm-dft/builder/ExplicitDFTModelBuilder.h
index 802aefe1b..b96dea410 100644
--- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h
+++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.h
@@ -26,7 +26,7 @@ namespace storm {
          * Build a Markov chain from DFT.
          */
         template<typename ValueType, typename StateType = uint32_t>
-        class ExplicitDFTModelBuilderApprox {
+        class ExplicitDFTModelBuilder {
 
             using DFTStatePointer = std::shared_ptr<storm::storage::DFTState<ValueType>>;
             // TODO Matthias: make choosable
@@ -177,7 +177,7 @@ namespace storm {
              * @param symmetries Symmetries in the dft.
              * @param enableDC Flag indicating if dont care propagation should be used.
              */
-            ExplicitDFTModelBuilderApprox(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC);
+            ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC);
 
             /*!
              * Build model from DFT.
diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
index 3a69cb5e4..d2b435c1c 100644
--- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
+++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
@@ -5,7 +5,7 @@
 #include "storm/utility/bitoperations.h"
 #include "storm/utility/DirectEncodingExporter.h"
 
-#include "storm-dft/builder/ExplicitDFTModelBuilderApprox.h"
+#include "storm-dft/builder/ExplicitDFTModelBuilder.h"
 #include "storm-dft/storage/dft/DFTIsomorphism.h"
 #include "storm-dft/settings/modules/FaultTreeSettings.h"
 
@@ -191,8 +191,8 @@ namespace storm {
 
                     // Build a single CTMC
                     STORM_LOG_INFO("Building Model...");
-                    storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(ft, symmetries, enableDC);
-                    typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions(properties);
+                    storm::builder::ExplicitDFTModelBuilder<ValueType> builder(ft, symmetries, enableDC);
+                    typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties);
                     builder.buildModel(labeloptions, 0, 0.0);
                     std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
                     explorationTimer.stop();
@@ -243,9 +243,8 @@ namespace storm {
                 // Build a single CTMC
                 STORM_LOG_INFO("Building Model...");
 
-
-                storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(dft, symmetries, enableDC);
-                typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions(properties);
+                storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, enableDC);
+                typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties);
                 builder.buildModel(labeloptions, 0, 0.0);
                 std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
                 model->printModelInformationToStream(std::cout);
@@ -276,8 +275,8 @@ namespace storm {
                 approximation_result approxResult = std::make_pair(storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>());
                 std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
                 std::vector<ValueType> newResult;
-                storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(dft, symmetries, enableDC);
-                typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions(properties);
+                storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, enableDC);
+                typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties);
 
                 // TODO Matthias: compute approximation for all properties simultaneously?
                 std::shared_ptr<const storm::logic::Formula> property = properties[0];
@@ -341,8 +340,8 @@ namespace storm {
             } else {
                 // Build a single Markov Automaton
                 STORM_LOG_INFO("Building Model...");
-                storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(dft, symmetries, enableDC);
-                typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions(properties, storm::settings::getModule<storm::settings::modules::IOSettings>().isExportExplicitSet());
+                storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, enableDC);
+                typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties, storm::settings::getModule<storm::settings::modules::IOSettings>().isExportExplicitSet());
                 builder.buildModel(labeloptions, 0, 0.0);
                 std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
                 model->printModelInformationToStream(std::cout);