Decoupled FDEP conflict search and SMT solver

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

@@ -4,6 +4,7 @@
 #include "storm-dft/settings/modules/DftGspnSettings.h"
 #include "storm-conv/settings/modules/JaniExportSettings.h"
 #include "storm-conv/api/storm-conv.h"
+#include "storm-dft/utility/FDEPConflictFinder.h"
 
 namespace storm {
     namespace api {
@@ -67,7 +68,8 @@ namespace storm {
                                                 "Upper bound: " << std::to_string(results.upperBEBound) << std::endl)
             }
 
-            results.fdepConflicts = smtChecker.getDependencyConflicts(solverTimeout);
+            results.fdepConflicts = storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(dft, true,
+                                                                                                    solverTimeout);
 
             if (printOutput) {
                 STORM_PRINT("========================================" << std::endl <<

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

@@ -13,7 +13,7 @@
 
 namespace storm {
     namespace api {
-        struct SMTResult {
+        struct PreprocessingResult {
             uint64_t lowerBEBound;
             uint64_t upperBEBound;
             std::vector<std::pair<uint64_t, uint64_t>> fdepConflicts;

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

@@ -939,51 +939,5 @@ namespace storm {
             return bound;
         }
 
-        std::vector<std::pair<uint64_t, uint64_t>> DFTASFChecker::getDependencyConflicts(uint_fast64_t timeout) {
-            STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries");
-            std::vector<std::pair<uint64_t, uint64_t>> res;
-            uint64_t dep1Index;
-            uint64_t dep2Index;
-            for (size_t i = 0; i < dft.getDependencies().size(); ++i) {
-                dep1Index = dft.getDependencies().at(i);
-                for (size_t j = i + 1; j < dft.getDependencies().size(); ++j) {
-                    dep2Index = dft.getDependencies().at(j);
-                    if (dft.getDynamicBehavior()[dep1Index] && dft.getDynamicBehavior()[dep2Index]) {
-                        if (dft.getDependency(dep1Index)->triggerEvent() ==
-                            dft.getDependency(dep2Index)->triggerEvent()) {
-                            STORM_LOG_DEBUG("Conflict between " << dft.getElement(dep1Index)->name() << " and "
-                                                                << dft.getElement(dep2Index)->name()
-                                                                << ": Same trigger");
-                            res.emplace_back(std::pair<uint64_t, uint64_t>(dep1Index, dep2Index));
-                        } else {
-                            switch (checkDependencyConflict(dep1Index, dep2Index, timeout)) {
-                                case storm::solver::SmtSolver::CheckResult::Sat:
-                                    STORM_LOG_DEBUG("Conflict between " << dft.getElement(dep1Index)->name() << " and "
-                                                                        << dft.getElement(dep2Index)->name());
-                                    res.emplace_back(std::pair<uint64_t, uint64_t>(dep1Index, dep2Index));
-                                    break;
-                                case storm::solver::SmtSolver::CheckResult::Unknown:
-                                    STORM_LOG_DEBUG(
-                                            "Unknown: Conflict between " << dft.getElement(dep1Index)->name() << " and "
-                                                                         << dft.getElement(dep2Index)->name());
-                                    res.emplace_back(std::pair<uint64_t, uint64_t>(dep1Index, dep2Index));
-                                    break;
-                                default:
-                                    STORM_LOG_DEBUG(
-                                            "No conflict between " << dft.getElement(dep1Index)->name() << " and "
-                                                                   << dft.getElement(dep2Index)->name());
-                                    break;
-                            }
-                        }
-                    } else {
-                        STORM_LOG_DEBUG(
-                                "Static behavior: No conflict between " << dft.getElement(dep1Index)->name() << " and "
-                                                                        << dft.getElement(dep2Index)->name());
-                        break;
-                    }
-                }
-            }
-            return res;
-        }
     }
 }

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

@@ -116,13 +116,6 @@ namespace storm {
              */
             uint64_t getAlwaysFailedBound(uint_fast64_t timeout = 10);
 
-            /**
-             * Get a vector of index pairs of FDEPs which are conflicting according to a conservative definition
-             *
-             * @param timeout timeout for each query in seconds, defaults to 10 seconds
-             * @return a vector of pairs of FDEP indices which are conflicting
-             */
-            std::vector<std::pair<uint64_t, uint64_t>> getDependencyConflicts(uint_fast64_t timeout = 10);
 
             /**
              * Set the timeout of the solver

src/storm-dft/utility/FDEPConflictFinder.cpp

@@ -0,0 +1,112 @@
+#include "FDEPConflictFinder.h"
+
+namespace storm {
+    namespace dft {
+        namespace utility {
+
+            std::vector<std::pair<uint64_t, uint64_t>>
+            FDEPConflictFinder::getDependencyConflicts(storm::storage::DFT<double> const &dft,
+                                                       bool useSMT,
+                                                       uint_fast64_t timeout) {
+
+                std::shared_ptr<storm::modelchecker::DFTASFChecker> smtChecker = nullptr;
+                if (useSMT) {
+                    storm::modelchecker::DFTASFChecker checker(dft);
+                    smtChecker = std::make_shared<storm::modelchecker::DFTASFChecker>(checker);
+                    smtChecker->activateExperimentalMode();
+                    smtChecker->toSolver();
+                }
+
+                std::vector<std::pair<uint64_t, uint64_t>> res;
+                uint64_t dep1Index;
+                uint64_t dep2Index;
+                for (size_t i = 0; i < dft.getDependencies().size(); ++i) {
+                    dep1Index = dft.getDependencies().at(i);
+                    for (size_t j = i + 1; j < dft.getDependencies().size(); ++j) {
+                        dep2Index = dft.getDependencies().at(j);
+                        if (dft.getDynamicBehavior()[dep1Index] && dft.getDynamicBehavior()[dep2Index]) {
+                            if (useSMT) { // if an SMT solver is to be used
+                                if (dft.getDependency(dep1Index)->triggerEvent() ==
+                                    dft.getDependency(dep2Index)->triggerEvent()) {
+                                    STORM_LOG_DEBUG("Conflict between " << dft.getElement(dep1Index)->name() << " and "
+                                                                        << dft.getElement(dep2Index)->name()
+                                                                        << ": Same trigger");
+                                    res.emplace_back(std::pair<uint64_t, uint64_t>(dep1Index, dep2Index));
+                                } else {
+                                    switch (smtChecker->checkDependencyConflict(dep1Index, dep2Index, timeout)) {
+                                        case storm::solver::SmtSolver::CheckResult::Sat:
+                                            STORM_LOG_DEBUG(
+                                                    "Conflict between " << dft.getElement(dep1Index)->name() << " and "
+                                                                        << dft.getElement(dep2Index)->name());
+                                            res.emplace_back(std::pair<uint64_t, uint64_t>(dep1Index, dep2Index));
+                                            break;
+                                        case storm::solver::SmtSolver::CheckResult::Unknown:
+                                            STORM_LOG_DEBUG(
+                                                    "Unknown: Conflict between " << dft.getElement(dep1Index)->name()
+                                                                                 << " and "
+                                                                                 << dft.getElement(dep2Index)->name());
+                                            res.emplace_back(std::pair<uint64_t, uint64_t>(dep1Index, dep2Index));
+                                            break;
+                                        default:
+                                            STORM_LOG_DEBUG(
+                                                    "No conflict between " << dft.getElement(dep1Index)->name()
+                                                                           << " and "
+                                                                           << dft.getElement(dep2Index)->name());
+                                            break;
+                                    }
+                                }
+                            } else {
+                                STORM_LOG_DEBUG(
+                                        "Conflict between " << dft.getElement(dep1Index)->name() << " and "
+                                                            << dft.getElement(dep2Index)->name());
+                                res.emplace_back(std::pair<uint64_t, uint64_t>(dep1Index, dep2Index));
+                            }
+                        } else {
+                            STORM_LOG_DEBUG(
+                                    "Static behavior: No conflict between " << dft.getElement(dep1Index)->name()
+                                                                            << " and "
+                                                                            << dft.getElement(dep2Index)->name());
+                            break;
+                        }
+                    }
+                }
+                return res;
+            }
+
+            std::vector<std::pair<uint64_t, uint64_t>>
+            FDEPConflictFinder::getDependencyConflicts(storm::storage::DFT<storm::RationalFunction> const &dft,
+                                                       bool useSMT,
+                                                       uint_fast64_t timeout) {
+                if (useSMT) {
+                    STORM_LOG_WARN("SMT encoding for rational functions is not supported");
+                }
+
+                std::vector<std::pair<uint64_t, uint64_t>> res;
+                uint64_t dep1Index;
+                uint64_t dep2Index;
+                for (size_t i = 0; i < dft.getDependencies().size(); ++i) {
+                    dep1Index = dft.getDependencies().at(i);
+                    for (size_t j = i + 1; j < dft.getDependencies().size(); ++j) {
+                        dep2Index = dft.getDependencies().at(j);
+                        if (dft.getDynamicBehavior()[dep1Index] && dft.getDynamicBehavior()[dep2Index]) {
+                            STORM_LOG_DEBUG(
+                                    "Conflict between " << dft.getElement(dep1Index)->name() << " and "
+                                                        << dft.getElement(dep2Index)->name());
+                            res.emplace_back(std::pair<uint64_t, uint64_t>(dep1Index, dep2Index));
+                        } else {
+                            STORM_LOG_DEBUG(
+                                    "Static behavior: No conflict between " << dft.getElement(dep1Index)->name()
+                                                                            << " and "
+                                                                            << dft.getElement(dep2Index)->name());
+                            break;
+                        }
+                    }
+                }
+                return res;
+            }
+
+            class FDEPConflictFinder;
+
+        }
+    }
+}

src/storm-dft/utility/FDEPConflictFinder.h

@@ -0,0 +1,29 @@
+#include <vector>
+#include "storm-dft/storage/dft/DFT.h"
+#include "storm-dft/modelchecker/dft/DFTASFChecker.h"
+
+namespace storm {
+    namespace dft {
+        namespace utility {
+            class FDEPConflictFinder {
+            public:
+                /**
+                 * Get a vector of index pairs of FDEPs in the DFT which are conflicting. Two FDEPs are conflicting if
+                 * their simultaneous triggering may cause unresolvable non-deterministic behavior.
+                 *
+                 * @param dft the DFT
+                 * @param useSMT if set, an SMT solver is used to refine the conflict set
+                 * @param timeout timeout for each query in seconds, defaults to 10 seconds
+                 * @return a vector of pairs of indices. The indices in a pair refer to FDEPs which are conflicting
+                 */
+                static std::vector<std::pair<uint64_t, uint64_t>>
+                getDependencyConflicts(storm::storage::DFT<double> const &dft,
+                                       bool useSMT = false, uint_fast64_t timeout = 10);
+
+                static std::vector<std::pair<uint64_t, uint64_t>>
+                getDependencyConflicts(storm::storage::DFT<storm::RationalFunction> const &dft,
+                                       bool useSMT = false, uint_fast64_t timeout = 10);
+            };
+        }
+    }
+}

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

@@ -1,3 +1,4 @@
+#include <storm-dft/utility/FDEPConflictFinder.h>
 #include "gtest/gtest.h"
 #include "storm-config.h"
 
@@ -65,11 +66,8 @@ namespace {
 
         dft->setDynamicBehaviorInfo();
         EXPECT_EQ(dft->getDynamicBehavior(), true_vector);
-        storm::modelchecker::DFTASFChecker smtChecker(*dft);
-        smtChecker.convert();
-        smtChecker.toSolver();
 
-        EXPECT_TRUE(smtChecker.getDependencyConflicts().empty());
+        EXPECT_TRUE(storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, true).empty());
     }
 
     TEST(DftSmtTest, FDEPConflictSPARETest) {
@@ -80,11 +78,8 @@ namespace {
 
         dft->setDynamicBehaviorInfo();
         EXPECT_EQ(dft->getDynamicBehavior(), true_vector);
-        storm::modelchecker::DFTASFChecker smtChecker(*dft);
-        smtChecker.convert();
-        smtChecker.toSolver();
 
-        EXPECT_TRUE(smtChecker.getDependencyConflicts().empty());
+        EXPECT_TRUE(storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, true).empty());
     }
 
     TEST(DftSmtTest, FDEPConflictSEQTest) {
@@ -96,10 +91,7 @@ namespace {
 
         dft->setDynamicBehaviorInfo();
         EXPECT_EQ(dft->getDynamicBehavior(), expected_dynamic_vector);
-        storm::modelchecker::DFTASFChecker smtChecker(*dft);
-        smtChecker.convert();
-        smtChecker.toSolver();
 
-        EXPECT_EQ(smtChecker.getDependencyConflicts().size(), uint64_t(3));
+        EXPECT_EQ(storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, true).size(), uint64_t(3));
     }
 }