From baa8a6dbcbcdbac45e3eb6b59473ebd02b155b66 Mon Sep 17 00:00:00 2001
From: Alexander Bork <alexander.bork@rwth-aachen.de>
Date: Fri, 17 May 2019 16:56:12 +0200
Subject: [PATCH] Improved conflict search by directly capturing DEPs with same
 trigger

---
 src/storm-dft/api/storm-dft.cpp               | 10 +++--
 .../modelchecker/dft/DFTASFChecker.cpp        | 37 +++++++++++--------
 2 files changed, 29 insertions(+), 18 deletions(-)

diff --git a/src/storm-dft/api/storm-dft.cpp b/src/storm-dft/api/storm-dft.cpp
index 6f9943768..16b6f4d00 100644
--- a/src/storm-dft/api/storm-dft.cpp
+++ b/src/storm-dft/api/storm-dft.cpp
@@ -45,19 +45,23 @@ namespace storm {
         template<>
         storm::api::SMTResult
         analyzeDFTSMT(storm::storage::DFT<double> const &dft, bool printOutput) {
+            uint64_t solverTimeout = 10;
+
             storm::modelchecker::DFTASFChecker smtChecker(dft);
             smtChecker.toSolver();
             storm::api::SMTResult results;
 
-            results.lowerBEBound = smtChecker.getLeastFailureBound();
-            results.upperBEBound = smtChecker.getAlwaysFailedBound();
+            results.lowerBEBound = smtChecker.getLeastFailureBound(solverTimeout);
+            results.upperBEBound = smtChecker.getAlwaysFailedBound(solverTimeout);
             if (printOutput) {
                 STORM_PRINT("BE FAILURE BOUNDS" << std::endl <<
                                                 "========================================" << std::endl <<
                                                 "Lower bound: " << std::to_string(results.lowerBEBound) << std::endl <<
                                                 "Upper bound: " << std::to_string(results.upperBEBound) << std::endl)
             }
-            results.fdepConflicts = smtChecker.getDependencyConflicts();
+
+            results.fdepConflicts = smtChecker.getDependencyConflicts(solverTimeout);
+
             if (printOutput) {
                 STORM_PRINT("========================================" << std::endl <<
                                                                        "FDEP CONFLICTS" << std::endl <<
diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
index beecbc805..85326c8b2 100644
--- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
+++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
@@ -798,21 +798,28 @@ namespace storm {
                 dep1Index = dft.getDependencies().at(i);
                 for (size_t j = i + 1; j < dft.getDependencies().size(); ++j) {
                     dep2Index = dft.getDependencies().at(j);
-                    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;
+                    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;
+                        }
                     }
                 }
             }