Added activation for experimental DFT SMT analysis

src/storm-dft-cli/storm-dft.cpp

@@ -7,6 +7,7 @@
 #include "storm-dft/settings/modules/FaultTreeSettings.h"
 #include <storm/exceptions/UnmetRequirementException.h>
 #include "storm/settings/modules/GeneralSettings.h"
+#include "storm/settings/modules/DebugSettings.h"
 #include "storm/settings/modules/IOSettings.h"
 #include "storm/settings/modules/ResourceSettings.h"
 #include "storm/utility/initialize.h"
@@ -80,9 +81,10 @@ void processOptions() {
 
 #ifdef STORM_HAVE_Z3
     if (faultTreeSettings.solveWithSMT()) {
+        auto const& debug = storm::settings::getModule<storm::settings::modules::DebugSettings>();
         // Solve with SMT
         STORM_LOG_DEBUG("Running DFT analysis with use of SMT");
-        storm::api::analyzeDFTSMT(*dft, true);
+        storm::api::analyzeDFTSMT(*dft, true, debug.isTestSet());
         return;
     }
 #endif

src/storm-dft/api/storm-dft.cpp

@@ -44,10 +44,13 @@ namespace storm {
 
         template<>
         storm::api::SMTResult
-        analyzeDFTSMT(storm::storage::DFT<double> const &dft, bool printOutput) {
+        analyzeDFTSMT(storm::storage::DFT<double> const &dft, bool printOutput, bool experimentalMode) {
             uint64_t solverTimeout = 10;
 
             storm::modelchecker::DFTASFChecker smtChecker(dft);
+            if (experimentalMode) {
+                smtChecker.activateExperimentalMode();
+            }
             smtChecker.toSolver();
             storm::api::SMTResult results;
 
@@ -77,7 +80,8 @@ namespace storm {
 
         template<>
         storm::api::SMTResult
-        analyzeDFTSMT(storm::storage::DFT<storm::RationalFunction> const &dft, bool printOutput) {
+        analyzeDFTSMT(storm::storage::DFT<storm::RationalFunction> const &dft, bool printOutput,
+                      bool experimentalMode) {
             STORM_LOG_THROW(false, storm::exceptions::NotSupportedException,
                             "Analysis by SMT not supported for this data type.");
         }

src/storm-dft/api/storm-dft.h

@@ -107,7 +107,7 @@ namespace storm {
          */
         template<typename ValueType>
         storm::api::SMTResult
-        analyzeDFTSMT(storm::storage::DFT<ValueType> const &dft, bool printOutput);
+        analyzeDFTSMT(storm::storage::DFT<ValueType> const &dft, bool printOutput, bool experimentalMode);
 
         /*!
          * Export DFT to JSON file.

src/storm-dft/modelchecker/dft/DFTASFChecker.cpp

@@ -18,6 +18,11 @@ namespace storm {
             // Intentionally left empty.
         }
 
+        void DFTASFChecker::activateExperimentalMode() {
+            STORM_LOG_WARN("DFT-SMT-Checker now runs in experimental mode, no guarantee for correct results is given!");
+            experimentalMode = true;
+        }
+
         uint64_t DFTASFChecker::getClaimVariableIndex(uint64_t spare, uint64_t child) const {
             return claimVariables.at(SpareAndChildPair(spare, child));
         }
@@ -36,7 +41,9 @@ namespace storm {
                         beVariables.push_back(varNames.size() - 1);
                         break;
                     case storm::storage::DFTElementType::BE_CONST:
-                        STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Constant BEs are not supported in SMT translation.");
+                        STORM_LOG_THROW(experimentalMode, storm::exceptions::NotSupportedException,
+                                        "Constant BEs are not supported in SMT translation.");
+                        STORM_LOG_WARN("Constant BEs are only experimentally supported");
                         break;
                     case storm::storage::DFTElementType::SPARE:
                     {
@@ -612,6 +619,7 @@ namespace storm {
 
         storm::solver::SmtSolver::CheckResult
         DFTASFChecker::checkDependencyConflict(uint64_t dep1Index, uint64_t dep2Index, uint64_t timeout) {
+            //TODO make constraints easier?
             std::vector<std::shared_ptr<SmtConstraint>> andConstr;
             std::vector<std::shared_ptr<SmtConstraint>> orConstr;
             STORM_LOG_DEBUG(

src/storm-dft/modelchecker/dft/DFTASFChecker.h

@@ -44,6 +44,13 @@ namespace storm {
             using ValueType = double;
         public:
             DFTASFChecker(storm::storage::DFT<ValueType> const&);
+
+            /**
+             * Activates the experimental support for constant BEs and possibly other not thoroughly tested features
+             *
+             */
+            void activateExperimentalMode();
+
             /**
              * Generate general variables and constraints for the DFT and store them in the corresponding maps and vectors
              *
@@ -264,6 +271,7 @@ namespace storm {
             std::unordered_map<uint64_t, uint64_t> markovianVariables;
             std::vector<uint64_t> tmpTimePointVariables;
             uint64_t notFailed;
+            bool experimentalMode = false;
         };
     }
 }