From aa150fc2e36eac98711e260f9fa85c9cab449188 Mon Sep 17 00:00:00 2001
From: Alexander Bork <alexander.bork@rwth-aachen.de>
Date: Fri, 7 Jun 2019 15:36:33 +0200
Subject: [PATCH] Extended FDEP conflict search by not considering pairs of
 FDEPs with static behavior

---
 .../modelchecker/dft/DFTASFChecker.cpp        | 52 +++++++++++--------
 1 file changed, 31 insertions(+), 21 deletions(-)

diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
index 668c75757..133a5ea14 100644
--- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
+++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
@@ -948,28 +948,38 @@ namespace storm {
                 dep1Index = dft.getDependencies().at(i);
                 for (size_t j = i + 1; j < dft.getDependencies().size(); ++j) {
                     dep2Index = dft.getDependencies().at(j);
-                    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;
+                    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;
                     }
                 }
             }