From a25707134665a4147e0e2a1ec8a509e2bf656e9e Mon Sep 17 00:00:00 2001
From: Alexander Bork <alexander.bork@rwth-aachen.de>
Date: Wed, 7 Aug 2019 17:10:47 +0200
Subject: [PATCH] Added option to transform a DFT to only use one unique
 constantly failed BE

---
 src/storm-dft-cli/storm-dft.cpp                    | 14 +++++---------
 .../settings/modules/FaultTreeSettings.cpp         |  7 +++++++
 src/storm-dft/settings/modules/FaultTreeSettings.h |  8 ++++++++
 3 files changed, 20 insertions(+), 9 deletions(-)

diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp
index 34bd53b69..d5f4bba36 100644
--- a/src/storm-dft-cli/storm-dft.cpp
+++ b/src/storm-dft-cli/storm-dft.cpp
@@ -56,6 +56,11 @@ void processOptions() {
         storm::api::exportDFTToJsonFile<ValueType>(*dft, dftIOSettings.getExportJsonFilename());
     }
 
+    // Limit to one constantly failed BE
+    if (faultTreeSettings.isUniqueFailedBE()) {
+        dft = dftTransformator.transformUniqueFailedBe(*dft);
+    }
+
     // Eliminate non-binary dependencies
     if (!dft->getDependencies().empty()) {
         dft = dftTransformator.transformBinaryFDEPs(*dft);
@@ -82,10 +87,6 @@ void processOptions() {
 
     // SMT
     if (dftIOSettings.isExportToSmt()) {
-        dft = dftTransformator.transformUniqueFailedBe(*dft);
-        if (!dft->getDependencies().empty()) {
-            dft = dftTransformator.transformBinaryFDEPs(*dft);
-        }
         // Export to smtlib2
         storm::api::exportDFTToSMT<ValueType>(*dft, dftIOSettings.getExportSmtFilename());
         return;
@@ -98,11 +99,6 @@ void processOptions() {
     if (faultTreeSettings.solveWithSMT()) {
         useSMT = true;
         STORM_PRINT("Use SMT for preprocessing" << std::endl)
-        dft = dftTransformator.transformUniqueFailedBe(*dft);
-        if (!dft->getDependencies().empty()) {
-            // Making the constantly failed BE unique may introduce non-binary FDEPs
-            dft = dftTransformator.transformBinaryFDEPs(*dft);
-        }
     }
 #endif
 
diff --git a/src/storm-dft/settings/modules/FaultTreeSettings.cpp b/src/storm-dft/settings/modules/FaultTreeSettings.cpp
index b45c37498..3fa4d6529 100644
--- a/src/storm-dft/settings/modules/FaultTreeSettings.cpp
+++ b/src/storm-dft/settings/modules/FaultTreeSettings.cpp
@@ -26,6 +26,7 @@ namespace storm {
             const std::string FaultTreeSettings::approximationHeuristicOptionName = "approximationheuristic";
             const std::string FaultTreeSettings::maxDepthOptionName = "maxdepth";
             const std::string FaultTreeSettings::firstDependencyOptionName = "firstdep";
+            const std::string FaultTreeSettings::uniqueFailedBEOptionName = "uniquefailedbe";
 #ifdef STORM_HAVE_Z3
             const std::string FaultTreeSettings::solveWithSmtOptionName = "smt";
 #endif
@@ -53,6 +54,8 @@ namespace storm {
                                                                      {"depth", "probability", "bounddifference"})).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, maxDepthOptionName, false, "Maximal depth for state space exploration.").addArgument(
                         storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("depth", "The maximal depth.").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, uniqueFailedBEOptionName, false,
+                                                               "Use a unique constantly failed BE.").build());
 #ifdef STORM_HAVE_Z3
                 this->addOption(storm::settings::OptionBuilder(moduleName, solveWithSmtOptionName, true, "Solve the DFT with SMT.").build());
 #endif
@@ -115,6 +118,10 @@ namespace storm {
                 return this->getOption(firstDependencyOptionName).getHasOptionBeenSet();
             }
 
+            bool FaultTreeSettings::isUniqueFailedBE() const {
+                return this->getOption(uniqueFailedBEOptionName).getHasOptionBeenSet();
+            }
+
 #ifdef STORM_HAVE_Z3
 
             bool FaultTreeSettings::solveWithSMT() const {
diff --git a/src/storm-dft/settings/modules/FaultTreeSettings.h b/src/storm-dft/settings/modules/FaultTreeSettings.h
index 5ed230bfb..6c5298f7b 100644
--- a/src/storm-dft/settings/modules/FaultTreeSettings.h
+++ b/src/storm-dft/settings/modules/FaultTreeSettings.h
@@ -103,6 +103,13 @@ namespace storm {
                  */
                 bool isTakeFirstDependency() const;
 
+                /*!
+                 * Retrieves whether the DFT should be transformed to contain at most one constantly failed BE.
+                 *
+                 * @return True iff the option was set.
+                  */
+                bool isUniqueFailedBE() const;
+
 #ifdef STORM_HAVE_Z3
 
                 /*!
@@ -134,6 +141,7 @@ namespace storm {
                 static const std::string approximationHeuristicOptionName;
                 static const std::string maxDepthOptionName;
                 static const std::string firstDependencyOptionName;
+                static const std::string uniqueFailedBEOptionName;
 #ifdef STORM_HAVE_Z3
                 static const std::string solveWithSmtOptionName;
 #endif